feat(PhyslibAlpha): finite path dimensional uncertainty chain

.codespellignore

@@ -20,3 +20,13 @@ hTe
 hSA
 hsI
 hax
+admisible
+argumentos
+doble
+fase
+imposible
+ortogonal
+pares
+posible
+ser
+vectores

PhyslibAlpha.lean

@@ -99,6 +99,24 @@ public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.SpectralMeasure
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Stinespring.Kernel
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Stinespring.Dilation
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.Uncertainty
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimensionalUncertainty
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D8_Szego
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D9_Monotonia
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D10_Certificado
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D11_CuantoMinimoArea
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D12_Trace
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D13_FirstBreak
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D14_SzegoExcess
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D15_Cosecant
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D0_Habitat
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D1_CauchyGram
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D2_Robertson
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D3_GrafoCamino
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D4_PorQueNoDiagonal
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D5_MaximaTension
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D6_Fiedler
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D7_Niven
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathSpectralGap
 public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Basic
 public import PhyslibAlpha.AlgebraicFramework.WStarAlgebra.ConjSpace
 public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.Dynamics.Automorphism
@@ -229,4 +247,5 @@ public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanStatistics
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanPositivity
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanCFC
 public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanSpecial
+public import PhyslibAlpha.AlgebraicFramework.InformationGeometry.FisherRao
 public import PhyslibAlpha.Relativity.General.Schwarzschild.IncompressibleSphere

PhyslibAlpha/AlgebraicFramework/CStarAlgebra/DimUncertainty/D10_Certificado.lean

