IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerSiteBlindness

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker
   3import IndisputableMonolith.Gravity.RecognitionLedger
   4
   5/-!
   6# Gap 2, R2: the recognition ledger's site symmetry cannot supply gauge counting
   7
   8A scoped no-go for the open measure obligation. The obligation is a proof of
   9`GaugeCountingPrinciple` in which some recognition-substrate premise is
  10load-bearing. This module shows that one whole shape of candidate premise is
  11dead, and names what any derivation must import instead.
  12
  13The shape: read the measure off the SITE SYMMETRY of a recognition ledger, that
  14is, off how many relabelings of the site type leave the ledger's cost unchanged.
  15This is the natural first move, because orbit-stabilizer already converts a
  16symmetry count into `1/|Aut|` and the ledger is the substrate's only carrier of
  17cost.
  18
  19The obstruction is that two of the ledger's own axioms make it blind at the
  20smallest size where the target has anything to say. On a two-element site type a
  21recognition ledger is a symmetric matrix with zero diagonal, so it is determined
  22by the single number `cost 0 1`, and the transposition therefore fixes EVERY such
  23ledger. Meanwhile two two-vertex complexes have different automorphism counts:
  24the edgeless pair has `|Aut| = 2` and the single directed edge has `|Aut| = 1`,
  25because `Relabel.edge_comm` compares ORDERED endpoint pairs and a symmetric cost
  26cannot see an orientation.
  27
  28So the site-symmetry count is 2 for both, while gauge counting demands masses
  29`1/2` and `1`. No measure that factors through the site-symmetry count can be
  30right.
  31
  32## What this licenses, exactly
  33
  34Under the premise that the candidate measure factors through the ledger's
  35site-symmetry count on the vertex site type, gauge counting fails. That is one
  36conditional and this module claims no more. It does NOT say the ledger cannot
  37supply the measure by some other route, and it does not touch any status flag.
  38
  39What it does supply is the named import: any derivation must bring structure
  40that separates the edgeless pair from the single directed edge. Ledger cost on
  41vertex sites provably does not, so the import is either an orientation-carrying
  42refinement of the ledger, or sites for simplices rather than for vertices alone.
  43
  44Status: THEOREM. Expected axiom footprint `[propext, Classical.choice,
  45Quot.sound]`.
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Gravity
  50namespace SevenGaps
  51namespace Gap2LedgerSiteBlindness
  52
  53open PathSumMeasure
  54open ExactShellGaugePreflight
  55open MeasureSubstrateBlocker
  56open MeasureInvarianceNoGo
  57open IndisputableMonolith.Gravity.RecognitionLedger
  58
  59/-! ## §1. The second witness: two vertices joined by one directed edge -/
  60
  61/-- Two vertices and a single edge from vertex 0 to vertex 1. -/
  62abbrev twoPointOneEdge (B : ℕ) (hB : 2 ≤ B) (hB1 : 1 ≤ B) : BoundedComplex B where
  63  nV := 2
  64  nE := 1
  65  nT := 0
  66  hV := hB
  67  hE := hB1
  68  hT := Nat.zero_le B
  69  edgeVerts := fun _ => (0, 1)
  70  tetVerts := fun t => t.elim0
  71
  72/-- The automorphism group of the directed edge is trivial. `edge_comm`
  73compares ordered endpoint pairs, so an automorphism must fix vertex 0 and
  74vertex 1 separately; the edge and tetrahedron index bijections are forced
  75because their index types have at most one element. -/
  76instance instSubsingletonAutOneEdge (B : ℕ) (hB : 2 ≤ B) (hB1 : 1 ≤ B) :
  77    Subsingleton (Aut (twoPointOneEdge B hB hB1)) := by
  78  constructor
  79  intro a b
  80  -- every automorphism fixes both vertices
  81  have key : ∀ c : Aut (twoPointOneEdge B hB hB1),
  82      c.vEquiv = Equiv.refl (Fin 2) := by
  83    intro c
  84    have h := c.edge_comm 0
  85    simp only [Prod.map] at h
  86    have h0 : c.vEquiv 0 = 0 := (Prod.mk.injEq _ _ _ _).mp h.symm |>.1
  87    have h1 : c.vEquiv 1 = 1 := (Prod.mk.injEq _ _ _ _).mp h.symm |>.2
  88    refine Equiv.ext fun x => ?_
  89    fin_cases x
  90    · simpa using h0
  91    · simpa using h1
  92  refine Relabel.ext (by rw [key a, key b]) ?_ ?_
  93  · exact Equiv.ext fun x => Subsingleton.elim _ _
  94  · exact Equiv.ext fun x => x.elim0
  95
  96/-- **THEOREM.** `|Aut(directed edge on two vertices)| = 1`. -/
  97theorem autCard_twoPointOneEdge (B : ℕ) (hB : 2 ≤ B) (hB1 : 1 ≤ B) :
  98    Nat.card (Aut (twoPointOneEdge B hB hB1)) = 1 :=
  99  Nat.card_unique
 100
 101/-- **THEOREM.** The symmetry-factor measure of the directed edge is 1. -/
 102theorem mu_twoPointOneEdge (B : ℕ) (hB : 2 ≤ B) (hB1 : 1 ≤ B) :
 103    mu (twoPointOneEdge B hB hB1) = 1 := by
 104  unfold mu
 105  rw [autCard_twoPointOneEdge]
 106  norm_num
 107
 108/-! ## §2. Ledger site symmetry, and its blindness at two sites -/
 109
 110/-- The site-symmetry count of a recognition ledger: how many relabelings of
 111the site type leave the cost function unchanged. This is the ledger-side
 112quantity a derivation would feed to orbit-stabilizer. Its definition mentions
 113no automorphism, no orbit count and no gauge volume. -/
 114noncomputable def siteSymCard {Λ : Type} [Fintype Λ] [DecidableEq Λ]
 115    (L : RecognitionLedger Λ) : ℕ :=
 116  Nat.card {σ : Equiv.Perm Λ // ∀ i j, L.cost (σ i) (σ j) = L.cost i j}
 117
 118/-- On two sites there is only one off-diagonal cost. Zero diagonal and
 119symmetry of cost together leave a recognition ledger on `Fin 2` with exactly
 120one degree of freedom, and this lemma is that fact in usable form. -/
 121theorem cost_offDiag_fin2 (L : RecognitionLedger (Fin 2)) :
 122    ∀ a b : Fin 2, a ≠ b → L.cost a b = L.cost 0 1 := by
 123  intro a b hab
 124  fin_cases a <;> fin_cases b <;> simp_all [L.symmetric]
 125
 126/-- **THEOREM (blindness at two sites).** EVERY permutation of a two-element
 127site type is a site symmetry of EVERY recognition ledger on it. A permutation
 128either fixes a pair of sites, where zero diagonal settles it, or exchanges
 129them, where symmetry of cost settles it. So no ledger on two sites can
 130distinguish its two sites. -/
 131theorem every_perm_is_siteSym (L : RecognitionLedger (Fin 2))
 132    (σ : Equiv.Perm (Fin 2)) (i j : Fin 2) :
 133    L.cost (σ i) (σ j) = L.cost i j := by
 134  by_cases hij : i = j
 135  · subst hij
 136    rw [L.diagonal_zero, L.diagonal_zero]
 137  · rw [cost_offDiag_fin2 L _ _ (fun h => hij (σ.injective h)),
 138      cost_offDiag_fin2 L _ _ hij]
 139
 140/-- **THEOREM.** The site-symmetry group at two sites is the whole permutation
 141group, so the site-symmetry count is 2 for every recognition ledger. -/
 142theorem siteSymCard_fin2 (L : RecognitionLedger (Fin 2)) : siteSymCard L = 2 := by
 143  have huniv : {σ : Equiv.Perm (Fin 2) //
 144      ∀ i j, L.cost (σ i) (σ j) = L.cost i j} ≃ Equiv.Perm (Fin 2) :=
 145    { toFun := fun s => s.val
 146      invFun := fun σ => ⟨σ, every_perm_is_siteSym L σ⟩
 147      left_inv := fun _ => Subtype.ext rfl
 148      right_inv := fun _ => rfl }
 149  rw [siteSymCard, Nat.card_congr huniv, Nat.card_eq_fintype_card,
 150    Fintype.card_perm, Fintype.card_fin]
 151  norm_num [Nat.factorial]
 152
 153/-! ## §3. The no-go -/
 154
 155/-- **HEADLINE (KILL + WITNESS).** No candidate measure that factors through
 156the ledger's site-symmetry count on the vertex site type satisfies gauge
 157counting.
 158
 159The premise `hfactor` says only that on two-vertex complexes the measure is
 160some function of the site-symmetry count of the encoded ledger. The encoding
 161`enc` and the readout `g` are arbitrary: this kills the whole shape at once,
 162not one construction. -/
 163theorem no_siteSymmetry_measure {B : ℕ} (hB : 2 ≤ B) (hB1 : 1 ≤ B)
 164    (enc : BoundedComplex B → RecognitionLedger (Fin 2)) (g : ℕ → ℝ)
 165    (ν : TriangulationClass B → ℝ)
 166    (hfactor : ∀ K : BoundedComplex B, K.nV = 2 →
 167      ν (Quotient.mk (relabelSetoid B) K) = g (siteSymCard (enc K))) :
 168    ¬ GaugeCountingPrinciple ν := by
 169  intro hgc
 170  have hmu := (gaugeCountingPrinciple_iff_mu_on_representatives ν).mp hgc
 171  -- the edgeless pair: gauge counting demands 1/2
 172  have e1 : g 2 = 1 / 2 := by
 173    have h := hfactor (twoPointComplex B hB) rfl
 174    rw [siteSymCard_fin2] at h
 175    rw [← h, hmu, mu_twoPointComplex B hB]
 176  -- the directed edge: gauge counting demands 1
 177  have e2 : g 2 = 1 := by
 178    have h := hfactor (twoPointOneEdge B hB hB1) rfl
 179    rw [siteSymCard_fin2] at h
 180    rw [← h, hmu, mu_twoPointOneEdge B hB hB1]
 181  rw [e1] at e2
 182  norm_num at e2
 183
 184/-- **The separation, stated without reference to any candidate measure.** The
 185two witnesses agree on every ledger site-symmetry count and disagree on the
 186symmetry-factor measure. This is what any derivation must import structure to
 187separate. -/
 188theorem witnesses_agree_on_ledger_disagree_on_measure {B : ℕ}
 189    (hB : 2 ≤ B) (hB1 : 1 ≤ B)
 190    (enc : BoundedComplex B → RecognitionLedger (Fin 2)) :
 191    siteSymCard (enc (twoPointComplex B hB))
 192        = siteSymCard (enc (twoPointOneEdge B hB hB1)) ∧
 193      mu (twoPointComplex B hB) ≠ mu (twoPointOneEdge B hB hB1) := by
 194  refine ⟨by rw [siteSymCard_fin2, siteSymCard_fin2], ?_⟩
 195  rw [mu_twoPointComplex B hB, mu_twoPointOneEdge B hB hB1]
 196  norm_num
 197
 198/-! ## §4. The other route, and why it is not a derivation either
 199
 200Section 3 kills measures that factor through the ledger's site-symmetry count,
 201which is the route by which an automorphism count naturally arises. The
 202remaining route is to read the measure off the ledger's cost VALUES. That route
 203is not blind, and it is not a derivation, for the opposite reason: the ledger
 204axioms place no constraint on which ledger a complex is encoded as, so the
 205encoding is a free parameter and whatever it is fed determines the answer.
 206
 207The two theorems below make that exact. First, every non-negative number is the
 208off-diagonal cost of some recognition ledger on two sites, so the axioms
 209constrain the value not at all. Second, one fixed readout gives the correct
 210measure under one encoding and a wrong measure under another, so what determined
 211the measure was the choice of encoding and not the substrate. -/
 212
 213/-- The uniform ledger on two sites with off-diagonal cost `t`. Every axiom
 214holds for every `t ≥ 0`: the gate `rclGate u v = 2uv + 2u + 2v` gives
 215`rclGate 0 t = 2t ≥ t`, so subadditivity is slack rather than binding. -/
 216noncomputable def uniformLedger {t : ℝ} (ht : 0 ≤ t) : RecognitionLedger (Fin 2) where
 217  cost := fun i j => if i = j then 0 else t
 218  symmetric := fun i j => by
 219    by_cases h : i = j
 220    · subst h; simp
 221    · simp [h, Ne.symm h]
 222  diagonal_zero := fun i => by simp
 223  nonneg := fun i j => by by_cases h : i = j <;> simp [h, ht]
 224  rcl_subadditive := fun i j k => by
 225    unfold rclGate
 226    fin_cases i <;> fin_cases j <;> fin_cases k <;> simp <;> nlinarith
 227
 228@[simp] theorem uniformLedger_offDiag {t : ℝ} (ht : 0 ≤ t) :
 229    (uniformLedger ht).cost 0 1 = t := by
 230  simp [uniformLedger]
 231
 232/-- **THEOREM (the encoding is unconstrained).** For any assignment of
 233non-negative numbers to bounded complexes there is an encoding into recognition
 234ledgers on two sites realizing it exactly. The ledger axioms therefore say
 235nothing about which ledger a complex should become. -/
 236theorem encoding_unconstrained {B : ℕ} (f : BoundedComplex B → ℝ)
 237    (hf : ∀ K, 0 ≤ f K) :
 238    ∃ enc : BoundedComplex B → RecognitionLedger (Fin 2),
 239      ∀ K, (enc K).cost 0 1 = f K :=
 240  ⟨fun K => uniformLedger (hf K), fun K => uniformLedger_offDiag (hf K)⟩
 241
 242/-- **HEADLINE (the value route is fitting, not deriving).** There is a single
 243readout, the identity on the off-diagonal cost, which returns exactly the
 244symmetry-factor measure under one encoding and returns the wrong answer under
 245another. So a construction of the form "encode the complex as a ledger, read the
 246measure off its cost" has its answer supplied by the encoding, not by the
 247substrate.
 248
 249Combined with §3 this is the named import the open obligation needs: any
 250derivation must bring a canonical encoding from complexes to recognition
 251ledgers, forced rather than chosen, and neither the ledger axioms nor the
 252carrier supplies one. -/
 253theorem value_route_is_encoding_choice {B : ℕ} (hB : 2 ≤ B) :
 254    ∃ enc enc' : BoundedComplex B → RecognitionLedger (Fin 2),
 255      (∀ K : BoundedComplex B, (enc K).cost 0 1 = mu K) ∧
 256      (∀ K : BoundedComplex B, (enc' K).cost 0 1 = 0) ∧
 257      mu (twoPointComplex B hB) ≠ 0 := by
 258  refine ⟨fun K => uniformLedger (mu_pos K).le, fun _ => flatLedger (Fin 2),
 259    fun K => uniformLedger_offDiag (mu_pos K).le, fun _ => rfl, ?_⟩
 260  rw [mu_twoPointComplex B hB]
 261  norm_num
 262
 263/-! ## §5. The general statement: on any site type the symmetry is chosen
 264
 265Sections 3 and 4 are about the vertex site type, where a two-vertex complex
 266encodes into a ledger on two sites. The obvious escape is a richer site type,
 267one site per simplex rather than per vertex, which can carry an orientation that
 268a symmetric cost on vertex sites cannot. This section shows the escape does not
 269change the verdict, and it upgrades the answer from "vertex sites" to "any site
 270type".
 271
 272The reason is that a recognition ledger's site-symmetry group is itself chosen by
 273the encoding. On three or more sites the axioms admit both a ledger whose site
 274symmetries are everything and a ledger for which a given transposition is not a
 275site symmetry. So the symmetry data a derivation would read is a function of the
 276encoding, and the ledger axioms never pick one. Whatever the site type, the
 277premise to import is the same: a canonical encoding, forced rather than chosen. -/
 278
 279/-- The uniform ledger on three sites: cost `t` off the diagonal, valid for
 280every `t ≥ 0`. -/
 281noncomputable def uniformLedger3 {t : ℝ} (ht : 0 ≤ t) : RecognitionLedger (Fin 3) where
 282  cost := fun i j => if i = j then 0 else t
 283  symmetric := fun i j => by
 284    by_cases h : i = j
 285    · subst h; simp
 286    · simp [h, Ne.symm h]
 287  diagonal_zero := fun i => by simp
 288  nonneg := fun i j => by by_cases h : i = j <;> simp [h, ht]
 289  rcl_subadditive := fun i j k => by
 290    unfold rclGate
 291    fin_cases i <;> fin_cases j <;> fin_cases k <;> simp <;> nlinarith
 292
 293/-- Every permutation is a site symmetry of the uniform ledger: its cost
 294depends only on whether two sites are equal, and a permutation preserves that. -/
 295theorem uniform3_siteSym {t : ℝ} (ht : 0 ≤ t) (σ : Equiv.Perm (Fin 3)) (i j : Fin 3) :
 296    (uniformLedger3 ht).cost (σ i) (σ j) = (uniformLedger3 ht).cost i j := by
 297  show (if σ i = σ j then (0:ℝ) else t) = if i = j then 0 else t
 298  by_cases h : i = j
 299  · subst h; simp
 300  · rw [if_neg h, if_neg (fun he : σ i = σ j => h (σ.injective he))]
 301
 302/-- Pair costs on three sites, pairwise different off the diagonal: `1`, `3/2`
 303and `2`. Matching on `Fin.mk` so the values reduce on literals. -/
 304noncomputable def dcost : Fin 3 → Fin 3 → ℝ
 305  | ⟨0, _⟩, ⟨1, _⟩ => 1
 306  | ⟨1, _⟩, ⟨0, _⟩ => 1
 307  | ⟨0, _⟩, ⟨2, _⟩ => 3 / 2
 308  | ⟨2, _⟩, ⟨0, _⟩ => 3 / 2
 309  | ⟨1, _⟩, ⟨2, _⟩ => 2
 310  | ⟨2, _⟩, ⟨1, _⟩ => 2
 311  | _, _ => 0
 312
 313/-- A ledger on three sites whose three pair costs are pairwise different. All
 314four axioms hold; RCL subadditivity is slack because the gate at two
 315off-diagonal arguments is at least `2 * 1 * 1 + 2 + 2 = 6`. -/
 316noncomputable def distinctLedger : RecognitionLedger (Fin 3) where
 317  cost := dcost
 318  symmetric := fun i j => by fin_cases i <;> fin_cases j <;> norm_num [dcost]
 319  diagonal_zero := fun i => by fin_cases i <;> norm_num [dcost]
 320  nonneg := fun i j => by fin_cases i <;> fin_cases j <;> norm_num [dcost]
 321  rcl_subadditive := fun i j k => by
 322    unfold rclGate
 323    fin_cases i <;> fin_cases j <;> fin_cases k <;> norm_num [dcost]
 324
 325/-- **THEOREM.** The transposition of sites 0 and 1 is NOT a site symmetry of
 326`distinctLedger`: it carries the pair cost `3/2` to the pair cost `2`. -/
 327theorem swap01_not_siteSym_distinct :
 328    ¬ (∀ i j : Fin 3, distinctLedger.cost (Equiv.swap 0 1 i) (Equiv.swap 0 1 j)
 329        = distinctLedger.cost i j) := by
 330  intro h
 331  have h02 := h 0 2
 332  rw [Equiv.swap_apply_left,
 333    Equiv.swap_apply_of_ne_of_ne (by decide) (by decide)] at h02
 334  norm_num [distinctLedger, dcost] at h02
 335
 336/-- **HEADLINE (general form).** On a site type with three or more sites the
 337recognition ledger axioms admit both a ledger for which every permutation is a
 338site symmetry and a ledger for which a given transposition is not. The
 339site-symmetry group a derivation would read off the substrate is therefore
 340determined by the encoding and not by the axioms, on every site type, however
 341rich.
 342
 343Together with §3 and §4 this is the answer to the open obligation's second
 344disjunct in its general form. The additional premise any encoding-based
 345derivation of the path-sum measure must import is a CANONICAL encoding from
 346bounded complexes to recognition ledgers, forced rather than chosen. Moving to
 347simplex-level sites buys the expressiveness that vertex sites provably lack, and
 348buys nothing at all against this. -/
 349theorem siteSymmetry_is_chosen_by_the_encoding :
 350    (∀ σ : Equiv.Perm (Fin 3), ∀ i j : Fin 3,
 351      (uniformLedger3 (le_refl (0:ℝ))).cost (σ i) (σ j)
 352        = (uniformLedger3 (le_refl (0:ℝ))).cost i j) ∧
 353    ¬ (∀ i j : Fin 3, distinctLedger.cost (Equiv.swap 0 1 i) (Equiv.swap 0 1 j)
 354        = distinctLedger.cost i j) :=
 355  ⟨fun σ => uniform3_siteSym (le_refl (0:ℝ)) σ, swap01_not_siteSym_distinct⟩
 356
 357#print axioms autCard_twoPointOneEdge
 358#print axioms siteSymCard_fin2
 359#print axioms no_siteSymmetry_measure
 360#print axioms witnesses_agree_on_ledger_disagree_on_measure
 361#print axioms encoding_unconstrained
 362#print axioms value_route_is_encoding_choice
 363#print axioms siteSymmetry_is_chosen_by_the_encoding
 364
 365end Gap2LedgerSiteBlindness
 366end SevenGaps
 367end Gravity
 368end IndisputableMonolith
 369