IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker

   1import IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight
   2import IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo
   3
   4/-!
   5# Path-sum measure: exact substrate blocker
   6
   7## Status: THEOREM
   8
   9`MeasureInvarianceNoGo` proves that relabeling invariance, positivity, and
  10normalization do not select a path-sum measure. `ExactShellGaugePreflight`
  11proves that the gauge-counting mass equals `1 / |Aut|`, while recording the
  12uniform gauge-density principle as a MODEL premise.
  13
  14This file identifies that premise exactly. A class mass satisfies normalized
  15gauge counting if its mass times the number of `(labeled copy, relabeling
  16witness)` pairs equals the number of labeled copies. The main equivalence says
  17that this principle holds exactly when every class has the `1 / |Aut|` mass.
  18
  19The explicit two-point class proves the principle has real content: the
  20quotient-uniform class mass fails it. Thus the remaining substrate task cannot
  21be discharged by the invariance axioms or by renaming uniform quotient
  22counting. It requires a derivation of normalized gauge counting from richer
  23ledger structure. This module supplies the certified blocker and flips no
  24`FullTheoryLedger` flag.
  25
  26No `sorry`, `admit`, new axiom, or `native_decide`.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Gravity
  31namespace SevenGaps
  32namespace MeasureSubstrateBlocker
  33
  34open PathSumMeasure
  35open ExactShellGaugePreflight
  36
  37noncomputable section
  38
  39/-- The exact extra principle used by the gauge-counting derivation: class
  40mass times gauge-witness volume equals labeled orbit size. -/
  41def GaugeCountingPrinciple {B : ℕ}
  42    (ν : TriangulationClass B → ℝ) : Prop :=
  43  ∀ c, ν c * (pairCountClass c : ℝ) = (orbitCardClass c : ℝ)
  44
  45/-- The counting-defined mass satisfies normalized gauge counting. -/
  46theorem gaugeOrbitMass_satisfies {B : ℕ} :
  47    GaugeCountingPrinciple (gaugeOrbitMass :
  48      TriangulationClass B → ℝ) :=
  49  gaugeOrbitMass_mul_pairCount
  50
  51/-- Normalized gauge counting selects exactly the counting-defined mass.
  52This packages existence and uniqueness in one equivalence. -/
  53theorem gaugeCountingPrinciple_iff_eq_gaugeOrbitMass {B : ℕ}
  54    (ν : TriangulationClass B → ℝ) :
  55    GaugeCountingPrinciple ν ↔ ν = gaugeOrbitMass := by
  56  constructor
  57  · intro hν
  58    funext c
  59    exact gaugeCountingMass_unique ν hν c
  60  · intro hν
  61    subst hν
  62    exact gaugeOrbitMass_satisfies
  63
  64/-- **Exact blocker theorem.** Normalized gauge counting is equivalent to
  65assigning `1 / |Aut K|` to every represented bounded complex. The forward
  66direction is the orbit-stabilizer derivation. The reverse direction shows
  67that no weaker unnamed condition is hidden in the counting statement. -/
  68theorem gaugeCountingPrinciple_iff_mu_on_representatives {B : ℕ}
  69    (ν : TriangulationClass B → ℝ) :
  70    GaugeCountingPrinciple ν ↔
  71      ∀ K : BoundedComplex B,
  72        ν (Quotient.mk (relabelSetoid B) K) = mu K := by
  73  rw [gaugeCountingPrinciple_iff_eq_gaugeOrbitMass]
  74  constructor
  75  · intro hν K
  76    rw [hν]
  77    exact gaugeOrbitMass_eq_mu K
  78  · intro hν
  79    funext c
  80    refine Quotient.inductionOn c ?_
  81    intro K
  82    exact (hν K).trans (gaugeOrbitMass_eq_mu K).symm
  83
  84/-- Uniform mass on quotient classes. This is the live decoy admitted by
  85the weaker invariance requirements. -/
  86def uniformClassMass {B : ℕ} : TriangulationClass B → ℝ :=
  87  fun _ => 1
  88
  89/-- The quotient-uniform decoy fails normalized gauge counting on the
  90two-point class, where the required mass is `1/2`. This proves that the
  91extra principle is discriminating and does not restate class invariance. -/
  92theorem uniformClassMass_not_gaugeCounting (B : ℕ) (hB : 2 ≤ B) :
  93    ¬ GaugeCountingPrinciple
  94      (uniformClassMass : TriangulationClass B → ℝ) := by
  95  intro h
  96  have hmu :=
  97    (gaugeCountingPrinciple_iff_mu_on_representatives
  98      (uniformClassMass : TriangulationClass B → ℝ)).mp h
  99      (MeasureInvarianceNoGo.twoPointComplex B hB)
 100  unfold uniformClassMass at hmu
 101  rw [MeasureInvarianceNoGo.mu_twoPointComplex B hB] at hmu
 102  norm_num at hmu
 103
 104/-- **Certified blocker package.** Gauge counting exists and selects
 105`1/|Aut|`; the quotient-uniform decoy fails it. What remains is precisely a
 106ledger theorem supplying `GaugeCountingPrinciple`, not more invariance. -/
 107theorem substrate_measure_blocker_certificate (B : ℕ) (hB : 2 ≤ B) :
 108    GaugeCountingPrinciple
 109        (gaugeOrbitMass : TriangulationClass B → ℝ) ∧
 110      (∀ ν : TriangulationClass B → ℝ,
 111        GaugeCountingPrinciple ν ↔
 112          ∀ K : BoundedComplex B,
 113            ν (Quotient.mk (relabelSetoid B) K) = mu K) ∧
 114      ¬ GaugeCountingPrinciple
 115        (uniformClassMass : TriangulationClass B → ℝ) :=
 116  ⟨gaugeOrbitMass_satisfies,
 117    gaugeCountingPrinciple_iff_mu_on_representatives,
 118    uniformClassMass_not_gaugeCounting B hB⟩
 119
 120end
 121
 122end MeasureSubstrateBlocker
 123end SevenGaps
 124end Gravity
 125end IndisputableMonolith
 126
 127#print axioms IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker.gaugeCountingPrinciple_iff_mu_on_representatives
 128#print axioms IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker.uniformClassMass_not_gaugeCounting
 129#print axioms IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker.substrate_measure_blocker_certificate
 130