IndisputableMonolith.Gravity.SevenGaps.MeasureInvarianceNoGo

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
   3
   4/-!
   5# Seven Gaps, Lane D1: invariance alone does not determine the path-sum measure
   6
   7## What this module proves (KILL + WITNESS)
   8
   9**Status: THEOREM (kernel no-go with explicit witnesses).**  The killed
  10prior attempt "mu-from-invariance" claimed that relabeling invariance
  11(plus the obvious positivity and normalization requirements) singles out
  12the symmetry-factor measure `mu = 1/|Aut|` on the scoped path-sum
  13configuration class.  That positive claim stays dead.  This module proves
  14the corresponding NO-GO as a kernel fact:
  15
  16* `InvarianceAxioms` names the invariance-type properties used here, each
  17  stateable against the existing Lean machinery: relabeling invariance
  18  (the measure is a class function for `relabelSetoid`),
  19  strict positivity, per-configuration normalization `w K <= 1`, and the
  20  unit normalization `w(empty) = 1` on the canonical empty configuration.
  21  The no-go is scoped to THIS named set; a strictly richer axiom set
  22  (gluing/factorization, orbit-stabilizer, substrate structure) could in
  23  principle restore uniqueness, and that possibility is exactly the OPEN
  24  substrate-derivation frontier.
  25* THREE genuinely different weight functions satisfy ALL of the named
  26  axioms: the symmetry-factor measure `mu = 1/|Aut|` (`muMeasure`), the
  27  uniform weight `1` (`uniformMeasure`), and the squared symmetry factor
  28  `1/|Aut|^2` (`muSqMeasure`).  In fact a countably infinite injective
  29  family does (`muPowMeasure`, `invariance_admits_infinite_measure_family`).
  30* The separation is witnessed concretely, not abstractly: the two-vertex
  31  edgeless configuration `twoPointComplex` has automorphism group of
  32  cardinality exactly 2 (`autCard_twoPointComplex`, via the explicit
  33  equivalence `twoPointAutEquiv` with the permutation triple), so
  34  `mu = 1/2 < 1` there (`mu_twoPointComplex`) while the uniform weight
  35  is `1`.
  36* **Headline:** `mu_not_determined_by_invariance`.  Both candidate
  37  measures satisfy the named axioms and they are unequal, with the
  38  pointwise strict inequality exhibited.  Invariance alone underdetermines
  39  the path-sum measure.
  40
  41## What this module does NOT prove (binding honesty disclosures)
  42
  43* It does NOT resurrect the positive claim that invariance fixes
  44  `1/|Aut|`; it refutes exactly that determination claim.
  45* It does NOT derive the `1/|Aut|` measure from recognition-ledger
  46  substrate axioms.  `substrate_measure_derived` stays RED (OPEN): no
  47  named substrate axiom set in the existing Lean forces a unique measure,
  48  and this module shows the invariance-type axioms stateable against the
  49  existing `PathSumMeasure` machinery cannot.  A future derivation would
  50  need strictly richer named substrate structure.
  51* A disjoint-union / gluing factorization axiom is NOT included in
  52  `InvarianceAxioms`, because the existing `BoundedComplex` machinery
  53  carries no disjoint-union operation to state it against.  The no-go is
  54  scoped to the axioms actually named; this scope is disclosed here and
  55  in `measureInvarianceNoGoStatus`.
  56* Nothing here concerns the continuum limit (`Z_RS_continuum_limit`
  57  stays RED / OPEN), and no `FullTheoryLedger` flag is touched.
  58
  59## Status tiers (honest tagging)
  60
  61**THEOREM (proved below, 0 sorry, 0 new axioms, no `native_decide`):**
  62`autCard_emptyComplex`, `mu_emptyComplex`, `autCard_twoPointComplex`,
  63`mu_twoPointComplex`, `muMeasure_satisfies`, `uniformMeasure_satisfies`,
  64`muSqMeasure_satisfies`, `muPowMeasure_satisfies`,
  65`mu_not_determined_by_invariance`, `invariance_underdetermines_measure`,
  66`invariance_admits_infinite_measure_family`.
  67
  68**MODEL (definitional, inherited):** the scoped configuration class
  69`BoundedComplex` and the `1/|Aut|` convention itself, from
  70`PathSumMeasure`.
  71
  72**OPEN (recorded, never claimed):** a substrate-DERIVED unique measure;
  73the continuum limit.
  74
  75Expected axiom footprint: standard trio
  76`[propext, Classical.choice, Quot.sound]`.
  77-/
  78
  79namespace IndisputableMonolith
  80namespace Gravity
  81namespace SevenGaps
  82namespace MeasureInvarianceNoGo
  83
  84open PathSumMeasure
  85
  86/-! ## §1. The named invariance axioms
  87
  88The invariance-type requirements on a candidate path-sum weight used by
  89this no-go: class-function invariance under `relabelSetoid`, strict
  90positivity, per-configuration normalization, and unit weight on the
  91canonical empty configuration.  A disjoint-union factorization axiom is
  92NOT stateable against the existing `BoundedComplex` inventory (no gluing
  93operation exists there); that scope limit is disclosed in the module
  94docstring, and the no-go is scoped to the axioms named here. -/
  95
  96/-- The named invariance axioms for a candidate path-sum weight `w` on the
  97scoped configuration class at cap `B`.  The no-go below is scoped to
  98exactly this axiom set. -/
  99structure InvarianceAxioms (B : ℕ) (w : BoundedComplex B → ℝ) : Prop where
 100  /-- The weight is a relabeling class function. -/
 101  relabel_invariant : ∀ K K' : BoundedComplex B, Equivalent K K' → w K = w K'
 102  /-- The weight is strictly positive. -/
 103  positive : ∀ K : BoundedComplex B, 0 < w K
 104  /-- Per-configuration normalization: no configuration outweighs the
 105  reference weight 1. -/
 106  normalized_le_one : ∀ K : BoundedComplex B, w K ≤ 1
 107  /-- Unit normalization on the canonical empty configuration. -/
 108  unital_on_empty : w (emptyComplex B) = 1
 109
 110/-- **THEOREM (normalizability on the finite scoped family).**  Any weight
 111satisfying the named axioms has finite total mass bounded by the proved
 112configuration count: the axioms already contain normalizability. -/
 113theorem InvarianceAxioms.totalMass_le_card {B : ℕ} {w : BoundedComplex B → ℝ}
 114    (h : InvarianceAxioms B w) :
 115    ∑ K : BoundedComplex B, w K ≤ (Fintype.card (BoundedComplex B) : ℝ) := by
 116  calc ∑ K : BoundedComplex B, w K
 117      ≤ ∑ _K : BoundedComplex B, (1 : ℝ) :=
 118        Finset.sum_le_sum fun K _ => h.normalized_le_one K
 119    _ = (Fintype.card (BoundedComplex B) : ℝ) := by
 120        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]
 121
 122/-! ## §2. The symmetry factor on the empty configuration -/
 123
 124/-- The automorphism group of the empty configuration is trivial: all
 125three index types are empty, so all three index bijections are forced. -/
 126instance instSubsingletonAutEmpty (B : ℕ) :
 127    Subsingleton (Aut (emptyComplex B)) :=
 128  ⟨fun _a _b => Relabel.ext
 129    (Equiv.ext fun x => x.elim0)
 130    (Equiv.ext fun x => x.elim0)
 131    (Equiv.ext fun x => x.elim0)⟩
 132
 133/-- **THEOREM.**  `|Aut(empty)| = 1`. -/
 134theorem autCard_emptyComplex (B : ℕ) :
 135    Nat.card (Aut (emptyComplex B)) = 1 :=
 136  Nat.card_unique
 137
 138/-- **THEOREM.**  The symmetry-factor measure is 1 on the empty
 139configuration, so `mu` satisfies the unit-normalization axiom. -/
 140theorem mu_emptyComplex (B : ℕ) : mu (emptyComplex B) = 1 := by
 141  unfold mu
 142  rw [autCard_emptyComplex]
 143  norm_num
 144
 145/-! ## §3. The separating witness: two vertices, no incidence
 146
 147The two-vertex edgeless configuration has a nontrivial automorphism (the
 148vertex swap), and its automorphism group is EXACTLY the permutation
 149triple `S_2 x S_0 x S_0` because the incidence commutation constraints
 150are vacuous.  So `mu = 1/2` there while the uniform weight is 1. -/
 151
 152/-- The two-vertex edgeless configuration at any cap `B >= 2`.  (`abbrev`
 153so the size fields reduce during elaboration.) -/
 154abbrev twoPointComplex (B : ℕ) (hB : 2 ≤ B) : BoundedComplex B where
 155  nV := 2
 156  nE := 0
 157  nT := 0
 158  hV := hB
 159  hE := Nat.zero_le B
 160  hT := Nat.zero_le B
 161  edgeVerts := fun e => e.elim0
 162  tetVerts := fun t => t.elim0
 163
 164/-- With no edges and no tetrahedra the commutation constraints are
 165vacuous: the automorphism group of the two-point configuration IS the
 166full triple of index permutations. -/
 167def twoPointAutEquiv (B : ℕ) (hB : 2 ≤ B) :
 168    Aut (twoPointComplex B hB) ≃
 169      ((Fin 2 ≃ Fin 2) × (Fin 0 ≃ Fin 0) × (Fin 0 ≃ Fin 0)) where
 170  toFun a := ⟨a.vEquiv, a.eEquiv, a.tEquiv⟩
 171  invFun p :=
 172    { vEquiv := p.1
 173      eEquiv := p.2.1
 174      tEquiv := p.2.2
 175      edge_comm := fun e => e.elim0
 176      tet_comm := fun t _ => t.elim0 }
 177  left_inv _ := rfl
 178  right_inv _ := rfl
 179
 180/-- **THEOREM.**  `|Aut(twoPoint)| = 2` exactly (the identity and the
 181vertex swap). -/
 182theorem autCard_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
 183    Nat.card (Aut (twoPointComplex B hB)) = 2 := by
 184  rw [Nat.card_congr (twoPointAutEquiv B hB), Nat.card_eq_fintype_card,
 185    Fintype.card_prod, Fintype.card_prod,
 186    Fintype.card_equiv (Equiv.refl (Fin 2)),
 187    Fintype.card_equiv (Equiv.refl (Fin 0)),
 188    Fintype.card_fin 2, Fintype.card_fin 0]
 189  norm_num [Nat.factorial]
 190
 191/-- **THEOREM.**  The symmetry-factor measure of the two-point witness is
 192exactly `1/2`. -/
 193theorem mu_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
 194    mu (twoPointComplex B hB) = 1 / 2 := by
 195  unfold mu
 196  rw [autCard_twoPointComplex B hB]
 197  norm_num
 198
 199/-! ## §4. The candidate measures and their axiom certificates -/
 200
 201/-- Candidate 1: the standing symmetry-factor measure `1/|Aut|`. -/
 202noncomputable def muMeasure (B : ℕ) : BoundedComplex B → ℝ := fun K => mu K
 203
 204/-- Candidate 2: the uniform weight 1. -/
 205def uniformMeasure (B : ℕ) : BoundedComplex B → ℝ := fun _ => 1
 206
 207/-- Candidate 3: the squared symmetry factor `1/|Aut|^2`. -/
 208noncomputable def muSqMeasure (B : ℕ) : BoundedComplex B → ℝ :=
 209  fun K => mu K ^ 2
 210
 211/-- A countable family of candidates: `1/|Aut|^(n+1)` for every `n`. -/
 212noncomputable def muPowMeasure (B : ℕ) (n : ℕ) : BoundedComplex B → ℝ :=
 213  fun K => mu K ^ (n + 1)
 214
 215/-- **THEOREM.**  `1/|Aut|` satisfies every named invariance axiom. -/
 216theorem muMeasure_satisfies (B : ℕ) : InvarianceAxioms B (muMeasure B) :=
 217  ⟨fun _ _ h => mu_congr h, fun K => mu_pos K, fun K => mu_le_one K,
 218    mu_emptyComplex B⟩
 219
 220/-- **THEOREM.**  The uniform weight 1 satisfies every named invariance
 221axiom. -/
 222theorem uniformMeasure_satisfies (B : ℕ) :
 223    InvarianceAxioms B (uniformMeasure B) :=
 224  ⟨fun _ _ _ => rfl, fun _ => one_pos, fun _ => le_refl 1, rfl⟩
 225
 226/-- **THEOREM.**  `1/|Aut|^2` satisfies every named invariance axiom. -/
 227theorem muSqMeasure_satisfies (B : ℕ) : InvarianceAxioms B (muSqMeasure B) :=
 228  ⟨fun K K' h => by
 229      show mu K ^ 2 = mu K' ^ 2
 230      rw [mu_congr h],
 231    fun K => pow_pos (mu_pos K) 2,
 232    fun K => pow_le_one₀ (mu_pos K).le (mu_le_one K),
 233    by
 234      show mu (emptyComplex B) ^ 2 = 1
 235      rw [mu_emptyComplex B]
 236      norm_num⟩
 237
 238/-- **THEOREM.**  Every member of the countable family satisfies every
 239named invariance axiom. -/
 240theorem muPowMeasure_satisfies (B n : ℕ) :
 241    InvarianceAxioms B (muPowMeasure B n) :=
 242  ⟨fun K K' h => by
 243      show mu K ^ (n + 1) = mu K' ^ (n + 1)
 244      rw [mu_congr h],
 245    fun K => pow_pos (mu_pos K) (n + 1),
 246    fun K => pow_le_one₀ (mu_pos K).le (mu_le_one K),
 247    by
 248      show mu (emptyComplex B) ^ (n + 1) = 1
 249      rw [mu_emptyComplex B]
 250      norm_num⟩
 251
 252/-! ## §5. The separation: the candidates are genuinely different -/
 253
 254/-- **Pointwise strict separation.**  At the two-point witness the
 255symmetry-factor measure is strictly below the uniform weight:
 256`1/2 < 1`. -/
 257theorem muMeasure_lt_uniform_at_witness (B : ℕ) (hB : 2 ≤ B) :
 258    muMeasure B (twoPointComplex B hB) <
 259      uniformMeasure B (twoPointComplex B hB) := by
 260  show mu (twoPointComplex B hB) < 1
 261  rw [mu_twoPointComplex B hB]
 262  norm_num
 263
 264/-- The two candidate measures are unequal as functions. -/
 265theorem muMeasure_ne_uniformMeasure (B : ℕ) (hB : 2 ≤ B) :
 266    muMeasure B ≠ uniformMeasure B := fun h =>
 267  absurd (congrFun h (twoPointComplex B hB))
 268    (ne_of_lt (muMeasure_lt_uniform_at_witness B hB))
 269
 270/-- The squared candidate also separates from both. -/
 271theorem muSqMeasure_separations (B : ℕ) (hB : 2 ≤ B) :
 272    muSqMeasure B ≠ uniformMeasure B ∧ muSqMeasure B ≠ muMeasure B := by
 273  constructor
 274  · intro h
 275    have hval := congrFun h (twoPointComplex B hB)
 276    have hmu : muSqMeasure B (twoPointComplex B hB) = 1 / 4 := by
 277      show mu (twoPointComplex B hB) ^ 2 = 1 / 4
 278      rw [mu_twoPointComplex B hB]
 279      norm_num
 280    rw [hmu] at hval
 281    have huni : uniformMeasure B (twoPointComplex B hB) = 1 := rfl
 282    rw [huni] at hval
 283    norm_num at hval
 284  · intro h
 285    have hval := congrFun h (twoPointComplex B hB)
 286    have hmu2 : muSqMeasure B (twoPointComplex B hB) = 1 / 4 := by
 287      show mu (twoPointComplex B hB) ^ 2 = 1 / 4
 288      rw [mu_twoPointComplex B hB]
 289      norm_num
 290    have hmu1 : muMeasure B (twoPointComplex B hB) = 1 / 2 :=
 291      mu_twoPointComplex B hB
 292    rw [hmu2, hmu1] at hval
 293    norm_num at hval
 294
 295/-! ## §6. Headline no-go theorems -/
 296
 297/-- **HEADLINE (KILL + WITNESS).**  The named invariance axioms do NOT
 298determine the path-sum measure: the symmetry-factor measure `1/|Aut|`
 299and the uniform weight 1 BOTH satisfy every named axiom, yet they are
 300unequal, with the pointwise strict inequality exhibited at the concrete
 301two-point witness (where `|Aut| = 2`).  This is the kernel refutation of
 302the killed "mu-from-invariance" determination claim; the substrate
 303derivation of a unique measure remains OPEN. -/
 304theorem mu_not_determined_by_invariance (B : ℕ) (hB : 2 ≤ B) :
 305    InvarianceAxioms B (muMeasure B) ∧
 306    InvarianceAxioms B (uniformMeasure B) ∧
 307    muMeasure B ≠ uniformMeasure B ∧
 308    muMeasure B (twoPointComplex B hB) <
 309      uniformMeasure B (twoPointComplex B hB) :=
 310  ⟨muMeasure_satisfies B, uniformMeasure_satisfies B,
 311    muMeasure_ne_uniformMeasure B hB,
 312    muMeasure_lt_uniform_at_witness B hB⟩
 313
 314/-- **Existential packaging of the headline.**  There exist two distinct
 315weight functions satisfying all the named invariance axioms. -/
 316theorem invariance_underdetermines_measure (B : ℕ) (hB : 2 ≤ B) :
 317    ∃ w₁ w₂ : BoundedComplex B → ℝ,
 318      InvarianceAxioms B w₁ ∧ InvarianceAxioms B w₂ ∧ w₁ ≠ w₂ :=
 319  ⟨muMeasure B, uniformMeasure B, muMeasure_satisfies B,
 320    uniformMeasure_satisfies B, muMeasure_ne_uniformMeasure B hB⟩
 321
 322/-- The countable family is injective: distinct exponents give distinct
 323measures (separated at the two-point witness where `mu = 1/2`). -/
 324theorem muPowMeasure_injective (B : ℕ) (hB : 2 ≤ B) :
 325    Function.Injective (muPowMeasure B) := by
 326  have hval : ∀ n : ℕ,
 327      muPowMeasure B n (twoPointComplex B hB) = (1 / 2 : ℝ) ^ (n + 1) := by
 328    intro n
 329    show mu (twoPointComplex B hB) ^ (n + 1) = (1 / 2 : ℝ) ^ (n + 1)
 330    rw [mu_twoPointComplex B hB]
 331  have hanti : StrictAnti (fun n : ℕ => ((1 : ℝ) / 2) ^ (n + 1)) := by
 332    intro a b hab
 333    exact pow_lt_pow_right_of_lt_one₀ (by norm_num) (by norm_num)
 334      (Nat.succ_lt_succ hab)
 335  intro n m h
 336  have h2 : ((1 : ℝ) / 2) ^ (n + 1) = ((1 : ℝ) / 2) ^ (m + 1) := by
 337    rw [← hval n, ← hval m, h]
 338  exact hanti.injective h2
 339
 340/-- **HEADLINE (strengthened form).**  The named invariance axioms admit a
 341countably INFINITE injective family of measures `1/|Aut|^(n+1)`: the
 342underdetermination is not a two-point accident. -/
 343theorem invariance_admits_infinite_measure_family (B : ℕ) (hB : 2 ≤ B) :
 344    (∀ n : ℕ, InvarianceAxioms B (muPowMeasure B n)) ∧
 345      Function.Injective (muPowMeasure B) :=
 346  ⟨muPowMeasure_satisfies B, muPowMeasure_injective B hB⟩
 347
 348/-! ## §7. Status record (honest boundary; RED flags stay RED) -/
 349
 350/-- Status record for the measure-invariance no-go.  Every `true` flag is
 351tied to its kernel theorem by the grounding theorem below; the RED flags
 352stay false. -/
 353structure MeasureInvarianceNoGoStatus where
 354  /-- §1: `InvarianceAxioms` names the stateable invariance properties. -/
 355  named_axioms_stated : Bool
 356  /-- §4: `muMeasure_satisfies`. -/
 357  mu_satisfies_axioms : Bool
 358  /-- §4: `uniformMeasure_satisfies`. -/
 359  uniform_satisfies_axioms : Bool
 360  /-- §6: `mu_not_determined_by_invariance`. -/
 361  measures_separated : Bool
 362  /-- §6: `invariance_admits_infinite_measure_family`. -/
 363  infinite_family_exhibited : Bool
 364  /-- Disclosed scope limit: no disjoint-union factorization axiom is
 365  stateable against the existing `BoundedComplex` machinery. -/
 366  factorization_axiom_stateable : Bool
 367  /-- RED (OPEN): no substrate derivation of a unique measure exists;
 368  this module proves the named invariance axioms cannot supply one. -/
 369  substrate_measure_derived : Bool
 370  /-- RED (OPEN). -/
 371  Z_RS_continuum_limit : Bool
 372
 373/-- The canonical status record. -/
 374def measureInvarianceNoGoStatus : MeasureInvarianceNoGoStatus where
 375  named_axioms_stated := true
 376  mu_satisfies_axioms := true
 377  uniform_satisfies_axioms := true
 378  measures_separated := true
 379  infinite_family_exhibited := true
 380  factorization_axiom_stateable := false
 381  substrate_measure_derived := false
 382  Z_RS_continuum_limit := false
 383
 384/-- **Grounding theorem.**  Every `true` status flag is tied to a kernel
 385statement; the RED flags remain false. -/
 386theorem measureInvarianceNoGoStatus_grounded :
 387    (measureInvarianceNoGoStatus.named_axioms_stated = true ∧
 388      ∀ B : ℕ, ∃ w : BoundedComplex B → ℝ, InvarianceAxioms B w) ∧
 389    (measureInvarianceNoGoStatus.mu_satisfies_axioms = true ∧
 390      ∀ B : ℕ, InvarianceAxioms B (muMeasure B)) ∧
 391    (measureInvarianceNoGoStatus.uniform_satisfies_axioms = true ∧
 392      ∀ B : ℕ, InvarianceAxioms B (uniformMeasure B)) ∧
 393    (measureInvarianceNoGoStatus.measures_separated = true ∧
 394      ∀ B : ℕ, 2 ≤ B → muMeasure B ≠ uniformMeasure B) ∧
 395    (measureInvarianceNoGoStatus.infinite_family_exhibited = true ∧
 396      (∀ B n : ℕ, InvarianceAxioms B (muPowMeasure B n)) ∧
 397      ∀ B : ℕ, 2 ≤ B → Function.Injective (muPowMeasure B)) ∧
 398    measureInvarianceNoGoStatus.factorization_axiom_stateable = false ∧
 399    measureInvarianceNoGoStatus.substrate_measure_derived = false ∧
 400    measureInvarianceNoGoStatus.Z_RS_continuum_limit = false :=
 401  ⟨⟨rfl, fun B => ⟨uniformMeasure B, uniformMeasure_satisfies B⟩⟩,
 402    ⟨rfl, muMeasure_satisfies⟩,
 403    ⟨rfl, uniformMeasure_satisfies⟩,
 404    ⟨rfl, muMeasure_ne_uniformMeasure⟩,
 405    ⟨rfl, fun B n => muPowMeasure_satisfies B n, muPowMeasure_injective⟩,
 406    rfl, rfl, rfl⟩
 407
 408#print axioms mu_not_determined_by_invariance
 409#print axioms invariance_underdetermines_measure
 410#print axioms invariance_admits_infinite_measure_family
 411#print axioms measureInvarianceNoGoStatus_grounded
 412
 413end MeasureInvarianceNoGo
 414end SevenGaps
 415end Gravity
 416end IndisputableMonolith
 417