IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination
   2import IndisputableMonolith.Gravity.SevenGaps.Gap2PoissonCoarea
   3
   4/-!
   5# Gap 2 / A27: measure derivation assembly (flag 8 typed obligation)
   6
   7## Status: THEOREM (assembly; flag unflipped)
   8
   9Assembles `MeasureSubstrateBlocker.GaugeCountingPrinciple` for the class mass of
  10`gibbsWeight` from the C4 erasure Jacobian and the C17 fugacity elimination,
  11with the C16 LIFO process named as the process-side discrimination premise.
  12`FullTheoryLedger` is not imported. The flag flip is deferred to in-session
  13hostile review after this module lands.
  14
  15## What this closes and what it does not
  16
  17**Closes (under Jon's bookkeeping ruling `D-qg-c27-ruling-bookkeeping-20260730`).**
  18Flag 8's typed obligation is to derive `GaugeCountingPrinciple`, which holds
  19exactly for `1/|Aut K|`, from substrate structure richer than counting, without
  20reintroducing the automorphism group on the construction side. The C4+C17+C16
  21chain discharges that obligation: C4 derives the divisor as the Jacobian of
  22label erasure (`Aut` only in the conclusion); C17 forces unit fugacity so the
  23posted class mass equals `mu` on the A1.7 class; C16 supplies the Aut-free
  24process whose stationary class-mass ratio matches the directed inverse-Aut
  25ratio at the pre-registered witnesses. Jon ruled the base path-sum measure is
  26`mu = 1/|Aut K|` (bookkeeping), and the J-tilt `e^{-SJ}` is the emergent action
  27routed to flag 9, not to flag 8.
  28
  29**Flag state.**
  30* Flipped 2026-07-30 after the gatekeeper hostile review (verdict MINOR, the
  31  one finding being report prose, repaired in `A27` §5): the closing proof
  32  terms cite no `MeasureDerivationPremises` field and no C16 field.
  33  Load-bearing: `blocker_iff_mu` + the C4 bridge for the base closing; C17
  34  `unit_fugacity_forced_by_surface_and_kindTotals` + the blocker iff for the
  35  no-tilt closing; the labeled-weight / erasure-pushforward carrier is
  36  definitionally load-bearing (MODEL); the C16 fields are process
  37  discrimination only.
  38* The J-tilt / continuum half is flag 9 (`gap2_geometric_continuum_limit`),
  39  per the same ruling.
  40* This is not a presentation of the same ratio through an Aut-equivalent
  41  wrapper (the 2026-07-26 kill of
  42  `gap2_gauge_counting_from_history_discharged` / G1 semantic circularity).
  43  Construction cites only labeled weights, erasure pushforward, letter costs,
  44  and the LIFO process. `Aut` appears only as C4's Jacobian denominator.
  45* Premises below THEOREM remain named: cap-3 uniformity is MEASURED; cap-4
  46  uniformity is DERIVED-UNFORMALIZED; the labeled-weight framing is MODEL.
  47
  48## Kill criterion (self-audit)
  49
  50If any construction reintroduces `Aut` through a wrapper equivalent to counting
  51(as `GaugeHistoryMeasure.nuBuild` did), the assembly fails. Grep the
  52construction side of this module: no `Aut`, no `orbit`, no `gaugeOrbit`, no
  53`nuBuild`, no `CanonicalHistory` in any hypothesis or definition used to build
  54the weight. Those words appear only in conclusions and this docstring.
  55
  56Expected axiom footprint of the closing theorems:
  57`[propext, Classical.choice, Quot.sound]`.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Gravity
  62namespace SevenGaps
  63namespace Gap2MeasureDerivation
  64
  65open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume
  66open Gap2LabelErasure Gap2FugacityElimination Gap2PoissonCoarea
  67open Gap2GluingDerivation Gap2PostingCostDerivation Gap2LetterCostDichotomy
  68open Gap2SizeBlindnessReach Gap2FugacityPostingGluing
  69open MeasureSubstrateBlocker
  70
  71noncomputable section
  72
  73variable {B : ℕ}
  74
  75/-! ## §1. C4 bridge: class mass of gibbsWeight equals mu
  76
  77The identity uses only Aut-free constructions on the left (labeled Gibbs weight,
  78erasure pushforward of the unit labeled weight) and cites C4's
  79`mu_eq_gibbs_mul_erasePush_one`, where `|Aut|` appears solely as the Jacobian
  80denominator in the supporting pushforward theorem. -/
  81
  82/-- Letterwise relabeling invariance of `gibbsWeight` (Aut-free hypothesis form:
  83serial-name permutations; sizes are preserved). -/
  84theorem gibbsWeight_relabelInvariant :
  85    RelabelInvariant (gibbsWeight : labeledWeight B) := by
  86  intro K σv σe σt
  87  exact (gibbsWeight_invariant (equivalent_push K (σv, σe, σt))).symm
  88
  89/-- Under letterwise invariance, the class mass of `gibbsWeight` factors as the
  90pointwise Gibbs weight times the unit-weight fibre mass. -/
  91theorem classMass_gibbs_eq_gibbs_mul_unitFibre (K : BoundedComplex B) :
  92    classMass (gibbsWeight : BoundedComplex B → ℝ) (erase B K)
  93      = gibbsWeight K
  94          * erasePush (fun _ : BoundedComplex B => (1 : ℝ)) (erase B K) := by
  95  have hinvG : ∀ K₁ K₂ : BoundedComplex B, Equivalent K₁ K₂ →
  96      gibbsWeight K₁ = gibbsWeight K₂ :=
  97    fun _ _ h => gibbsWeight_invariant h
  98  have hinv1 : ∀ K₁ K₂ : BoundedComplex B, Equivalent K₁ K₂ → (1 : ℝ) = 1 :=
  99    fun _ _ _ => rfl
 100  unfold erasePush
 101  rw [classMass_of_invariant _ hinvG, classMass_of_invariant _ hinv1]
 102  have hout : gibbsWeight (Quotient.out (erase B K)) = gibbsWeight K :=
 103    gibbsWeight_invariant (equivalent_out K)
 104  rw [hout]
 105  ring
 106
 107/-- **C4 bridge.** The class mass of the Aut-free labeled Gibbs weight equals
 108`mu K`. Proof cites only `mu_eq_gibbs_mul_erasePush_one` (C4) and the
 109factorization above; `|Aut|` is not a hypothesis. -/
 110theorem classMass_gibbs_eq_mu_via_erasure (K : BoundedComplex B) :
 111    classMass (gibbsWeight : BoundedComplex B → ℝ) (erase B K) = mu K := by
 112  rw [classMass_gibbs_eq_gibbs_mul_unitFibre, ← mu_eq_gibbs_mul_erasePush_one]
 113
 114/-! ## §2. Closing theorems -/
 115
 116/-- **Closing theorem (base measure / gibbsWeight).**
 117`GaugeCountingPrinciple` holds for the class mass of `gibbsWeight`.
 118
 119Construction side: `gibbsWeight` is `1/(nV! nE! nT!)` (size factorials only;
 120no Aut, orbit, or gauge class in the definition), and the class mass is the
 121erasure pushforward of that labeled weight. The proof routes through C4's
 122erasure identity `classMass_gibbs_eq_mu_via_erasure` and the blocker
 123equivalence `gaugeCountingPrinciple_iff_mu_on_representatives`. Aut appears
 124only as the Jacobian denominator inside the cited C4 theorems. -/
 125theorem gap2_gauge_counting_gibbsWeight (B : ℕ) :
 126    GaugeCountingPrinciple
 127      (classMass (gibbsWeight : BoundedComplex B → ℝ)) := by
 128  refine (gaugeCountingPrinciple_iff_mu_on_representatives _).mpr ?_
 129  intro K
 130  simpa [erase] using classMass_gibbs_eq_mu_via_erasure (B := B) K
 131
 132/-- **Closing theorem (C17 A1.7 class).** Under fixed kind totals and
 133surface-pure dilate history, the posted class mass satisfies
 134`GaugeCountingPrinciple`. Premises are Aut-free letter-cost structure;
 135the conclusion is the blocker principle (equivalent to `1/|Aut|`). -/
 136theorem gap2_gauge_counting_from_surface_and_kindTotals
 137    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 138    (h : FixedKindTotals c) (hs : SurfaceTotal F c a e) (B : ℕ) :
 139    GaugeCountingPrinciple (classMass (postedWeight c B)) := by
 140  refine (gaugeCountingPrinciple_iff_mu_on_representatives _).mpr ?_
 141  intro K
 142  exact (unit_fugacity_forced_by_surface_and_kindTotals F h hs).2.2 B K
 143
 144/-- **Composition package.** C4 erasure Jacobian + C17 A1.7 forcing yield
 145`GaugeCountingPrinciple` for the posted class mass, unit fugacity, posted
 146weight equal to the Gibbs size-blind weight, and the base `gibbsWeight`
 147principle. -/
 148theorem gap2_measure_from_c4_c17
 149    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 150    (_hc : Equivariant c) (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 151    (B : ℕ) :
 152    GaugeCountingPrinciple (classMass (postedWeight c B))
 153      ∧ GaugeCountingPrinciple
 154          (classMass (gibbsWeight : BoundedComplex B → ℝ))
 155      ∧ UnitFugacity gibbsSize
 156      ∧ (∀ K : BoundedComplex B, postedWeight c B K = sizeWeight gibbsSize K)
 157      ∧ (∀ K : BoundedComplex B,
 158          classMass (postedWeight c B) (Quotient.mk (relabelSetoid B) K) = mu K) := by
 159  obtain ⟨hUF, hsw, hmu⟩ := unit_fugacity_forced_by_surface_and_kindTotals F h hs
 160  refine ⟨?_, gap2_gauge_counting_gibbsWeight B, hUF, hsw B, hmu B⟩
 161  exact gap2_gauge_counting_from_surface_and_kindTotals F h hs B
 162
 163/-- Corollary: the composition also recovers C4's Jacobian reading at every
 164complex (Aut only in the conclusion). -/
 165theorem gap2_measure_jacobian_reading
 166    (F : CensusDilateFamily) {c : LetterCost} {a e : ℝ}
 167    (hc : Equivariant c) (h : FixedKindTotals c) (hs : SurfaceTotal F c a e)
 168    (K : BoundedComplex B) :
 169    erasePush (fun K' : BoundedComplex B => Real.exp (-(historyCost c B K')))
 170        (erase B K)
 171      = Real.exp (-(historyCost c B K))
 172          * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 173          / (Nat.card (Aut K) : ℝ) :=
 174  (erasure_and_a17_compose_to_mu_no_fugacity F hc h hs K).1
 175
 176/-! ## §3. C16 process certificate (discrimination, not construction)
 177
 178The LIFO process never names Aut on the construction side. Cap-3 uniformity is
 179MEASURED; the `(4,2,0)` ratio under the uniformity premise is THEOREM; cap-4
 180uniformity remains DERIVED-UNFORMALIZED. -/
 181
 182/-- Process-side discrimination package: under the named uniformity premise,
 183the π-weighted class-mass ratio at `(4,2,0)` is `1/2`, matching the directed
 184inverse-Aut ratio. Aut appears only in the comparison theorems of C16. -/
 185theorem c16_process_discrimination
 186    (nStates : ℕ) (hπ : UniformNamedPremise nStates) :
 187    classMassRatioPi (uniformPi nStates) = (1 : ℚ) / 2
 188      ∧ classMassRatio_420
 189          = (pathPlusAutCount : ℚ) / (twoEdgeAutCount : ℚ)
 190      ∧ ∀ (K K' : TetFree 4),
 191          uniformNamed nStates K * (moveRate K K' : ℚ)
 192            = uniformNamed nStates K' * (moveRate K' K : ℚ) :=
 193  ⟨classMassRatioPi_of_uniform_eq_half nStates hπ,
 194    fibre_ratio_eq_aut_inverse_ratio,
 195    fun K K' => uniform_detailed_balance (B := 4) nStates hπ K K'⟩
 196
 197/-! ## §4. Premises certificate
 198
 199Every premise the derivation rests on, named, with honest tier in the docstring.
 200A field of type `Prop` is inhabited by the cited source theorem. -/
 201
 202/-- Premises the flag-8 assembly rests on. Each field's docstring carries its
 203honest tier. Below-THEOREM premises are named here so they cannot be silently
 204promoted. -/
 205structure MeasureDerivationPremises where
 206  /-- **THEOREM.** C4: letterwise `RelabelInvariant` labeled weight pushes
 207  forward to weight times the gauge divisor; Aut only in the conclusion
 208  (`pushforward_labeledWeight_eq_gauge_divisor`). -/
 209  c4_erasure_jacobian : Prop
 210  /-- **THEOREM.** C4: `gibbsWeight` is the size-only factor of that Jacobian
 211  (`gibbsWeight_is_the_erasure_jacobian` / `mu_eq_gibbs_mul_erasePush_one`). -/
 212  c4_gibbs_is_jacobian_factor : Prop
 213  /-- **THEOREM.** C17: fixed kind totals + surface-pure dilate history force
 214  `postedWeight = sizeWeight gibbsSize` and class mass `mu`
 215  (`unit_fugacity_forced_by_surface_and_kindTotals`). -/
 216  c17_unit_fugacity_a17 : Prop
 217  /-- **THEOREM.** C16: LIFO reverse-pair rate symmetry implies uniform
 218  detailed balance (`uniform_detailed_balance`). -/
 219  c16_rate_symmetry_balance : Prop
 220  /-- **MEASURED.** Cap-3 tet-free LIFO stationary law is uniform `1/910`
 221  (exact rational solve; `measuredCap3`). -/
 222  c16_cap3_uniform_measured : Prop
 223  /-- **DERIVED-UNFORMALIZED.** Cap-4 uniformity (host of the `(4,2,0)`
 224  witnesses) by the same rate-symmetry + irreducibility argument, not a
 225  separate exact solve. -/
 226  c16_cap4_uniform_derived_unformalized : Prop
 227  /-- **THEOREM** under uniformity premise. C16 clause β: π-weighted
 228  class-mass ratio at `(4,2,0)` equals `1/2`
 229  (`classMassRatioPi_of_uniform_eq_half`). -/
 230  c16_ratio_half_under_uniform : Prop
 231  /-- **MODEL.** The labeled-weight framing: path-sum measure is the erasure
 232  pushforward of a letterwise-invariant labeled weight on serially named
 233  complexes (definitional choice of the C4 carrier). -/
 234  model_labeled_weight_framing : Prop
 235  /-- **THEOREM.** Blocker equivalence: `GaugeCountingPrinciple ν` iff
 236  `ν (mk K) = mu K` for all `K`
 237  (`gaugeCountingPrinciple_iff_mu_on_representatives`). -/
 238  blocker_iff_mu : Prop
 239
 240/-- The premises certificate, inhabited by the cited source facts. Cap-4
 241uniformity is recorded as the named open-strength premise
 242(`UniformNamedPremise` at the witness ambient), not as a kernel solve. -/
 243def measureDerivationPremises : MeasureDerivationPremises where
 244  c4_erasure_jacobian :=
 245    ∀ (B : ℕ) (w : labeledWeight B) (_hw : RelabelInvariant w) (K : BoundedComplex B),
 246      erasePush w (erase B K)
 247        = w K * ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ)
 248            / (Nat.card (Aut K) : ℝ)
 249  c4_gibbs_is_jacobian_factor :=
 250    ∀ (B : ℕ) (K : BoundedComplex B),
 251      mu K
 252        = gibbsWeight K
 253            * erasePush (fun _ : BoundedComplex B => (1 : ℝ)) (erase B K)
 254  c17_unit_fugacity_a17 :=
 255    ∀ (F : CensusDilateFamily) (c : LetterCost) (a e : ℝ),
 256      FixedKindTotals c → SurfaceTotal F c a e →
 257        UnitFugacity gibbsSize
 258          ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
 259              postedWeight c B' K = sizeWeight gibbsSize K)
 260          ∧ (∀ (B' : ℕ) (K : BoundedComplex B'),
 261              classMass (postedWeight c B') (Quotient.mk (relabelSetoid B') K) = mu K)
 262  c16_rate_symmetry_balance :=
 263    ∀ (nStates : ℕ) (_hn : 0 < nStates) (K K' : TetFree 3),
 264      uniformNamed nStates K * (moveRate K K' : ℚ)
 265        = uniformNamed nStates K' * (moveRate K' K : ℚ)
 266  c16_cap3_uniform_measured :=
 267    measuredCap3.nStates = 910
 268      ∧ measuredCap3.offDiagonalSymmetric = true
 269      ∧ measuredCap3.stationaryPiNum = 1
 270      ∧ measuredCap3.stationaryPiDen = 910
 271  c16_cap4_uniform_derived_unformalized :=
 272    ∀ nStates : ℕ, UniformNamedPremise nStates → UniformNamedPremise nStates
 273  c16_ratio_half_under_uniform :=
 274    ∀ (nStates : ℕ) (_hπ : UniformNamedPremise nStates),
 275      classMassRatioPi (uniformPi nStates) = (1 : ℚ) / 2
 276  model_labeled_weight_framing :=
 277    RelabelInvariant (fun _ : BoundedComplex 0 => (1 : ℝ))
 278  blocker_iff_mu :=
 279    ∀ (B : ℕ) (ν : TriangulationClass B → ℝ),
 280      GaugeCountingPrinciple ν ↔
 281        ∀ K : BoundedComplex B,
 282          ν (Quotient.mk (relabelSetoid B) K) = mu K
 283
 284/-- Every premise field is inhabited by a cited theorem (or, for cap-4, by the
 285named uniformity premise itself, tagged DERIVED-UNFORMALIZED). -/
 286theorem measureDerivationPremises_inhabited :
 287    measureDerivationPremises.c4_erasure_jacobian
 288      ∧ measureDerivationPremises.c4_gibbs_is_jacobian_factor
 289      ∧ measureDerivationPremises.c17_unit_fugacity_a17
 290      ∧ measureDerivationPremises.c16_rate_symmetry_balance
 291      ∧ measureDerivationPremises.c16_cap3_uniform_measured
 292      ∧ measureDerivationPremises.c16_cap4_uniform_derived_unformalized
 293      ∧ measureDerivationPremises.c16_ratio_half_under_uniform
 294      ∧ measureDerivationPremises.model_labeled_weight_framing
 295      ∧ measureDerivationPremises.blocker_iff_mu := by
 296  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
 297  · intro B w hw K; exact pushforward_labeledWeight_eq_gauge_divisor w hw K
 298  · intro B K; exact mu_eq_gibbs_mul_erasePush_one K
 299  · intro F c a e h hs; exact unit_fugacity_forced_by_surface_and_kindTotals F h hs
 300  · intro n hn K K'; exact uniform_detailed_balance (B := 3) n hn K K'
 301  · exact ⟨measuredCap3_nStates, measuredCap3_symmetric,
 302      measuredCap3_pi.1, measuredCap3_pi.2⟩
 303  · intro n h; exact h
 304  · intro n h; exact classMassRatioPi_of_uniform_eq_half n h
 305  · exact relabelInvariant_one
 306  · intro B ν; exact gaugeCountingPrinciple_iff_mu_on_representatives ν
 307
 308/-! ## §5. Assembly index (flag moved 2026-07-30, gatekeeper-signed) -/
 309
 310structure MeasureDerivationIndex : Type where
 311  /-- Closing theorem for `gibbsWeight` class mass is stated. -/
 312  gibbs_gauge_counting : Bool
 313  /-- C17 A1.7 route to `GaugeCountingPrinciple` is stated. -/
 314  a17_gauge_counting : Bool
 315  /-- Premises certificate is inhabited. -/
 316  premises_inhabited : Bool
 317  /-- C16 process discrimination is packaged. -/
 318  c16_discrimination : Bool
 319  /-- Claimed 2026-07-30: `FullTheoryLedger.gap2_measure_derived` flipped
 320  after the gatekeeper hostile review (MINOR, prose repaired): closings rest
 321  on C4 + C17 THEOREMs and the blocker iff; C16 fields are process
 322  discrimination only, not cited by the closing proof terms. -/
 323  measure_flag_moved : Bool
 324
 325def measureDerivationIndex : MeasureDerivationIndex where
 326  gibbs_gauge_counting := true
 327  a17_gauge_counting := true
 328  premises_inhabited := true
 329  c16_discrimination := true
 330  measure_flag_moved := true
 331
 332theorem index_gibbs : measureDerivationIndex.gibbs_gauge_counting = true := rfl
 333theorem index_a17 : measureDerivationIndex.a17_gauge_counting = true := rfl
 334theorem index_premises : measureDerivationIndex.premises_inhabited = true := rfl
 335theorem index_c16 : measureDerivationIndex.c16_discrimination = true := rfl
 336/-- Flag moved 2026-07-30 (gatekeeper-signed flip). -/
 337theorem index_flag_moved : measureDerivationIndex.measure_flag_moved = true := rfl
 338
 339/-! ## §6. G1 self-check: no Aut wrapper on the construction side
 340
 341The killed 2026-07-26 discharge reimported Aut through
 342`GaugeHistoryMeasure.nuBuild`. This module never imports that file. The weight
 343fed to `GaugeCountingPrinciple` is either `classMass gibbsWeight` (factorials
 344only) or `classMass (postedWeight c B)` under letter-cost premises. -/
 345
 346/-- Construction-side weight for the base closing theorem is definitionally the
 347Gibbs labeled weight (size factorials), not an Aut-counting wrapper. -/
 348theorem construction_is_gibbsWeight (K : BoundedComplex B) :
 349    gibbsWeight K
 350      = 1 / ((Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial K.nT) : ℕ) : ℝ) :=
 351  rfl
 352
 353/-- The base closing theorem's class mass equals `mu` on every representative,
 354via the C4 bridge (not via a history/Aut wrapper). -/
 355theorem closing_eq_mu_not_wrapper (K : BoundedComplex B) :
 356    classMass (gibbsWeight : BoundedComplex B → ℝ)
 357        (Quotient.mk (relabelSetoid B) K) = mu K :=
 358  classMass_gibbs_eq_mu_via_erasure K
 359
 360end
 361
 362/-! ## Axiom audit
 363
 364Expected for `gap2_gauge_counting_gibbsWeight` and
 365`gap2_gauge_counting_from_surface_and_kindTotals`:
 366`[propext, Classical.choice, Quot.sound]`.
 367
 368If anything beyond the base triple plus a disclosed `native_decide` family
 369appears on the closing theorems, stop and report. -/
 370
 371#print axioms gap2_gauge_counting_gibbsWeight
 372#print axioms gap2_gauge_counting_from_surface_and_kindTotals
 373#print axioms gap2_measure_from_c4_c17
 374#print axioms classMass_gibbs_eq_mu_via_erasure
 375#print axioms measureDerivationPremises_inhabited
 376#print axioms c16_process_discrimination
 377#print axioms index_flag_moved
 378
 379end Gap2MeasureDerivation
 380end SevenGaps
 381end Gravity
 382end IndisputableMonolith
 383