feat(PhyslibAlpha): finite path dimensional uncertainty chain

[naype888-cloud]

Summary

This PR submits the complete chain together, separated into atomic commits:

1. Fisher–Rao geometry and the Cramér–Rao bound on the finite open simplex.
2. HilbertSpace.PathSpectralGap: finite path habitat, Gram/Robertson bridge, canonical path observables, maximal-tension state, explicit Fiedler spectral decomposition, and the Niven saturation classification.
3. CStarAlgebra.DimensionalUncertainty: strict positivity from dimension four, the exact Szegő limit, monotonicity, terminal certificates, and related finite-dimensional corollaries.
4. A final integration commit exposing the chain through PhyslibAlpha.lean.

The mathematical purpose is to connect the general algebraic-state uncertainty API merged in #1649 and #1650 to an explicit finite-dimensional family, while also providing the Fisher–Rao side relevant to the Fubini–Study/information-geometry discussion.

Main definitions and results

The added files define Hd, the path observables Td and Pd, their commutator observable KdOp, the explicit Fiedler state, CNava, deltaGeom, and the Szegő limit Cinf. They prove the Gram form of Robertson–Schrödinger, hermiticity and noncommutativity of the path observables, the explicit path spectrum, saturation exactly in dimensions two and three, strict gap for every d ≥ 4, strict monotonicity on that tail, and convergence to a strictly positive limiting defect. Each source file contains its complete declaration-level documentation.

Reviewer map

1. PathSpectralGap/D0_Habitat through D3_GrafoCamino: setup and observables.
2. D5_MaximaTension and D6_Fiedler: operator and spectral core.
3. D7_Niven: equality classification.
4. DimensionalUncertainty/D8_Szego and D9_Monotonia: strict gap and asymptotics.
5. D10_Certificado and D11_CuantoMinimoArea: terminal certificates and corollary.
6. D12–D15: independent finite-dimensional complements.

Verification

• lake build PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimensionalUncertainty
• 3429 jobs completed successfully
• zero sorry, admit, or custom axioms in the submitted modules
• Mathlib/PhyslibAlpha imports only

The mathematical design and intended interpretation are by the human author. Code organization and porting were AI-assisted; the author will provide the requested human explanation and verified bibliography in the review thread.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[naype888-cloud]

hi Joseph i comiit this one large PR to make this happen quickly, im srry becouse i answer with out reading your instructions before comit. tks for your time i hope this matehematical framework works to ypu guys. my best regards Eduardo Nava Hernandez
(Lalo)

[TomOleDiem]

Can you please make the comments in the files english.

[naype888-cloud]

Can you please make the comments in the files english.

Dear Tom, done i all ready translate all the coments inside the file, idk if Joseph or some body all ready catch the point here, mmmm maybe the best aproaching becomes if think abouth the electron insithe the atom, where the theorem it's saying abouth the electron it's very very clear, you can get a perfect exact value from A variable if you only chose that one, if you choose B then you get a perfect info from B meassure becomes, so what you never be abble to get perfectly it's sharp bougth at the same time with out an irreductible gap, in other wise the only one thing you can know perfectly or exact when you try to meassuare or refine A same time B, the only one perfect determinate value it's the defect itself, how many info you never gone a get exactly at same time...that the algebraic thefect exactly means...

[jstoobysmith]

Closeness as it currently does not meet our standards, and we do not put detailed reviews into PhyslibAlpha.