IndisputableMonolith.Gravity.SevenGaps.CapShellBridge

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker
   3
   4/-!
   5# Seven Gaps, P2.3: the capped-quotient to exact-shell carrier bridge
   6
   7This module constructs the missing carrier equivalence behind
   8`ZqContinuumBlocker.CapShellCompatibility`.
   9
  10At cap `B`, a bounded complex has a unique exact complexity
  11`max nV (max nE nT) ≤ B`.  Conversely, an exact complex in shell `n ≤ B`
  12becomes a bounded complex by reattaching the three cap proofs.  Both maps
  13carry the original incidence data and relabeling witnesses.  They therefore
  14descend to the two quotient carriers and are inverse there.
  15
  16The bridge preserves automorphism cardinality and hence the `1 / |Aut|`
  17class measure.  An arbitrary exact-shell phase transports to a `PhaseModel`
  18at every cap.  Reindexing the finite quotient sum along the carrier
  19equivalence then proves the required equality with
  20`exactComplexityCutoff phase B`, whose shell range is `B + 1`.
  21
  22No target sum equality, convergence statement, substrate phase, or physical
  23continuum interpretation is assumed.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace SevenGaps
  29namespace CapShellBridge
  30
  31open PathSumMeasure
  32open QuotientFirstZ
  33open ExactShellGaugeUV
  34open ZqPhaseStructure
  35open ZqContinuumBlocker
  36
  37noncomputable section
  38
  39/-! ## 1. The labeled carrier maps -/
  40
  41/-- The exact shells whose complexity is at most `B`.  The outer
  42`Fin (B + 1)` is the off-by-one-safe carrier for shell indices `0, ..., B`. -/
  43abbrev ShellsUpTo (B : ℕ) : Type :=
  44  Σ n : Fin (B + 1), ExactPathClass n
  45
  46noncomputable local instance instFintypeTriangulationClass (B : ℕ) :
  47    Fintype (TriangulationClass B) :=
  48  Fintype.ofFinite _
  49
  50/-- A bounded complex's exact complexity, packaged as an index in
  51`Fin (B + 1)`. -/
  52def boundedShellIndex {B : ℕ} (K : BoundedComplex B) : Fin (B + 1) :=
  53  ⟨complexity K, Nat.lt_succ_of_le (max_le K.hV (max_le K.hE K.hT))⟩
  54
  55/-- The exact signature carried by a bounded complex. -/
  56def boundedShellSig {B : ℕ} (K : BoundedComplex B) : ShellSig (complexity K) :=
  57  ⟨(⟨K.nV, Nat.lt_succ_of_le (Nat.le_max_left _ _)⟩,
  58    ⟨K.nE, Nat.lt_succ_of_le
  59      (le_trans (Nat.le_max_left _ _) (Nat.le_max_right _ _))⟩,
  60    ⟨K.nT, Nat.lt_succ_of_le
  61      (le_trans (Nat.le_max_right _ _) (Nat.le_max_right _ _))⟩), rfl⟩
  62
  63/-- Forward labeled map: forget the cap proofs, retain the exact signature
  64and incidence data, then enter the exact relabeling quotient. -/
  65def boundedToShell {B : ℕ} (K : BoundedComplex B) : ShellsUpTo B :=
  66  ⟨boundedShellIndex K, boundedShellSig K,
  67    Quotient.mk _ (toExact K)⟩
  68
  69/-- Backward labeled map: attach a cap `B` to an exact complex whose shell
  70index is at most `B`. -/
  71def exactToBounded {B n : ℕ} (hn : n ≤ B) (s : ShellSig n)
  72    (K : ExactComplex (sigV s) (sigE s) (sigT s)) : BoundedComplex B where
  73  nV := sigV s
  74  nE := sigE s
  75  nT := sigT s
  76  hV := le_trans (Nat.le_of_lt_succ s.1.1.isLt) hn
  77  hE := le_trans (Nat.le_of_lt_succ s.1.2.1.isLt) hn
  78  hT := le_trans (Nat.le_of_lt_succ s.1.2.2.isLt) hn
  79  edgeVerts := K.edgeVerts
  80  tetVerts := K.tetVerts
  81
  82/-- An exact relabeling remains a bounded relabeling after cap proofs are
  83attached. -/
  84def exactRelabelToBounded {B n : ℕ} (hn : n ≤ B) (s : ShellSig n)
  85    {K K' : ExactComplex (sigV s) (sigE s) (sigT s)}
  86    (r : ExactRelabel K K') :
  87    Relabel (exactToBounded hn s K) (exactToBounded hn s K') where
  88  vEquiv := r.vEquiv
  89  eEquiv := r.eEquiv
  90  tEquiv := r.tEquiv
  91  edge_comm := r.edge_comm
  92  tet_comm := r.tet_comm
  93
  94/-- The backward map on one exact-signature quotient. -/
  95def exactClassToCap {B n : ℕ} (hn : n ≤ B) (s : ShellSig n) :
  96    Quotient (exactSetoid (sigV s) (sigE s) (sigT s)) →
  97      TriangulationClass B :=
  98  Quotient.lift
  99    (fun K => Quotient.mk _ (exactToBounded hn s K))
 100    (fun _K _K' h => Quotient.sound <|
 101      h.elim fun r => ⟨exactRelabelToBounded hn s r⟩)
 102
 103/-- Backward map on the full disjoint union of exact shells through `B`. -/
 104def shellToCap {B : ℕ} (x : ShellsUpTo B) : TriangulationClass B :=
 105  exactClassToCap (Nat.le_of_lt_succ x.1.isLt) x.2.1 x.2.2
 106
 107/-! ## 2. Descent to quotients and inverse laws -/
 108
 109/-- The forward labeled map respects bounded relabeling. -/
 110theorem boundedToShell_congr {B : ℕ} {K K' : BoundedComplex B}
 111    (h : Equivalent K K') : boundedToShell K = boundedToShell K' := by
 112  rcases K with ⟨v, e, t, hV, hE, hT, edgeVerts, tetVerts⟩
 113  rcases K' with ⟨v', e', t', hV', hE', hT', edgeVerts', tetVerts'⟩
 114  obtain ⟨r⟩ := h
 115  have hv : v = v' := relabel_nV_eq r
 116  have he : e = e' := relabel_nE_eq r
 117  have ht : t = t' := relabel_nT_eq r
 118  cases hv
 119  cases he
 120  cases ht
 121  have hVproof : hV = hV' := Subsingleton.elim _ _
 122  have hEproof : hE = hE' := Subsingleton.elim _ _
 123  have hTproof : hT = hT' := Subsingleton.elim _ _
 124  cases hVproof
 125  cases hEproof
 126  cases hTproof
 127  apply Sigma.ext
 128  · rfl
 129  exact heq_of_eq <| by
 130    apply Sigma.ext
 131    · rfl
 132    exact heq_of_eq <| Quotient.sound ⟨{
 133      vEquiv := r.vEquiv
 134      eEquiv := r.eEquiv
 135      tEquiv := r.tEquiv
 136      edge_comm := r.edge_comm
 137      tet_comm := r.tet_comm }⟩
 138
 139/-- Forward map on bounded quotient classes. -/
 140def capToShell {B : ℕ} : TriangulationClass B → ShellsUpTo B :=
 141  Quotient.lift boundedToShell (fun _K _K' h => boundedToShell_congr h)
 142
 143/-- Attaching a cap after forgetting it returns the original bounded class. -/
 144theorem shellToCap_boundedToShell {B : ℕ} (K : BoundedComplex B) :
 145    shellToCap (boundedToShell K) =
 146      Quotient.mk (relabelSetoid B) K := by
 147  apply Quotient.sound
 148  exact ⟨{
 149    vEquiv := Equiv.refl _
 150    eEquiv := Equiv.refl _
 151    tEquiv := Equiv.refl _
 152    edge_comm := by
 153      intro e
 154      change K.edgeVerts e =
 155        Prod.map (Equiv.refl _) (Equiv.refl _) (K.edgeVerts e)
 156      cases K.edgeVerts e
 157      rfl
 158    tet_comm := by
 159      intro t i
 160      rfl }⟩
 161
 162/-- Forgetting the cap after attaching it returns the original exact-shell
 163class.  Proof fields disappear by proof irrelevance; incidence data is
 164unchanged. -/
 165theorem boundedToShell_exactToBounded {B n : ℕ} (hn : n ≤ B)
 166    (s : ShellSig n) (K : ExactComplex (sigV s) (sigE s) (sigT s)) :
 167    boundedToShell (exactToBounded hn s K) =
 168      ⟨⟨n, Nat.lt_succ_of_le hn⟩, s, Quotient.mk _ K⟩ := by
 169  rcases s with ⟨⟨v, e, t⟩, hs⟩
 170  rcases v with ⟨v, hv⟩
 171  rcases e with ⟨e, he⟩
 172  rcases t with ⟨t, ht⟩
 173  dsimp only [sigV, sigE, sigT] at K ⊢
 174  dsimp only at hs
 175  subst n
 176  simp [boundedToShell, boundedShellIndex, boundedShellSig, exactToBounded,
 177    sigV, sigE, sigT, complexity]
 178  exact Quotient.sound ⟨ExactRelabel.refl K⟩
 179
 180/-- Right inverse law on exact-shell quotient classes. -/
 181theorem capToShell_shellToCap {B : ℕ} (x : ShellsUpTo B) :
 182    capToShell (shellToCap x) = x := by
 183  rcases x with ⟨⟨n, hn⟩, s, q⟩
 184  refine Quotient.inductionOn q ?_
 185  intro K
 186  exact boundedToShell_exactToBounded (Nat.le_of_lt_succ hn) s K
 187
 188/-- Left inverse law on bounded quotient classes. -/
 189theorem shellToCap_capToShell {B : ℕ} (q : TriangulationClass B) :
 190    shellToCap (capToShell q) = q := by
 191  refine Quotient.inductionOn q ?_
 192  intro K
 193  exact shellToCap_boundedToShell K
 194
 195/-- **HEADLINE CARRIER EQUIVALENCE.**  Bounded quotient classes at cap `B`
 196are exactly the disjoint union of exact quotient shells `0, ..., B`. -/
 197def capShellEquiv (B : ℕ) : TriangulationClass B ≃ ShellsUpTo B where
 198  toFun := capToShell
 199  invFun := shellToCap
 200  left_inv := shellToCap_capToShell
 201  right_inv := capToShell_shellToCap
 202
 203/-! ## 3. Automorphism cardinality and measure preservation -/
 204
 205/-- Bounded automorphisms and exact automorphisms of the cap-forgotten
 206complex carry exactly the same relabeling data. -/
 207def autEquivToExact {B : ℕ} (K : BoundedComplex B) :
 208    Aut K ≃ ExactAut (toExact K) where
 209  toFun r :=
 210    { vEquiv := r.vEquiv
 211      eEquiv := r.eEquiv
 212      tEquiv := r.tEquiv
 213      edge_comm := r.edge_comm
 214      tet_comm := r.tet_comm }
 215  invFun r :=
 216    { vEquiv := r.vEquiv
 217      eEquiv := r.eEquiv
 218      tEquiv := r.tEquiv
 219      edge_comm := r.edge_comm
 220      tet_comm := r.tet_comm }
 221  left_inv r := Relabel.ext rfl rfl rfl
 222  right_inv r := ExactRelabel.ext rfl rfl rfl
 223
 224/-- **AUTOMORPHISM-CARDINALITY PRESERVATION.** -/
 225theorem autCard_toExact {B : ℕ} (K : BoundedComplex B) :
 226    Nat.card (Aut K) = Nat.card (ExactAut (toExact K)) :=
 227  Nat.card_congr (autEquivToExact K)
 228
 229/-- The labeled symmetry-factor measures agree under cap forgetting. -/
 230theorem mu_eq_exactMu_toExact {B : ℕ} (K : BoundedComplex B) :
 231    mu K = exactMu (toExact K) := by
 232  unfold mu exactMu
 233  rw [autCard_toExact K]
 234
 235/-- Automorphism cardinality of a represented exact-shell class. -/
 236noncomputable def shellAutCard {n : ℕ} (c : ExactPathClass n) : ℕ :=
 237  Nat.card (ExactAut (Quotient.out c.2))
 238
 239/-- **QUOTIENT-LEVEL AUTOMORPHISM PRESERVATION.** -/
 240theorem shellAutCard_capToShell {B : ℕ} (q : TriangulationClass B) :
 241    shellAutCard (capToShell q).2 = Nat.card (Aut (Quotient.out q)) := by
 242  refine Quotient.inductionOn q ?_
 243  intro K
 244  let qe := Quotient.mk (exactSetoid K.nV K.nE K.nT) (toExact K)
 245  have hrel : GlobalEquivalent (Quotient.out qe) (toExact K) :=
 246    Quotient.exact (Quotient.out_eq qe)
 247  obtain ⟨r⟩ := hrel
 248  have hcap : Equivalent
 249      (Quotient.out (Quotient.mk (relabelSetoid B) K)) K :=
 250    PathSum.equivalent_of_mk_eq
 251      (Quotient.out_eq (Quotient.mk (relabelSetoid B) K))
 252  obtain ⟨s⟩ := hcap
 253  dsimp [capToShell, boundedToShell, shellAutCard]
 254  calc
 255    Nat.card (ExactAut (Quotient.out qe))
 256        = Nat.card (ExactAut (toExact K)) := Nat.card_congr r.autCongr
 257    _ = Nat.card (Aut K) := (autCard_toExact K).symm
 258    _ = Nat.card (Aut (Quotient.out (Quotient.mk (relabelSetoid B) K))) :=
 259        (Nat.card_congr s.autCongr).symm
 260
 261/-- **QUOTIENT-LEVEL MEASURE PRESERVATION.**  The class measure on the
 262exact-shell image is the capped representative measure. -/
 263theorem classMu_capToShell {B : ℕ} (q : TriangulationClass B) :
 264    classMu (capToShell q).2 = mu (Quotient.out q) := by
 265  refine Quotient.inductionOn q ?_
 266  intro K
 267  let qe := Quotient.mk (exactSetoid K.nV K.nE K.nT) (toExact K)
 268  have hrel : GlobalEquivalent (Quotient.out qe) (toExact K) :=
 269    Quotient.exact (Quotient.out_eq qe)
 270  have hcap : Equivalent
 271      (Quotient.out (Quotient.mk (relabelSetoid B) K)) K :=
 272    PathSum.equivalent_of_mk_eq
 273      (Quotient.out_eq (Quotient.mk (relabelSetoid B) K))
 274  dsimp [capToShell, boundedToShell, classMu]
 275  show classMuOn K.nV K.nE K.nT qe =
 276    mu (Quotient.out (Quotient.mk (relabelSetoid B) K))
 277  rw [RegulatorRemovalNoGo.classMuOn_out qe]
 278  calc
 279    exactMu (Quotient.out qe) = exactMu (toExact K) := exactMu_congr hrel
 280    _ = mu K := (mu_eq_exactMu_toExact K).symm
 281    _ = mu (Quotient.out (Quotient.mk (relabelSetoid B) K)) :=
 282        (mu_congr hcap).symm
 283
 284/-! ## 4. Transport of arbitrary exact-shell phases -/
 285
 286/-- Transport an arbitrary phase on exact shells to the labeled bounded
 287carrier at cap `B`. -/
 288def phaseModelAtCap
 289    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) : PhaseModel B where
 290  phase K := phase (boundedToShell K).1 (boundedToShell K).2
 291  invariant K K' h := by rw [boundedToShell_congr h]
 292
 293/-- The transported phase descends to exactly the original phase after the
 294carrier equivalence. -/
 295theorem classPhase_phaseModelAtCap
 296    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) {B : ℕ}
 297    (q : TriangulationClass B) :
 298    classPhase (phaseModelAtCap phase B) q =
 299      phase (capToShell q).1 (capToShell q).2 := by
 300  refine Quotient.inductionOn q ?_
 301  intro K
 302  rfl
 303
 304/-- The transported phase model at every cap. -/
 305def capPhaseFamily
 306    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) : CapPhaseFamily :=
 307  fun B => phaseModelAtCap phase B
 308
 309/-! ## 5. Finite-sum reindexing and compatibility -/
 310
 311/-- A sum over `Fin N` is the corresponding natural-number range sum. -/
 312theorem sum_fin_eq_sum_range {α : Type*} [AddCommMonoid α]
 313    (f : ℕ → α) (N : ℕ) :
 314    (∑ i : Fin N, f i) = ∑ i ∈ Finset.range N, f i := by
 315  induction N with
 316  | zero => simp
 317  | succ N ih =>
 318      calc
 319        (∑ i : Fin (N + 1), f i)
 320            = (∑ i : Fin N, f i) + f N := by
 321                simpa using Fin.sum_univ_castSucc
 322                  (f := fun i : Fin (N + 1) => f i)
 323        _ = (∑ i ∈ Finset.range N, f i) + f N := by rw [ih]
 324        _ = ∑ i ∈ Finset.range (N + 1), f i := by
 325              rw [Finset.sum_range_succ]
 326
 327/-- Splitting the disjoint-union carrier gives exactly the shell cutoff
 328through `B`; the range is `B + 1`, so shell `B` is included. -/
 329theorem sum_shellsUpTo_eq_exactComplexityCutoff
 330    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
 331    (∑ x : ShellsUpTo B,
 332      (classMu x.2 : ℂ) *
 333        Complex.exp (Complex.I * (phase x.1 x.2 : ℂ))) =
 334      exactComplexityCutoff phase B := by
 335  rw [Fintype.sum_sigma]
 336  change (∑ n : Fin (B + 1), exactShellAmplitude phase n) =
 337    ∑ n ∈ Finset.range (B + 1), exactShellAmplitude phase n
 338  exact sum_fin_eq_sum_range (exactShellAmplitude phase) (B + 1)
 339
 340/-- **HEADLINE FINITE-SUM REINDEXING.**  The phased capped quotient sum
 341transported from any exact-shell phase equals its exact-shell cutoff through
 342shell `B`. -/
 343theorem phasedZq_eq_exactComplexityCutoff
 344    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
 345    phasedZqSequence (capPhaseFamily phase) B =
 346      exactComplexityCutoff phase B := by
 347  unfold phasedZqSequence
 348  change Zq B (phasedWeight (phaseModelAtCap phase B)) =
 349    exactComplexityCutoff phase B
 350  rw [Zq]
 351  calc
 352    (∑ q : TriangulationClass B,
 353      (mu (Quotient.out q) : ℂ) *
 354        phasedWeight (phaseModelAtCap phase B) q)
 355        = ∑ x : ShellsUpTo B,
 356            (classMu x.2 : ℂ) *
 357              Complex.exp (Complex.I * (phase x.1 x.2 : ℂ)) := by
 358            apply Fintype.sum_equiv (capShellEquiv B)
 359            intro q
 360            change (mu (Quotient.out q) : ℂ) *
 361                phasedWeight (phaseModelAtCap phase B) q =
 362              (classMu (capToShell q).2 : ℂ) *
 363                Complex.exp (Complex.I * (phase (capToShell q).1 (capToShell q).2 : ℂ))
 364            rw [classMu_capToShell]
 365            simp only [phasedWeight, classPhase_phaseModelAtCap]
 366    _ = exactComplexityCutoff phase B :=
 367      sum_shellsUpTo_eq_exactComplexityCutoff phase B
 368
 369/-- **P2.3 CLOSER.**  Every exact-shell phase has a canonically transported
 370capped phase family satisfying the previously missing
 371`ZqContinuumBlocker.CapShellCompatibility`. -/
 372theorem capShellCompatibility
 373    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
 374    CapShellCompatibility (capPhaseFamily phase) phase :=
 375  ⟨phasedZq_eq_exactComplexityCutoff phase⟩
 376
 377#print axioms capShellEquiv
 378#print axioms autCard_toExact
 379#print axioms shellAutCard_capToShell
 380#print axioms classMu_capToShell
 381#print axioms phasedZq_eq_exactComplexityCutoff
 382#print axioms capShellCompatibility
 383
 384end
 385
 386end CapShellBridge
 387end SevenGaps
 388end Gravity
 389end IndisputableMonolith
 390