@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2026 Eduardo Nava-Hernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava Gómez
+-/
+module
+
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D6_Fiedler
+public import PhyslibAlpha.AlgebraicFramework.HilbertSpace.PathGap.D7_Niven
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D8_Szego
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D9_Monotonia
+
+/-!
+# D10 — Joint certificate: Fiedler + Niven + Szegő in `H_d`
+
+Gathers, in a single citable certificate, the three pillars that rest on
+the common habitat `H_d = ℂ^d` (`D0_Habitat.lean`): the Fiedler spectral
+decomposition (`D6_Fiedler.lean`), the Niven theorem (`D7_Niven.lean`),
+and the Szegő limit with gap positivity (`D8_Szego.lean`). This is the
+terminal theorem of the package: the mathematics proved in this
+repository ends here.
+
+# Shielding `δ_geom(d)` in the finite Hilbert space `H_d`
+
+**Habitat:** \(H_d=\mathtt{EuclideanSpace}\,\mathbb{C}\,(\mathtt{Fin}\,d)\).
+This space is never left: it is where the framework derivation lives.
+
+**Shield triad** (all on the discrete setting):
+
+| Shield | Lean content |
+|--------|-------------|
+| **Fiedler** | fundamental mode / `KdOp` / spectral radius in \(H_d\) |
+| **Niven** | `saturacion_iff` + `no_reposición_saturacion_camino` + `deltaGeom_pos_of_four_le` |
+| **Szegő** | `limite_szego_CNava` + `deltaInf_pos` + ∞ is not a dimension |
+| **Monotonicity** | `deltaGeom_four_le`: `δ_geom(4)` is the global floor for all `d ≥ 4` |
+
+Reading: the simultaneously rational trigonometric products of path
+saturation **only** exist at \(d\in\{2,3\}\). There are no more seeds;
+that is why **nothing restores the unit bound** after \(d=4\).
+Moreover, certified monotonicity pins \(d=4\) as the smallest realized
+defect: any measurement in a physical \(H_d\) with \(d\ge4\) is
+separated from zero by at least \(\delta_{\rm geom}(4)\). As the finite
+family grows, the defect does not vanish: it converges to
+\(\delta_\infty>0\).
+
+**Habitat closure:** \(H_d = \mathbb{C}^d \cong \mathbb{R}^{2d}\), finite.
+Period. For continuous infinite, this is not a hotel — \(d=\infty\) is not
+hosted in this package; at most one sees it arriving through the window as
+a limit (`D8_Szego.lean`), but it never crosses the door.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open Real
+open Filter
+open scoped Topology
+
+namespace BlindajeHd
+
+open TransportePosicion
+open Gnomon
+
+/-! ## Habitat: stays within \(H_d\) -/
+
+/-- Predicate recording that the entire construction remains in the finite Hilbert space `Hd d`. -/
+def HabitatHilbertFinito (d : ℕ) : Prop :=
+  Hd d = EuclideanSpace ℂ (Fin d)
+
+theorem habitatHilbertFinito (d : ℕ) : HabitatHilbertFinito d :=
+  Hd_eq_euclidean d
+
+theorem infinito_no_es_habitat :
+    Tendsto deltaGeom atTop (𝓝 deltaInf) ∧
+      deltaInf = Cinf - 1 ∧
+      0 < deltaInf :=
+  infinito_no_es_dimension_sino_limite
+
+/-! ## Niven: the unit bound does not recover -/
+
+theorem niven_saturacion_solo_semillas (d : ℕ) (hd : 2 ≤ d) :
+    cos (π / (d + 1)) ^ 2 = ((d : ℝ) - 1) / 4 ↔ d = 2 ∨ d = 3 :=
+  saturacion_iff d hd
+
+/-- **Nothing restores the bound** after \(d=4\). -/
+theorem niven_cota_unitaria_no_se_repone (d : ℕ) (hd : 4 ≤ d) :
+    cos (π / (d + 1)) ^ 2 ≠ ((d : ℝ) - 1) / 4 :=
+  no_reposición_saturacion_camino d hd
+
+theorem niven_deltaGeom_pos_en_Hd (d : ℕ) (hd : 4 ≤ d) :
+    0 < deltaGeom d :=
+  deltaGeom_pos_of_four_le d hd
+
+theorem piso_precision_deltaGeom_d4_en_Hd (d : ℕ) (hd : 4 ≤ d) :
+    deltaGeom 4 ≤ deltaGeom d :=
+  deltaGeom_four_le d hd
+
+/-- In the finite physical regime `H_d`, `d ≥ 4`, no reading has defect
+below the elementary floor `δ_geom(4)`. -/
+theorem no_medicion_absoluta_bajo_piso_d4_en_Hd
+    (d : ℕ) (hd : 4 ≤ d) (ε : ℝ) (hε : ε < deltaGeom 4) :
+    ε < deltaGeom d :=
+  lt_of_lt_of_le hε (piso_precision_deltaGeom_d4_en_Hd d hd)
+
+/-! ## Fiedler: spectrum and band in \(H_d\) -/
+
+theorem fiedler_autovector_en_Hd (d : ℕ) (hd : 2 ≤ d) :
+    KdOp d (vectorFiedlerExplicito d) =
+      ((2 / ((d : ℝ) - 1) : ℝ) : ℂ) • vectorFiedlerExplicito d :=
+  KdOp_vectorFiedlerExplicito d hd
+
+theorem fiedler_radio_banda (d : ℕ) (hd : 2 ≤ d) :
+    letI : Nonempty (Fin d) := ⟨⟨0, by omega⟩⟩
+    letI : Nontrivial (Hd d) := inferInstance
+    ConstructorEspectralTP.radioEspectral (KdOp d) (KdOp_simetrico d) =
+      2 / ((d : ℝ) - 1) := by
+  letI : Nonempty (Fin d) := ⟨⟨0, by omega⟩⟩
+  letI : Nontrivial (Hd d) := inferInstance
+  exact radioEspectral_KdOp_eq_paso d hd
+
+/-! ## Szegő: asymptotics of the finite family -/
+
+theorem szego_limite_familia_finita :
+    Tendsto CNava atTop (𝓝 Cinf) :=
+  limite_szego_CNava
+
+theorem szego_deltaInf_pos : 0 < deltaInf :=
+  deltaInf_pos
+
+theorem defecto_real_positivo_desde_Hd4_hasta_limite :
+    (∀ d : ℕ, 4 ≤ d → 0 < deltaGeom d) ∧
+      Tendsto deltaGeom atTop (𝓝 deltaInf) ∧
+      0 < deltaInf :=
+  ⟨niven_deltaGeom_pos_en_Hd, limite_defecto_geometrico, szego_deltaInf_pos⟩
+
+/-! ## Joint citable certificate -/
+
+/-- Joint certificate collecting the finite habitat, saturation classification, and positive gap. -/
+structure CertificadoBlindajeHd where
+  habitat : ∀ d : ℕ, HabitatHilbertFinito d
+  niven_iff :
+    ∀ d : ℕ, 2 ≤ d →
+      (cos (π / ((d : ℝ) + 1)) ^ 2 = ((d : ℝ) - 1) / 4 ↔ d = 2 ∨ d = 3)
+  niven_no_reposición :
+    ∀ d : ℕ, 4 ≤ d →
+      cos (π / ((d : ℝ) + 1)) ^ 2 ≠ ((d : ℝ) - 1) / 4
+  deltaGeom_pos : ∀ d : ℕ, 4 ≤ d → 0 < deltaGeom d
+  deltaGeom_piso_d4 : ∀ d : ℕ, 4 ≤ d → deltaGeom 4 ≤ deltaGeom d
+  fiedler_autovector :
+    ∀ d : ℕ, 2 ≤ d →
+      KdOp d (vectorFiedlerExplicito d) =
+        ((2 / ((d : ℝ) - 1) : ℝ) : ℂ) • vectorFiedlerExplicito d
+  szego_limite : Tendsto CNava atTop (𝓝 Cinf)
+  szego_deltaInf : 0 < deltaInf
+  defecto_real_positivo :
+    (∀ d : ℕ, 4 ≤ d → 0 < deltaGeom d) ∧
+      Tendsto deltaGeom atTop (𝓝 deltaInf) ∧
+      0 < deltaInf
+  infinito_limite :
+    Tendsto deltaGeom atTop (𝓝 deltaInf) ∧
+      deltaInf = Cinf - 1 ∧ 0 < deltaInf
+
+theorem certificadoBlindajeHd_OK : Nonempty CertificadoBlindajeHd :=
+  ⟨{ habitat := habitatHilbertFinito
+     niven_iff := fun d hd => niven_saturacion_solo_semillas d hd
+     niven_no_reposición := fun d hd => niven_cota_unitaria_no_se_repone d hd
+     deltaGeom_pos := fun d hd => niven_deltaGeom_pos_en_Hd d hd
+     deltaGeom_piso_d4 := fun d hd => piso_precision_deltaGeom_d4_en_Hd d hd
+     fiedler_autovector := fun d hd => fiedler_autovector_en_Hd d hd
+     szego_limite := szego_limite_familia_finita
+     szego_deltaInf := szego_deltaInf_pos
+     defecto_real_positivo := defecto_real_positivo_desde_Hd4_hasta_limite
+     infinito_limite := infinito_no_es_habitat }⟩
+
+end BlindajeHd

