IndisputableMonolith.Gravity.SevenGaps.GaugeHistoryMeasure

   1import IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker
   2import IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D
   3
   4/-!
   5# Wave C1 R5: gauge-counting measure from posted-history presentation
   6
   7Implements the adjudicated Codex design for gap2 gauge counting from
   8history (`plans/QG_WaveC1_Gap2_Residual_DAG_Draft_20260722.txt` residual R5),
   9repaired post-critic (Wave C1 R5 REPAIR 2026-07-22).
  10
  11## Core idea
  12
  13A `PostedBoundedHistory` is a labeled bounded complex whose incidence indices
  14are posting-alphabet elements of a dual-entry ledger state. History
  15relabeling is posting-alphabet gauge redundancy. The class measure is defined
  16as
  17
  18```
  19ν(c) = (# histories presenting c) / (history gauge volume of c)
  20```
  21
  22and is proved to satisfy `GaugeCountingPrinciple` by explicit bijections with
  23the banked orbit/pair counts. Equality with `gaugeOrbitMass` is obtained ONLY
  24through `gaugeCountingPrinciple_iff_eq_gaugeOrbitMass` (never by defining `ν`
  25to be that mass).
  26
  27## Honest scoping (design adjudication)
  28
  29The dual-entry columns **anchor** the substrate reading (ledger-native
  30carrier: postings over a `DualEntryStrainState`). The **count** is driven by
  31the posting/relabel presentation degrees of freedom. Arbitrary dual-entry
  32state fields would inflate the history count and break the counting identity,
  33so counted histories **carry** the dual-entry state and pin it to the
  34canonical balanced zero state (`debit = credit = 0`, `mag = 0`) by a Prop
  35field. Dual-entry is therefore present-and-pinned, not erased.
  36
  37## Non-circularity (honest boundary)
  38
  39"Does not mention Aut/mu" is a meta-level property of the definitional layer.
  40The formal layer proves counting theorems for the **named** definition
  41`nuBuild`. Non-circularity is certified by the definition text of `nuBuild`
  42together with the paired `rfl` audit certificates:
  43
  44* `nuBuild_def_history_only` — `nuBuild` is definitionally the history-count
  45  quotient;
  46* `circularNu_def_is_gaugeOrbitMass` — the circular decoy is definitionally
  47  `gaugeOrbitMass`.
  48
  49There is no `∃`-package that formally discharges non-circularity; a reader
  50audits the named definition plus those two certificates. The discharge
  51headline is `gap2_gauge_counting_from_history_discharged`.
  52
  53## Honesty / scope
  54
  55* Does **not** flip `gap2_continuum_and_measure` or continuum Bools.
  56* Status Bools `pathSumMeasureStatus.substrate_measure_derived` and
  57  `gaugePreflightStatus.counting_principle_derived_from_ledger` are
  58  flipped in Wave C1 R6 (`Gap2MeasureStatusBinding`), bound to
  59  `gap2_gauge_counting_from_history_discharged` in the same commit.
  60* No `sorry`, `admit`, new axiom, or `native_decide`.
  61-/
  62
  63namespace IndisputableMonolith
  64namespace Gravity
  65namespace SevenGaps
  66namespace GaugeHistoryMeasure
  67
  68open PathSumMeasure
  69open ExactShellGaugePreflight
  70open MeasureSubstrateBlocker
  71open Analysis.RecognitionDualEntryEnrichment4D
  72
  73noncomputable section
  74
  75variable {B : ℕ}
  76
  77/-! ## §1. Posted histories (ledger-native carrier) -/
  78
  79/-- Posting alphabet of a labeled complex: one letter per vertex, edge, and
  80tet index (avoids universe/counting inflation). -/
  81abbrev PostingAlphabet (K : BoundedComplex B) : Type :=
  82  Fin K.nV ⊕ Fin K.nE ⊕ Fin K.nT
  83
  84/-- Canonical balanced zero dual-entry state (normalized counting substrate). -/
  85def balancedZeroState (Λ : Type*) : DualEntryStrainState Λ where
  86  debit := fun _ => 0
  87  credit := fun _ => 0
  88  mag := fun _ => 0
  89  mag_nonneg := fun _ => le_rfl
  90  flux_unit := fun _ => by
  91    simp only [sub_self, abs_zero]
  92    exact zero_le_one
  93
  94/-- **Ledger-native history carrier.** A labeled bounded complex together with
  95a dual-entry strain state on its posting alphabet. Posting maps are the
  96canonical injections into `PostingAlphabet` (see `vertexPost` / `edgePost` /
  97`tetPost`). -/
  98structure PostedBoundedHistory (B : ℕ) where
  99  K : BoundedComplex B
 100  state : DualEntryStrainState (PostingAlphabet K)
 101
 102namespace PostedBoundedHistory
 103
 104variable {B : ℕ} (H : PostedBoundedHistory B)
 105
 106/-- Vertex posting map (canonical left injection). -/
 107def vertexPost : Fin H.K.nV → PostingAlphabet H.K :=
 108  Sum.inl
 109
 110/-- Edge posting map (canonical mid injection). -/
 111def edgePost : Fin H.K.nE → PostingAlphabet H.K :=
 112  fun e => Sum.inr (Sum.inl e)
 113
 114/-- Tet posting map (canonical right injection). -/
 115def tetPost : Fin H.K.nT → PostingAlphabet H.K :=
 116  fun t => Sum.inr (Sum.inr t)
 117
 118theorem vertexPost_injective : Function.Injective H.vertexPost :=
 119  Sum.inl_injective
 120
 121theorem edgePost_injective : Function.Injective H.edgePost := by
 122  intro e₁ e₂ h
 123  exact Sum.inl_injective (Sum.inr_injective h)
 124
 125theorem tetPost_injective : Function.Injective H.tetPost := by
 126  intro t₁ t₂ h
 127  exact Sum.inr_injective (Sum.inr_injective h)
 128
 129end PostedBoundedHistory
 130
 131/-- Canonical history presentation of a labeled complex: zero dual-entry state
 132and the complex's own incidence as the posting presentation. -/
 133def canonicalHistory (K : BoundedComplex B) : PostedBoundedHistory B where
 134  K := K
 135  state := balancedZeroState _
 136
 137/-- State-canonical posted histories equal the canonical presentation. -/
 138theorem PostedBoundedHistory.eq_canonicalHistory
 139    (H : PostedBoundedHistory B)
 140    (h : H.state = balancedZeroState (PostingAlphabet H.K)) :
 141    H = canonicalHistory H.K := by
 142  cases H with | mk K state
 143  -- `subst` rejects the raw hypothesis: `state` occurs syntactically in
 144  -- `PostingAlphabet { K := K, state := state }.K` before reduction.
 145  change state = balancedZeroState (PostingAlphabet K) at h
 146  subst h
 147  rfl
 148
 149/-! ## §2. Counted (normalized) histories — state-carrying -/
 150
 151/-- **Counted history.** Carries the full posted carrier (complex + dual-entry
 152state) with state pinned to the canonical balanced zero. The state is present
 153in the counted type; canonicality is a Prop field, not an erasure. -/
 154structure CanonicalHistory (B : ℕ) where
 155  H : PostedBoundedHistory B
 156  state_canonical : H.state = balancedZeroState (PostingAlphabet H.K)
 157
 158namespace CanonicalHistory
 159
 160variable {B : ℕ}
 161
 162/-- The posted carrier (state present). -/
 163abbrev toPosted (CH : CanonicalHistory B) : PostedBoundedHistory B := CH.H
 164
 165/-- Underlying labeled complex. -/
 166def underlying (CH : CanonicalHistory B) : BoundedComplex B := CH.H.K
 167
 168/-- Build the unique counted history presenting a labeled complex. -/
 169def ofComplex (K : BoundedComplex B) : CanonicalHistory B where
 170  H := canonicalHistory K
 171  state_canonical := rfl
 172
 173@[ext] theorem ext {CH₁ CH₂ : CanonicalHistory B} (h : CH₁.H = CH₂.H) :
 174    CH₁ = CH₂ := by
 175  cases CH₁; cases CH₂; cases h; rfl
 176
 177/-- Posted carrier of a counted history is the canonical presentation. -/
 178theorem toPosted_eq_canonicalHistory (CH : CanonicalHistory B) :
 179    CH.toPosted = canonicalHistory CH.underlying :=
 180  PostedBoundedHistory.eq_canonicalHistory CH.H CH.state_canonical
 181
 182/-- Triangulation class presented by this history. -/
 183def classOf (CH : CanonicalHistory B) : TriangulationClass B :=
 184  Quotient.mk (relabelSetoid B) CH.underlying
 185
 186/-- For each labeled complex, the state-canonicality fiber of counted
 187histories is a singleton (`Unique` is Type-valued, so this is a `def`). -/
 188noncomputable def fiber_unique (K : BoundedComplex B) :
 189    Unique {CH : CanonicalHistory B // CH.underlying = K} where
 190  default := ⟨ofComplex K, rfl⟩
 191  uniq := by
 192    intro ⟨CH, hK⟩
 193    apply Subtype.ext
 194    apply CanonicalHistory.ext
 195    -- `hK : CH.underlying = K` (after unfold); rewrite under `canonicalHistory`.
 196    calc
 197      CH.H = canonicalHistory CH.underlying := CH.toPosted_eq_canonicalHistory
 198      _ = canonicalHistory K := congrArg canonicalHistory hK
 199      _ = (ofComplex K).H := rfl
 200
 201/-- Counted histories ↔ labeled complexes; the state-canonicality fiber
 202collapses by `toPosted_eq_canonicalHistory` / `fiber_unique`. -/
 203def equivUnderlying : CanonicalHistory B ≃ BoundedComplex B where
 204  toFun := underlying
 205  invFun := ofComplex
 206  left_inv := fun CH => by
 207    -- Need `ofComplex (underlying CH) = CH`. After `ext`, Lean asks for
 208    -- `(ofComplex _).H = CH.H`, i.e. the symmetric of `toPosted_eq_canonicalHistory`.
 209    refine CanonicalHistory.ext ?_
 210    change canonicalHistory CH.underlying = CH.H
 211    exact (CH.toPosted_eq_canonicalHistory).symm
 212  right_inv := fun _ => rfl
 213
 214instance instFinite : Finite (CanonicalHistory B) :=
 215  Finite.of_equiv _ equivUnderlying.symm
 216
 217@[simp] theorem classOf_ofComplex (K : BoundedComplex B) :
 218    (ofComplex K).classOf = Quotient.mk (relabelSetoid B) K :=
 219  rfl
 220
 221@[simp] theorem toPosted_ofComplex (K : BoundedComplex B) :
 222    (ofComplex K).toPosted = canonicalHistory K :=
 223  rfl
 224
 225@[simp] theorem underlying_ofComplex (K : BoundedComplex B) :
 226    (ofComplex K).underlying = K :=
 227  rfl
 228
 229end CanonicalHistory
 230
 231/-! ## §3. History relabeling (posting-level gauge redundancy) -/
 232
 233/-- Alphabet transport induced by index bijections. -/
 234def postingAlphEquiv {K K' : BoundedComplex B}
 235    (vEquiv : Fin K.nV ≃ Fin K'.nV)
 236    (eEquiv : Fin K.nE ≃ Fin K'.nE)
 237    (tEquiv : Fin K.nT ≃ Fin K'.nT) :
 238    PostingAlphabet K ≃ PostingAlphabet K' :=
 239  Equiv.sumCongr vEquiv (Equiv.sumCongr eEquiv tEquiv)
 240
 241/-- **History relabeling (posting-level).** Index bijections together with
 242incidence preservation (as in `Relabel`) AND posting-transport compatibility:
 243the alphabet transport induced by the index bijections must commute with the
 244canonical vertex/edge/tet posting maps. This is a genuinely different
 245structure from `Relabel`; agreement is a theorem, not a definition. -/
 246structure HistoryRelabel {B : ℕ} (H H' : PostedBoundedHistory B) where
 247  vEquiv : Fin H.K.nV ≃ Fin H'.K.nV
 248  eEquiv : Fin H.K.nE ≃ Fin H'.K.nE
 249  tEquiv : Fin H.K.nT ≃ Fin H'.K.nT
 250  edge_comm : ∀ e : Fin H.K.nE,
 251    H'.K.edgeVerts (eEquiv e) = Prod.map vEquiv vEquiv (H.K.edgeVerts e)
 252  tet_comm : ∀ (t : Fin H.K.nT) (i : Fin 4),
 253    H'.K.tetVerts (tEquiv t) i = vEquiv (H.K.tetVerts t i)
 254  vertexPost_comm : ∀ v : Fin H.K.nV,
 255    H'.vertexPost (vEquiv v) =
 256      postingAlphEquiv vEquiv eEquiv tEquiv (H.vertexPost v)
 257  edgePost_comm : ∀ e : Fin H.K.nE,
 258    H'.edgePost (eEquiv e) =
 259      postingAlphEquiv vEquiv eEquiv tEquiv (H.edgePost e)
 260  tetPost_comm : ∀ t : Fin H.K.nT,
 261    H'.tetPost (tEquiv t) =
 262      postingAlphEquiv vEquiv eEquiv tEquiv (H.tetPost t)
 263
 264namespace HistoryRelabel
 265
 266variable {B : ℕ} {H H' : PostedBoundedHistory B}
 267
 268/-- Forget posting-transport fields to obtain a complex `Relabel`. -/
 269def toRelabel (r : HistoryRelabel H H') : Relabel H.K H'.K where
 270  vEquiv := r.vEquiv
 271  eEquiv := r.eEquiv
 272  tEquiv := r.tEquiv
 273  edge_comm := r.edge_comm
 274  tet_comm := r.tet_comm
 275
 276/-- Transport a complex `Relabel` to a posting-level `HistoryRelabel` by
 277equipping the induced alphabet transport; posting-commutation holds by the
 278canonical definition of `vertexPost` / `edgePost` / `tetPost`. -/
 279def ofRelabel (r : Relabel H.K H'.K) : HistoryRelabel H H' where
 280  vEquiv := r.vEquiv
 281  eEquiv := r.eEquiv
 282  tEquiv := r.tEquiv
 283  edge_comm := r.edge_comm
 284  tet_comm := r.tet_comm
 285  vertexPost_comm := fun _ => rfl
 286  edgePost_comm := fun _ => rfl
 287  tetPost_comm := fun _ => rfl
 288
 289/-- Extensionality: a history relabeling is determined by its index
 290bijections (commutation / posting fields are propositions). -/
 291@[ext] theorem ext {r s : HistoryRelabel H H'}
 292    (hv : r.vEquiv = s.vEquiv) (he : r.eEquiv = s.eEquiv)
 293    (ht : r.tEquiv = s.tEquiv) : r = s := by
 294  cases r; cases s
 295  cases hv; cases he; cases ht
 296  rfl
 297
 298end HistoryRelabel
 299
 300/-- Posting-level history relabeling is equivalent to complex relabeling.
 301Constructed (forget posting fields / equip induced alphabet transport);
 302not `Equiv.refl`, not definitional. -/
 303def historyRelabel_equiv_relabel (H H' : PostedBoundedHistory B) :
 304    HistoryRelabel H H' ≃ Relabel H.K H'.K where
 305  toFun := HistoryRelabel.toRelabel
 306  invFun := HistoryRelabel.ofRelabel
 307  left_inv := fun r => by
 308    apply HistoryRelabel.ext
 309    · rfl
 310    · rfl
 311    · rfl
 312  right_inv := fun r => by
 313    cases r
 314    rfl
 315
 316/-- On canonical presentations, specialize the general equivalence. -/
 317def historyRelabel_equiv_relabel_canonical (K K' : BoundedComplex B) :
 318    HistoryRelabel (canonicalHistory K) (canonicalHistory K') ≃ Relabel K K' :=
 319  historyRelabel_equiv_relabel (canonicalHistory K) (canonicalHistory K')
 320
 321instance instFiniteHistoryRelabel (H H' : PostedBoundedHistory B) :
 322    Finite (HistoryRelabel H H') :=
 323  Finite.of_equiv _ (historyRelabel_equiv_relabel H H').symm
 324
 325/-! ## §4. History counting (definitional layer: no Aut / mu / banked mass) -/
 326
 327/-- Number of counted histories presenting class `c`.
 328DEFINITION: history class cardinality only. -/
 329noncomputable def historyOrbitCardClass (c : TriangulationClass B) : ℕ :=
 330  Nat.card {H : CanonicalHistory B // H.classOf = c}
 331
 332/-- History gauge volume of class `c`: pairs `(H, r)` with `H` presenting `c`
 333and `r` a history relabeling from the canonical presentation of `Quotient.out c`
 334to `H`. DEFINITION: history / HistoryRelabel cardinality only. -/
 335noncomputable def historyPairCountClass (c : TriangulationClass B) : ℕ :=
 336  Nat.card
 337    (Σ H : {H : CanonicalHistory B // H.classOf = c},
 338      HistoryRelabel (canonicalHistory (Quotient.out c)) H.val.toPosted)
 339
 340/-- Trivial enrichment carrier (keeps the `Enrich → …` shape of `nuBuild`
 341without carrying Aut/mu data). -/
 342structure GaugeHistoryEnrichment : Type where
 343  mk ::
 344
 345/-- **History-built class mass.** Labeled history copies per unit of history
 346gauge volume. DEFINITION mentions only `historyOrbitCardClass` and
 347`historyPairCountClass`. -/
 348noncomputable def nuBuild (_E : GaugeHistoryEnrichment) (B : ℕ)
 349    (c : TriangulationClass B) : ℝ :=
 350  (historyOrbitCardClass c : ℝ) / (historyPairCountClass c : ℝ)
 351
 352/-- **History-only definitional certificate.** `nuBuild` is definitionally
 353the history-count quotient — not `gaugeOrbitMass`, not `1/|Aut|`. Paired with
 354`circularNu_def_is_gaugeOrbitMass` this is the mechanical non-circularity
 355audit surface. -/
 356theorem nuBuild_def_history_only :
 357    nuBuild =
 358      fun (_E : GaugeHistoryEnrichment) (B : ℕ) (c : TriangulationClass B) =>
 359        (historyOrbitCardClass c : ℝ) / (historyPairCountClass c : ℝ) :=
 360  rfl
 361
 362/-! ## §5. Bridge layer (may mention banked orbit / pair counts) -/
 363
 364/-- Counted histories of class `c` ↔ labeled complexes with class `c`.
 365Routes through the state-carrying counted type; the state-canonicality fiber
 366is collapsed by `CanonicalHistory.equivUnderlying` / `fiber_unique`. -/
 367def history_class_equiv_mk (c : TriangulationClass B) :
 368    {H : CanonicalHistory B // H.classOf = c} ≃
 369      {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c} where
 370  toFun H := ⟨H.val.underlying, H.property⟩
 371  invFun K := ⟨CanonicalHistory.ofComplex K.val, K.property⟩
 372  left_inv := fun H => by
 373    apply Subtype.ext
 374    exact CanonicalHistory.equivUnderlying.left_inv H.val
 375  right_inv := fun _ => rfl
 376
 377/-- Labeled complexes of class `c` ↔ the relabeling orbit of `Quotient.out c`
 378(banked pattern from `ExactShellGaugePreflight`). -/
 379def class_mk_equiv_orbit (c : TriangulationClass B) :
 380    {K : BoundedComplex B // Quotient.mk (relabelSetoid B) K = c} ≃
 381      {K' : BoundedComplex B // Equivalent (Quotient.out c) K'} := by
 382  have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c :=
 383    Quotient.out_eq c
 384  exact Equiv.subtypeEquivRight fun K =>
 385    ⟨fun hK => Quotient.exact (hc.trans hK.symm),
 386     fun hE => by
 387       have h1 :
 388           Quotient.mk (relabelSetoid B) (Quotient.out c) =
 389             Quotient.mk (relabelSetoid B) K :=
 390         Quotient.sound hE
 391       exact h1.symm.trans hc⟩
 392
 393/-- History class fiber ↔ banked gauge orbit of the out-representative. -/
 394def history_class_equiv_orbit (c : TriangulationClass B) :
 395    {H : CanonicalHistory B // H.classOf = c} ≃
 396      {K' : BoundedComplex B // Equivalent (Quotient.out c) K'} :=
 397  (history_class_equiv_mk c).trans (class_mk_equiv_orbit c)
 398
 399theorem historyOrbitCardClass_eq_orbitCardClass (c : TriangulationClass B) :
 400    historyOrbitCardClass c = orbitCardClass c := by
 401  have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c :=
 402    Quotient.out_eq c
 403  unfold historyOrbitCardClass
 404  rw [Nat.card_congr (history_class_equiv_orbit c)]
 405  have hcard :
 406      Nat.card {K' : BoundedComplex B // Equivalent (Quotient.out c) K'} =
 407        gaugeOrbitCard (Quotient.out c) :=
 408    rfl
 409  rw [hcard]
 410  conv_rhs => rw [← hc]
 411  rfl
 412
 413/-- History-pair sigma ↔ banked pair sigma on the out-representative.
 414Uses the `historyRelabel_equiv_relabel` equivalence, not `Equiv.refl`.
 415`H.val.toPosted.K` is definitionally `H.val.underlying`, matching the
 416orbit representative produced by `history_class_equiv_orbit`. -/
 417def history_pair_equiv_pair (c : TriangulationClass B) :
 418    (Σ H : {H : CanonicalHistory B // H.classOf = c},
 419        HistoryRelabel (canonicalHistory (Quotient.out c)) H.val.toPosted) ≃
 420      (Σ K' : {K' : BoundedComplex B // Equivalent (Quotient.out c) K'},
 421        Relabel (Quotient.out c) K'.val) :=
 422  Equiv.sigmaCongr (history_class_equiv_orbit c) fun H =>
 423    historyRelabel_equiv_relabel
 424      (canonicalHistory (Quotient.out c)) H.val.toPosted
 425
 426theorem historyPairCountClass_eq_pairCountClass (c : TriangulationClass B) :
 427    historyPairCountClass c = pairCountClass c := by
 428  have hc : Quotient.mk (relabelSetoid B) (Quotient.out c) = c :=
 429    Quotient.out_eq c
 430  unfold historyPairCountClass
 431  rw [Nat.card_congr (history_pair_equiv_pair c)]
 432  have hcard :
 433      Nat.card
 434          (Σ K' : {K' : BoundedComplex B // Equivalent (Quotient.out c) K'},
 435            Relabel (Quotient.out c) K'.val) =
 436        pairCount (Quotient.out c) :=
 437    rfl
 438  rw [hcard]
 439  conv_rhs => rw [← hc]
 440  rfl
 441
 442theorem historyPairCountClass_pos (c : TriangulationClass B) :
 443    0 < historyPairCountClass c := by
 444  rw [historyPairCountClass_eq_pairCountClass]
 445  exact pairCountClass_pos c
 446
 447/-! ## §6. Headlines -/
 448
 449/-- **HEADLINE.** The history-built mass satisfies normalized gauge counting. -/
 450theorem nuBuild_gaugeCounting (E : GaugeHistoryEnrichment) (B : ℕ) :
 451    GaugeCountingPrinciple (nuBuild E B) := by
 452  intro c
 453  unfold nuBuild
 454  have hp : (pairCountClass c : ℝ) ≠ 0 := by
 455    exact_mod_cast (pairCountClass_pos c).ne'
 456  rw [historyOrbitCardClass_eq_orbitCardClass,
 457    historyPairCountClass_eq_pairCountClass, div_mul_cancel₀ _ hp]
 458
 459/-- **HEADLINE.** History-built mass equals the banked gauge-orbit mass,
 460derived via the counting-principle uniqueness IFF — not by definitional
 461unfolding of `nuBuild` to `gaugeOrbitMass`. -/
 462theorem nuBuild_eq_gaugeOrbitMass (E : GaugeHistoryEnrichment) (B : ℕ) :
 463    nuBuild E B = gaugeOrbitMass :=
 464  (gaugeCountingPrinciple_iff_eq_gaugeOrbitMass (nuBuild E B)).mp
 465    (nuBuild_gaugeCounting E B)
 466
 467/-! ## §7. Named-witness discharge (route (b); no fake ∃-package) -/
 468
 469/-- **HEADLINE.** Gap2 gauge-counting from history, discharged for the named
 470builder `nuBuild`: counting principle + equality via uniqueness IFF.
 471Non-circularity is certified outside this Prop by the definition text of
 472`nuBuild` and the paired `rfl` certificates `nuBuild_def_history_only` /
 473`circularNu_def_is_gaugeOrbitMass`. -/
 474theorem gap2_gauge_counting_from_history_discharged :
 475    (∀ (E : GaugeHistoryEnrichment) (B : ℕ),
 476      GaugeCountingPrinciple (nuBuild E B)) ∧
 477    (∀ (E : GaugeHistoryEnrichment) (B : ℕ),
 478      nuBuild E B = gaugeOrbitMass) :=
 479  ⟨nuBuild_gaugeCounting, nuBuild_eq_gaugeOrbitMass⟩
 480
 481/-- Compatibility Prop for downstream DAG wiring. States the named-witness
 482discharge; does **not** claim an `∃`-package discharges non-circularity. -/
 483def TypedResidual_gap2_gauge_counting_from_history : Prop :=
 484  (∀ (E : GaugeHistoryEnrichment) (B : ℕ),
 485    GaugeCountingPrinciple (nuBuild E B)) ∧
 486  (∀ (E : GaugeHistoryEnrichment) (B : ℕ),
 487    nuBuild E B = gaugeOrbitMass)
 488
 489/-- **HEADLINE.** R5 closed by the named posted-history construction. -/
 490theorem typedResidual_gap2_gauge_counting_from_history_closed :
 491    TypedResidual_gap2_gauge_counting_from_history :=
 492  gap2_gauge_counting_from_history_discharged
 493
 494theorem TypedResidual_gap2_gauge_counting_from_history_closed :
 495    TypedResidual_gap2_gauge_counting_from_history :=
 496  typedResidual_gap2_gauge_counting_from_history_closed
 497
 498/-! ## §8. Decoys (paired `rfl` audit surface) -/
 499
 500/-- **Circular decoy:** mass defined as the banked gauge-orbit mass.
 501Satisfies `GaugeCountingPrinciple`, but is definitionally the banked mass
 502(`circularNu_def_is_gaugeOrbitMass`), so it cannot supply the history-only
 503`rfl` certificate `nuBuild_def_history_only`. -/
 504def circularNu (_E : GaugeHistoryEnrichment) :
 505    ∀ B, TriangulationClass B → ℝ :=
 506  fun _B => gaugeOrbitMass
 507
 508theorem circularNu_def_is_gaugeOrbitMass :
 509    circularNu =
 510      fun (_E : GaugeHistoryEnrichment) (_B : ℕ) =>
 511        (gaugeOrbitMass : TriangulationClass _ → ℝ) :=
 512  rfl
 513
 514theorem circularNu_satisfies_gaugeCounting
 515    (E : GaugeHistoryEnrichment) (B : ℕ) :
 516    GaugeCountingPrinciple (circularNu E B) :=
 517  gaugeOrbitMass_satisfies
 518
 519/-- Uniform class-mass decoy fails gauge counting (re-export). -/
 520theorem decoy_uniformClassMass_not_gaugeCounting (B : ℕ) (hB : 2 ≤ B) :
 521    ¬ GaugeCountingPrinciple
 522      (uniformClassMass : TriangulationClass B → ℝ) :=
 523  uniformClassMass_not_gaugeCounting B hB
 524
 525/-- Audit package: paired `rfl` certificates distinguish `nuBuild` from
 526`circularNu`; counting holds for `nuBuild` and fails for uniform. -/
 527theorem gap2_history_measure_decoy_anchors (B : ℕ) (hB : 2 ≤ B) :
 528    (nuBuild =
 529        fun (_E : GaugeHistoryEnrichment) (B : ℕ) (c : TriangulationClass B) =>
 530          (historyOrbitCardClass c : ℝ) / (historyPairCountClass c : ℝ)) ∧
 531      (circularNu = fun _ _ => gaugeOrbitMass) ∧
 532      GaugeCountingPrinciple
 533        (circularNu GaugeHistoryEnrichment.mk B) ∧
 534      ¬ GaugeCountingPrinciple
 535        (uniformClassMass : TriangulationClass B → ℝ) ∧
 536      GaugeCountingPrinciple
 537        (nuBuild GaugeHistoryEnrichment.mk B) ∧
 538      nuBuild GaugeHistoryEnrichment.mk B = gaugeOrbitMass :=
 539  ⟨nuBuild_def_history_only, circularNu_def_is_gaugeOrbitMass,
 540    circularNu_satisfies_gaugeCounting _ B,
 541    decoy_uniformClassMass_not_gaugeCounting B hB,
 542    nuBuild_gaugeCounting _ B, nuBuild_eq_gaugeOrbitMass _ B⟩
 543
 544end
 545
 546end GaugeHistoryMeasure
 547end SevenGaps
 548end Gravity
 549end IndisputableMonolith
 550