IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation
   3
   4/-!
   5# Gap 2 / A18: label erasure Jacobian (lane C4)
   6
   7## Scoped headline (exact shape; flag 8 unmoved)
   8
   9mu is the pushforward of a local relabeling-invariant labeled weight; 1/|Aut| is the
  10erasure Jacobian; the surviving freedom is the local numerator and three fugacities.
  11
  12This module does **not** assert flag 8 closed.  Flag 8 moves only on G1∧G2 PASS plus later
  13fugacity elimination plus numerator triviality.  `FullTheoryLedger` is not imported.
  14`measure_flag_moved = false` is rfl-forced below.
  15
  16## What is proved
  17
  18**D1 (statability gate G1).**  On serially named (labeled) bounded complexes, a
  19`labeledWeight` carries no `gibbsWeight` factor.  `RelabelInvariant` is stated
  20letterwise: invariance under the serial-name permutation action (`Gap2GaugeVolume.push`).
  21Its hypothesis side names neither `Aut`, nor orbit, nor stabilizer, nor gauge class, nor
  22canonical representative.  For the erasure map `q = Quotient.mk (relabelSetoid B)`,
  23
  24  `(q_* w)(K) = w(L_K) · (nV! · nE! · nT!) / |Aut K|`
  25
  26by orbit-stabilizer (`Gap2GaugeVolume.orbitCard_mul_autCard`).  Corollary:
  27`gibbsWeight` is the size-only factor of that Jacobian (not a substrate hypothesis).
  28
  29**D2 (discrimination gate G2).**  Locality `h(A ⊔ B) = h(A) + h(B)` is an explicit
  30hypothesis (the raw `LetterCost` API admits ambient-dependent charges).  On the
  31admissible witness `A = dust 1` with `A ⊔ A` admissible, `|Aut(A ⊔ A)| = 2 · |Aut A|²`
  32by the S₂ wreath factor, so `log|Aut|` is not disjoint-additive.  Hence no locally
  33additive cost realizes `log|Aut|`.  Fugacity-robust corollary: no
  34disjoint-multiplicative numerator `Q` times count fugacities converts the gauge weight
  35into uniform-on-iso-classes, because the S₂ factor cannot be absorbed.
  36
  37## Pre-flight Aut note (directed carrier)
  38
  39Library `Aut K := Relabel K K` is the group of incidence-preserving index bijections on
  40the directed/ordered carrier.  Permuting isomorphic connected components is included
  41(component swap is an automorphism).  Reversing a directed edge with distinct endpoints
  42is **not** included.  Panel undirected witnesses `|Aut|=8` vs `|Aut|=2` at count vector
  43`(4,2,0)` therefore do **not** hold as stated; the directed recomputation is `|Aut|=2`
  44(two disjoint directed edges) vs `|Aut|=1` (directed 2-path plus isolated vertex), so
  45the predicted class-mass ratio is `1/2`, not `1/4`.  The D2 wreath identity used below
  46is unaffected: it needs only the S₂ factor on identical components, which the directed
  47carrier still supplies (witness: dust).
  48
  49Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Gravity
  54namespace SevenGaps
  55namespace Gap2LabelErasure
  56
  57open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  58open Gap2GluingDerivation Gap2PostingCostDerivation Gap2NonEquivariantPosting
  59
  60variable {B : ℕ}
  61
  62/-! ## §1. Letterwise relabeling invariance (G1 hypothesis side)
  63
  64The invariance predicate below is the entire load of gate G1.  Its binders mention
  65serial-name permutations and the rename action only. -/
  66
  67/-- A **labeled weight**: a real function of serially named bounded complexes.
  68Definitionally no `gibbsWeight` factor appears. -/
  69abbrev labeledWeight (B : ℕ) : Type := BoundedComplex B → ℝ
  70
  71/-- Rename a labeled complex by independently permuting its vertex, edge, and
  72tetrahedron serial names (the carrier's incidence is transported).  This is
  73`Gap2GaugeVolume.push` under a letterwise name. -/
  74def rename (K : BoundedComplex B)
  75    (σv : Equiv.Perm (Fin K.nV)) (σe : Equiv.Perm (Fin K.nE))
  76    (σt : Equiv.Perm (Fin K.nT)) : BoundedComplex B :=
  77  Gap2GaugeVolume.push K (σv, σe, σt)
  78
  79/-- **Letterwise relabeling invariance.**  The weight is unchanged when serial names
  80are permuted.  No Aut, orbit, stabilizer, gauge class, or canonical representative
  81appears in this definition. -/
  82def RelabelInvariant {B : ℕ} (w : labeledWeight B) : Prop :=
  83  ∀ (K : BoundedComplex B) (σv : Equiv.Perm (Fin K.nV))
  84    (σe : Equiv.Perm (Fin K.nE)) (σt : Equiv.Perm (Fin K.nT)),
  85    w (rename K σv σe σt) = w K
  86
  87/-- Erasure: forget serial names down to the isomorphism class. -/
  88def erase (B : ℕ) : BoundedComplex B → TriangulationClass B :=
  89  Quotient.mk (relabelSetoid B)
  90
  91/-- Pushforward of a labeled weight along erasure: sum the weight over the fibre. -/
  92noncomputable def erasePush {B : ℕ} (w : labeledWeight B)
  93    (c : TriangulationClass B) : ℝ :=
  94  classMass w c
  95
  96/-! ## §2. Letterwise invariance implies class-function invariance -/
  97
  98theorem rename_eq_push (K : BoundedComplex B)
  99    (σv : Equiv.Perm (Fin K.nV)) (σe : Equiv.Perm (Fin K.nE))
 100    (σt : Equiv.Perm (Fin K.nT)) :
 101    rename K σv σe σt = Gap2GaugeVolume.push K (σv, σe, σt) := rfl
 102
 103/-- Letterwise invariance upgrades to invariance under any relabeling equivalence. -/
 104theorem relabelInvariant_implies_classFun {w : labeledWeight B}
 105    (hw : RelabelInvariant w) {K K' : BoundedComplex B} (h : Equivalent K K') :
 106    w K = w K' := by
 107  obtain ⟨r⟩ := h
 108  let g : Gap2GaugeVolume.SectorGroup K := Gap2GaugeVolume.toSector ⟨K', r⟩
 109  have hpair : Gap2GaugeVolume.ofSector K g = ⟨K', r⟩ :=
 110    Gap2GaugeVolume.ofSector_toSector K ⟨K', r⟩
 111  have hpush : Gap2GaugeVolume.push K g = K' := congrArg Sigma.fst hpair
 112  have hw' : w (Gap2GaugeVolume.push K g) = w K := hw K g.1 g.2.1 g.2.2
 113  rw [← hpush, hw']
 114
 115/-- The constant weight `1` is letterwise relabeling-invariant. -/
 116theorem relabelInvariant_one : RelabelInvariant (fun _ : BoundedComplex B => (1 : ℝ)) := by
 117  intro K σv σe σt; rfl
 118
 119/-- An equivariant letter cost has a letterwise-invariant Boltzmann numerator. -/
 120theorem relabelInvariant_exp_neg_history {c : LetterCost} (hc : Equivariant c) :
 121    RelabelInvariant (fun K : BoundedComplex B => Real.exp (-(historyCost c B K))) := by
 122  intro K σv σe σt
 123  have hEq : Equivalent K (rename K σv σe σt) :=
 124    Gap2GaugeVolume.equivalent_push K (σv, σe, σt)
 125  obtain ⟨r⟩ := hEq
 126  simp only [historyCost_invariant hc r]
 127
 128/-! ## §3. D1: pushforward equals labeled weight times the gauge divisor -/
 129
 130/-- **D1.**  For any letterwise relabeling-invariant labeled weight, the erasure
 131pushforward on the class of `K` equals the weight at `K` times the gauge divisor
 132`(nV! nE! nT!) / |Aut K|`.  `|Aut|` appears only in the conclusion. -/
 133theorem pushforward_labeledWeight_eq_gauge_divisor
 134    (w : labeledWeight B) (hw : RelabelInvariant w) (K : BoundedComplex B) :
 135    erasePush w (erase B K)
 136      = w K * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 137          / (Nat.card (Aut K) : ℝ) := by
 138  have hinv : ∀ K₁ K₂ : BoundedComplex B, Equivalent K₁ K₂ → w K₁ = w K₂ :=
 139    fun _ _ h => relabelInvariant_implies_classFun hw h
 140  have hpos : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by exact_mod_cast autCard_pos K
 141  have hmass :
 142      erasePush w (erase B K)
 143        = (gaugeOrbitCard K : ℝ) * w (Quotient.out (erase B K)) := by
 144    unfold erasePush erase
 145    rw [classMass_of_invariant w hinv, orbitCardClass_mk]
 146  have hout : w (Quotient.out (erase B K)) = w K :=
 147    hinv _ _ (equivalent_out K)
 148  have hOS :
 149      (gaugeOrbitCard K : ℝ) * (Nat.card (Aut K) : ℝ)
 150        = ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) := by
 151    exact_mod_cast orbitCard_mul_autCard K
 152  rw [hmass, hout]
 153  have hdiv :
 154      (gaugeOrbitCard K : ℝ)
 155        = ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 156            / (Nat.card (Aut K) : ℝ) :=
 157    (eq_div_iff hpos.ne').2 hOS
 158  rw [hdiv, mul_div_assoc, mul_comm]
 159
 160/-- Uniform labeled weight pushes forward to the orbit count; times `gibbsWeight` is `mu`. -/
 161theorem mu_eq_gibbs_mul_erasePush_one (K : BoundedComplex B) :
 162    mu K
 163      = gibbsWeight K
 164          * erasePush (fun _ : BoundedComplex B => (1 : ℝ)) (erase B K) := by
 165  have h1 := pushforward_labeledWeight_eq_gauge_divisor
 166    (fun _ : BoundedComplex B => (1 : ℝ)) relabelInvariant_one K
 167  have hpos : (0 : ℝ) < (Nat.card (Aut K) : ℝ) := by exact_mod_cast autCard_pos K
 168  unfold gibbsWeight mu
 169  rw [h1]
 170  field_simp [hpos.ne']
 171
 172/-- **Corollary.**  The posted weight factors as Boltzmann numerator times
 173`gibbsWeight`; under letterwise invariance of the numerator, D1 identifies
 174`gibbsWeight` as the size-only factor of the erasure Jacobian
 175`(nV! nE! nT!) / |Aut|`, not as an independent substrate hypothesis. -/
 176theorem gibbsWeight_is_the_erasure_jacobian
 177    {c : LetterCost} (hc : Equivariant c) (K : BoundedComplex B) :
 178    erasePush (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K'))) (erase B K)
 179      = Real.exp (-(historyCost c B K))
 180          * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 181          / (Nat.card (Aut K) : ℝ)
 182      ∧ postedWeight c B K
 183          = Real.exp (-(historyCost c B K)) * gibbsWeight K
 184      ∧ mu K
 185          = gibbsWeight K
 186              * erasePush (fun _ : BoundedComplex B => (1 : ℝ)) (erase B K) :=
 187  ⟨pushforward_labeledWeight_eq_gauge_divisor _
 188      (relabelInvariant_exp_neg_history hc) K,
 189    rfl,
 190    mu_eq_gibbs_mul_erasePush_one K⟩
 191
 192/-! ## §4. G2 witness: admissible A with A ⊔ A admissible -/
 193
 194/-- **G2(a).**  The singleton dust complex is admissible at cap 1, and its
 195disjoint union with itself is admissible at cap 2 (equivalent to `dust 2`). -/
 196theorem dust_twin_admissible :
 197    (dust 1 : BoundedComplex 1).nV = 1 ∧ (dust 1).nE = 0 ∧ (dust 1).nT = 0
 198      ∧ Equivalent (dunion (dust 1) (dust 1)) (dust 2) :=
 199  ⟨rfl, rfl, rfl, dunion_dust_equivalent 1 1⟩
 200
 201/-- **Wreath factor on the dust twin.**  `|Aut(A ⊔ A)| = 2 · |Aut A|²` for
 202`A = dust 1`. -/
 203theorem autCard_dust_twin :
 204    Nat.card (Aut (dunion (dust 1) (dust 1)))
 205      = 2 * (Nat.card (Aut (dust 1))) ^ 2 := by
 206  rw [autCard_congr (dunion_dust_equivalent 1 1), autCard_dust, autCard_dust]
 207  decide
 208
 209/-- The wreath factor is strictly larger than the naive product of Aut counts. -/
 210theorem autCard_dust_twin_ne_square :
 211    Nat.card (Aut (dunion (dust 1) (dust 1)))
 212      ≠ Nat.card (Aut (dust 1)) * Nat.card (Aut (dust 1)) := by
 213  rw [autCard_dust_twin, autCard_dust]
 214  decide
 215
 216/-! ## §5. D2: no local additive cost realizes log|Aut| -/
 217
 218/-- Explicit locality hypothesis for a size-indexed real cost: additive under
 219disjoint union.  Required because the raw `LetterCost` API admits
 220ambient-dependent charges, so additivity is not free. -/
 221def LocallyAdditive (h : ∀ B : ℕ, BoundedComplex B → ℝ) : Prop :=
 222  ∀ (B B' : ℕ) (A : BoundedComplex B) (C : BoundedComplex B'),
 223    h (B + B') (dunion A C) = h B A + h B' C
 224
 225/-- **D2.**  No locally additive real cost on bounded complexes can realize
 226`log|Aut|` at every complex.  Witness: `A = dust 1` forces
 227`log|Aut(A ⊔ A)| = log 2` against `2 · log|Aut A| = 0`. -/
 228theorem no_local_additive_cost_realizes_log_aut :
 229    ¬ ∃ h : ∀ B : ℕ, BoundedComplex B → ℝ,
 230        LocallyAdditive h
 231          ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 232              h B K = Real.log (Nat.card (Aut K) : ℝ)) := by
 233  intro ⟨h, hloc, hlog⟩
 234  have hEq := hloc 1 1 (dust 1) (dust 1)
 235  have hEq' :
 236      Real.log (Nat.card (Aut (dunion (dust 1) (dust 1))) : ℝ)
 237        = Real.log (Nat.card (Aut (dust 1)) : ℝ)
 238            + Real.log (Nat.card (Aut (dust 1)) : ℝ) := by
 239    simpa [hlog] using hEq
 240  have hL : Nat.card (Aut (dunion (dust 1) (dust 1))) = 2 := by
 241    rw [autCard_congr (dunion_dust_equivalent 1 1), autCard_dust]; decide
 242  have hR : Nat.card (Aut (dust 1)) = 1 := by rw [autCard_dust]; decide
 243  have h2 : Real.log (2 : ℝ) = Real.log (1 : ℝ) + Real.log (1 : ℝ) := by
 244    simpa [hL, hR] using hEq'
 245  have h0 : Real.log (1 : ℝ) = 0 := Real.log_one
 246  have hbad : Real.log (2 : ℝ) = 0 := by simpa [h0] using h2
 247  exact (ne_of_gt (Real.log_pos (by norm_num : (1 : ℝ) < 2))) hbad
 248
 249/-- **Fugacity-robust corollary.**  No disjoint-multiplicative numerator `Q`
 250together with three count fugacities can convert the gauge weight into
 251uniform-on-iso-classes: the identity `Q · z^counts = |Aut|` fails at the dust
 252twin because the left side squares while the right side carries the S₂ factor. -/
 253theorem uniform_is_not_a_local_pushforward :
 254    ¬ ∃ (Q : ∀ B : ℕ, BoundedComplex B → ℝ) (zV zE zT : ℝ),
 255        (∀ (B B' : ℕ) (A : BoundedComplex B) (C : BoundedComplex B'),
 256          Q (B + B') (dunion A C) = Q B A * Q B' C)
 257          ∧ (∀ (B : ℕ) (K : BoundedComplex B),
 258              Q B K * zV ^ K.nV * zE ^ K.nE * zT ^ K.nT
 259                = (Nat.card (Aut K) : ℝ)) := by
 260  intro ⟨Q, zV, zE, zT, hQ, hAut⟩
 261  have h1 := hAut 1 (dust 1)
 262  have h2 := hAut (1 + 1) (dunion (dust 1) (dust 1))
 263  have hQd := hQ 1 1 (dust 1) (dust 1)
 264  have hR : Nat.card (Aut (dust 1)) = 1 := by rw [autCard_dust]; decide
 265  have hL : Nat.card (Aut (dunion (dust 1) (dust 1))) = 2 := by
 266    rw [autCard_congr (dunion_dust_equivalent 1 1), autCard_dust]; decide
 267  -- At dust 1: Q * zV = 1.
 268  have hone : Q 1 (dust 1) * zV = (1 : ℝ) := by
 269    simpa [dust_nV, dust_nE, dust_nT, hR, pow_one, pow_zero, mul_one] using h1
 270  -- At the twin: Q(A⊔A) * zV^2 = 2, and Q(A⊔A) = Q(A)^2.
 271  have hsq : Q 1 (dust 1) * Q 1 (dust 1) * zV ^ 2 = (2 : ℝ) := by
 272    have h2' :
 273        Q (1 + 1) (dunion (dust 1) (dust 1))
 274            * zV ^ ((dust 1).nV + (dust 1).nV)
 275            * zE ^ ((dust 1).nE + (dust 1).nE)
 276            * zT ^ ((dust 1).nT + (dust 1).nT)
 277          = (2 : ℝ) := by
 278      simpa [dunion_nV, dunion_nE, dunion_nT, hL] using h2
 279    simpa [hQd, dust_nV, dust_nE, dust_nT, pow_zero, mul_one] using h2'
 280  have hpow : (Q 1 (dust 1) * zV) ^ 2 = (2 : ℝ) := by
 281    calc (Q 1 (dust 1) * zV) ^ 2
 282        = Q 1 (dust 1) * Q 1 (dust 1) * zV ^ 2 := by ring
 283      _ = 2 := hsq
 284  rw [hone] at hpow
 285  norm_num at hpow
 286
 287/-! ## §6. Certificate: flag unmoved -/
 288
 289structure LabelErasureIndex : Type where
 290  /-- D1 is stated with letterwise RelabelInvariant (G1). -/
 291  d1_stated_letterwise : Bool
 292  /-- D2 landed with locality explicit and the dust twin witness (G2). -/
 293  d2_wreath_witness : Bool
 294  /-- NOT claimed: flag 8 / gap2_measure_derived. -/
 295  measure_flag_moved : Bool
 296
 297def labelErasureIndex : LabelErasureIndex where
 298  d1_stated_letterwise := true
 299  d2_wreath_witness := true
 300  measure_flag_moved := false
 301
 302theorem index_d1 : labelErasureIndex.d1_stated_letterwise = true := rfl
 303theorem index_d2 : labelErasureIndex.d2_wreath_witness = true := rfl
 304/-- NOT moved.  Flag 8 stays false; this module derives the Jacobian reading, not
 305the full measure. -/
 306theorem index_flag_unmoved : labelErasureIndex.measure_flag_moved = false := rfl
 307
 308/-! ## Axiom audit -/
 309
 310#print axioms relabelInvariant_implies_classFun
 311#print axioms pushforward_labeledWeight_eq_gauge_divisor
 312#print axioms gibbsWeight_is_the_erasure_jacobian
 313#print axioms mu_eq_gibbs_mul_erasePush_one
 314#print axioms dust_twin_admissible
 315#print axioms autCard_dust_twin
 316#print axioms autCard_dust_twin_ne_square
 317#print axioms no_local_additive_cost_realizes_log_aut
 318#print axioms uniform_is_not_a_local_pushforward
 319#print axioms index_flag_unmoved
 320
 321end Gap2LabelErasure
 322end SevenGaps
 323end Gravity
 324end IndisputableMonolith
 325