PhyslibAlpha/AlgebraicFramework/CStarAlgebra/DimUncertainty/D11_CuantoMinimoArea.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Eduardo Nava-Hernández. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eduardo Nava-Hernández, José Arturo Nava-Hernández, Gerardo Gabriel Nava Gómez
+-/
+module
+
+public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.DimUncertainty.D10_Certificado
+
+/-!
+# D11 — Elementary quantum of area
+
+This module brings to Lean the strictly mathematical reading of the
+elementary quantum:
+
+* `deltaGeom 4` is the first positive linear defect of the `d ≥ 4` tail.
+* `deltaGeom 4 ^ 2` is the first elementary quantum of area.
+* By monotonicity, no area resolution realized in `H_d`, `d ≥ 4`,
+  falls below that quantum.
+
+No physical units, baryons, or Planck scale are introduced. To attach
+an external unit later, it suffices to multiply by a nonnegative scale:
+the bound survives by order.
+
+The mathematical dependency is the package chain:
+Cauchy--Gram → Robertson--Schrödinger → `T_d/P_d` instance →
+Niven/Szegő/monotonicity. It does not modify Robertson 1929; it uses
+it as an anchor and derives the area floor from its discrete realization.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace CuantoMinimoArea
+
+open Gnomon
+
+/-- Elementary quantum of area of the `H_d` tail, `d ≥ 4`. -/
+def cuantoCuanticoElemental : ℝ :=
+  deltaGeom 4 ^ 2
+
+/-- Operational alias: the minimum "small square" is the elementary quantum. -/
+def cuadritoMinimo : ℝ :=
+  cuantoCuanticoElemental
+
+/-- Resolution area induced by the geometric defect in `H_d`. -/
+def areaResolucionHd (d : ℕ) : ℝ :=
+  deltaGeom d ^ 2
+
+/-- The citable name and the operational alias are the same quantity. -/
+theorem cuadritoMinimo_eq_cuantoCuanticoElemental :
+    cuadritoMinimo = cuantoCuanticoElemental := by
+  rfl
+
+/-- The "small square" is exactly the area resolution in `H_4`. -/
+theorem cuadritoMinimo_eq_areaResolucionH4 :
+    cuadritoMinimo = areaResolucionHd 4 := by
+  rfl
+
+/-- The elementary quantum is exactly the area resolution in `H_4`. -/
+theorem cuantoCuanticoElemental_eq_areaResolucionH4 :
+    cuantoCuanticoElemental = areaResolucionHd 4 := by
+  rfl
+
+/-- The elementary quantum of area is strictly positive. -/
+theorem cuantoCuanticoElemental_pos : 0 < cuantoCuanticoElemental := by
+  unfold cuantoCuanticoElemental
+  have hδ : 0 < deltaGeom 4 :=
+    deltaGeom_pos_of_four_le 4 (by omega)
+  positivity
+
+/-- Positivity alias for the operational name. -/
+theorem cuadritoMinimo_pos : 0 < cuadritoMinimo := by
+  simpa [cuadritoMinimo] using cuantoCuanticoElemental_pos
+
+/-- Every resolution area in `H_d`, `d ≥ 4`, lies above the quantum. -/
+theorem cuantoCuanticoElemental_le_areaResolucionHd (d : ℕ) (hd : 4 ≤ d) :
+    cuantoCuanticoElemental ≤ areaResolucionHd d := by
+  unfold cuantoCuanticoElemental areaResolucionHd
+  exact deltaGeom_sq_four_le d hd
+
+/-- Every resolution area in `H_d`, `d ≥ 4`, lies above the small square. -/
+theorem cuadritoMinimo_le_areaResolucionHd (d : ℕ) (hd : 4 ≤ d) :
+    cuadritoMinimo ≤ areaResolucionHd d := by
+  simpa [cuadritoMinimo] using cuantoCuanticoElemental_le_areaResolucionHd d hd
+
+/-- No realized resolution in `H_d`, `d ≥ 4`, is strictly less than the
+elementary quantum. -/
+theorem no_hay_resolucion_menor_que_cuanto_cuantico
+    (d : ℕ) (hd : 4 ≤ d) :
+    ¬ areaResolucionHd d < cuantoCuanticoElemental := by
+  exact not_lt.mpr (cuantoCuanticoElemental_le_areaResolucionHd d hd)
+
+/-- Operational alias: no resolution is less than the minimum small square. -/
+theorem no_hay_resolucion_menor_que_cuadrito
+    (d : ℕ) (hd : 4 ≤ d) :
+    ¬ areaResolucionHd d < cuadritoMinimo := by
+  simpa [cuadritoMinimo] using no_hay_resolucion_menor_que_cuanto_cuantico d hd
+
+/-- Any threshold below the small square falls below every realized
+resolution in the `d ≥ 4` tail. -/
+theorem umbral_bajo_cuadrito_no_alcanza_Hd
+    (d : ℕ) (hd : 4 ≤ d) (ε : ℝ) (hε : ε < cuadritoMinimo) :
+    ε < areaResolucionHd d :=
+  lt_of_lt_of_le hε (cuadritoMinimo_le_areaResolucionHd d hd)
+
+/-- Applying a nonnegative external scale preserves the minimum bound. -/
+theorem escala_no_negativa_conserva_cuanto_cuantico
+    (escala : ℝ) (hesc : 0 ≤ escala) (d : ℕ) (hd : 4 ≤ d) :
+    escala * cuantoCuanticoElemental ≤ escala * areaResolucionHd d :=
+  mul_le_mul_of_nonneg_left (cuantoCuanticoElemental_le_areaResolucionHd d hd) hesc
+
+/-- Operational alias for the nonnegative external scale. -/
+theorem escala_no_negativa_conserva_cuadrito
+    (escala : ℝ) (hesc : 0 ≤ escala) (d : ℕ) (hd : 4 ≤ d) :
+    escala * cuadritoMinimo ≤ escala * areaResolucionHd d := by
+  simpa [cuadritoMinimo] using escala_no_negativa_conserva_cuanto_cuantico escala hesc d hd
+
+/-- With a positive external scale, the scaled quantum remains strictly
+positive. -/
+theorem cuanto_cuantico_escalado_pos
+    (escala : ℝ) (hesc : 0 < escala) :
+    0 < escala * cuantoCuanticoElemental :=
+  mul_pos hesc cuantoCuanticoElemental_pos
+
+/-- Operational alias: with a positive scale, the scaled small square
+remains strictly positive. -/
+theorem cuadrito_escalado_pos
+    (escala : ℝ) (hesc : 0 < escala) :
+    0 < escala * cuadritoMinimo := by
+  simpa [cuadritoMinimo] using cuanto_cuantico_escalado_pos escala hesc
+
+/-- Citable certificate for the elementary quantum of area. -/
+structure CertificadoCuantoMinimoArea where
+  cuanto_pos : 0 < cuantoCuanticoElemental
+  area_minima : ∀ d : ℕ, 4 ≤ d → cuantoCuanticoElemental ≤ areaResolucionHd d
+  no_menor : ∀ d : ℕ, 4 ≤ d → ¬ areaResolucionHd d < cuantoCuanticoElemental
+  escala_conserva :
+    ∀ escala : ℝ, 0 ≤ escala →
+      ∀ d : ℕ, 4 ≤ d →
+        escala * cuantoCuanticoElemental ≤ escala * areaResolucionHd d
+
+theorem certificadoCuantoMinimoArea_OK :
+    Nonempty CertificadoCuantoMinimoArea :=
+  ⟨{ cuanto_pos := cuantoCuanticoElemental_pos
+     area_minima := cuantoCuanticoElemental_le_areaResolucionHd
+     no_menor := no_hay_resolucion_menor_que_cuanto_cuantico
+     escala_conserva := escala_no_negativa_conserva_cuanto_cuantico }⟩
+
+end CuantoMinimoArea