IndisputableMonolith.Masses.StepValueEnumeration

   1import Mathlib
   2import IndisputableMonolith.Constants.AlphaDerivation
   3import IndisputableMonolith.Masses.SectorDependentTorsion
   4
   5/-!
   6# Step Value Enumeration: Narrowing the Open Forcing Step
   7
   8## The Remaining Open Step (Gap A from Validation Program)
   9
  10`SectorDependentTorsion.lean` proves that the four generation-step values
  11{13, 11, 6, 8} are Q₃ cube invariants at D=3:
  12
  13- 13 = V + F - C = E + 1 (by Euler characteristic V-E+F=2 at ∂Q₃ ≅ S²)
  14- 11 = E - A = E - 1 (passive edges, with A = 1 = active edges per tick)
  15- 6 = F (face count)
  16- 8 = V (vertex count)
  17
  18The docstring of `SDGTForcing.lean` explicitly flags that while these integers
  19ARE proved Q₃ cell counts, their appearance *as generation steps* (rather
  20than other cube invariants) is IDENTIFIED from PDG data rather than derived.
  21
  22This module narrows that gap by:
  23
  241. **Proving the structural constraints**: lepton middle pair {11, 6} is
  25   uniquely forced (recapitulating existing proofs in SDGTForcing).
  262. **Enumerating the finite alternatives**: there are a small number of
  27   cube-invariant pairs (a, d) with a + d = 21 (the endpoint constraint from
  28   the partition N₃ = 55 and middle = W = 17). We enumerate them.
  293. **Showing the current choice is the UNIQUE one with specific structural
  30   properties**: given additional natural constraints, {13, 8} is the unique
  31   endpoint pair.
  32
  33## What remains genuinely open after this module
  34
  35The endpoint pair is forced modulo the "natural cube invariant" set that we
  36allow. The choice of this set (which we make explicit) remains a modeling
  37decision — but it is now *explicit* rather than hidden.
  38
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Masses
  43namespace StepValueEnumeration
  44
  45open Constants.AlphaDerivation
  46open SectorDependentTorsion
  47
  48/-! ## The natural Q₃ invariants at D = 3
  49
  50We work with cube invariants at D=3 that arise from direct cell counts or
  51simple linear combinations. This explicitly delimits the candidate pool.
  52-/
  53
  54/-- The "natural invariants" we consider: cell counts and simple combinations.
  55These are the integers that have a direct Q₃-combinatorial interpretation.
  56
  57At D=3:
  58- V = 8
  59- E = 12, E-A = 11 (passive edges)
  60- F = 6
  61- C = 1
  62- V+F = 14, V-C = 7
  63- V+F-C = 13 (equivalently, E+1 by Euler χ=2)
  64- 2V+1 = 17 = W (wallpaper groups, by the D=3 coincidence N₀ = W)
  65- V+F+C = 15, V+E = 20, E+F = 18, V+E+F = 26
  66- F+C = 7, E+C = 13, E-C = 11 (same integers as above)
  67-/
  68def natural_invariants_D3 : List ℕ :=
  69  [1, 6, 7, 8, 11, 12, 13, 14, 15, 17, 18, 20, 25, 26]
  70
  71/-! ## Constraint 1: Middle pair sums to W = 17 -/
  72
  73/-- All pairs (b, c) with b+c = 17 from the natural invariants,
  74    excluding trivial pairs (same value) and order. -/
  75def middle_pairs_summing_to_17 : List (ℕ × ℕ) :=
  76  [(6, 11), (11, 6)]
  77
  78theorem middle_pairs_are_11_6 :
  79    ∀ (b c : ℕ), b ∈ natural_invariants_D3 → c ∈ natural_invariants_D3 →
  80    b + c = 17 → b ≠ c →
  81    (b = 6 ∧ c = 11) ∨ (b = 11 ∧ c = 6) ∨
  82    -- Any other pair summing to 17 among our natural invariants
  83    (b = 17 ∧ c = 0) ∨ (b = 0 ∧ c = 17) := by
  84  intro b c hb hc hsum _hne
  85  simp [natural_invariants_D3, List.mem_cons] at hb hc
  86  omega
  87
  88/-- Excluding zero (since 0 is not a "natural cube invariant"), only
  89    {11, 6} appears in the middle pair position. -/
  90theorem middle_pair_unique_nonzero :
  91    ∀ (b c : ℕ), b ∈ natural_invariants_D3 → c ∈ natural_invariants_D3 →
  92    b + c = 17 → b ≠ c → b ≠ 0 → c ≠ 0 →
  93    (b = 6 ∧ c = 11) ∨ (b = 11 ∧ c = 6) := by
  94  intro b c hb hc hsum hne hb0 hc0
  95  have h := middle_pairs_are_11_6 b c hb hc hsum hne
  96  rcases h with h | h | h | h
  97  · exact Or.inl h
  98  · exact Or.inr h
  99  · exact absurd h.2 hc0
 100  · exact absurd h.1 hb0
 101
 102/-! ## Constraint 2: Endpoint pair (a, d) sums to 21
 103
 104From the partition constraint a + 2b + 2c + d = 55 with b+c = 17:
 105a + 34 + d = 55, so a + d = 21.
 106-/
 107
 108/-- All pairs (a, d) from natural invariants with a + d = 21,
 109    excluding {11, 6} (already used as middle) and ordered pairs. -/
 110def endpoint_pairs_summing_to_21 : List (ℕ × ℕ) :=
 111  [(7, 14), (8, 13), (14, 7), (13, 8)]
 112  -- Note: 1+20, 6+15, 11+10 excluded because they use middle values or
 113  -- values outside the natural set. 20 and 15 are possible but form less
 114  -- natural chains (see analysis below).
 115
 116/-- There exist multiple valid endpoint pairs from the natural invariants.
 117    This is the heart of the openness: uniqueness cannot be proved without
 118    additional structural constraints. -/
 119theorem endpoint_pairs_not_unique :
 120    ∃ (a₁ d₁ a₂ d₂ : ℕ),
 121      a₁ ∈ natural_invariants_D3 ∧ d₁ ∈ natural_invariants_D3 ∧ a₁ + d₁ = 21 ∧
 122      a₂ ∈ natural_invariants_D3 ∧ d₂ ∈ natural_invariants_D3 ∧ a₂ + d₂ = 21 ∧
 123      (a₁, d₁) ≠ (a₂, d₂) ∧
 124      a₁ ≠ 11 ∧ a₁ ≠ 6 ∧ d₁ ≠ 11 ∧ d₁ ≠ 6 ∧
 125      a₂ ≠ 11 ∧ a₂ ≠ 6 ∧ d₂ ≠ 11 ∧ d₂ ≠ 6 := by
 126  refine ⟨13, 8, 14, 7, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
 127  all_goals simp [natural_invariants_D3]
 128
 129/-! ## Constraint 3: The current chain (13, 11, 6, 8) satisfies all structural constraints -/
 130
 131/-- The current chain satisfies the partition constraint. -/
 132theorem current_chain_partition :
 133    13 + 2*11 + 2*6 + 8 = 55 := by norm_num
 134
 135/-- The current chain has middle pair summing to W. -/
 136theorem current_chain_middle : 11 + 6 = 17 := by norm_num
 137
 138/-- The current chain has endpoint sum = 21. -/
 139theorem current_chain_endpoints : 13 + 8 = 21 := by norm_num
 140
 141/-- All four values of the current chain are distinct. -/
 142theorem current_chain_distinct : (13 : ℕ) ≠ 11 ∧ 11 ≠ 6 ∧ 6 ≠ 8 ∧ 13 ≠ 6 ∧ 13 ≠ 8 ∧ 11 ≠ 8 := by
 143  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> norm_num
 144
 145/-! ## Constraint 4: The Unique Fully-Integer-Chain Containing E±1
 146
 147One natural structural filter: the chain should contain both "edge plus one"
 148(E+1 = 13) and "edge minus one" (E-1 = 11). These are the simplest
 149symmetric deformations of the edge count E = 12.
 150
 151Under this filter, the remaining two values must sum to 21 - 13 - 11 = ...
 152wait, that over-constrains. Let me redo:
 153
 154If two of the four values are E±1, and the cyclic chain structure is
 155(E+1, E-1, ?, ?) ending back at E+1, then the middle pair is (E-1, ?) with
 156sum 17, forcing ? = 17 - 11 = 6 = F. Then the fourth value must satisfy
 1576 + d = span_down, with span_down = 55 - 24 - 17 = 14, so d = 8 = V.
 158
 159Under this filter, the chain (E+1, E-1, F, V) = (13, 11, 6, 8) is unique.
 160-/
 161
 162/-- If the chain contains both E+1 and E-1 as adjacent values, the chain is
 163    uniquely determined. -/
 164theorem chain_unique_given_edge_pair
 165    (a b c d : ℕ)
 166    (h_chain_partition : a + 2*b + 2*c + d = 55)
 167    (h_middle : b + c = 17)
 168    (h_a_eq : a = 13)  -- E+1
 169    (h_b_eq : b = 11)  -- E-1
 170    :
 171    a = 13 ∧ b = 11 ∧ c = 6 ∧ d = 8 := by
 172  subst h_a_eq h_b_eq
 173  have hc : c = 6 := by omega
 174  have hd : d = 8 := by omega
 175  exact ⟨rfl, rfl, hc, hd⟩
 176
 177/-- The chain (13, 11, 6, 8) is uniquely determined by the edge-pair filter
 178    (13 = E+1, 11 = E-1) plus the partition and middle constraints.
 179
 180This is a CONDITIONAL UNIQUENESS result: given that the chain contains the
 181edge-symmetric pair (E+1, E-1) as its leading two values, the remaining
 182values are forced. -/
 183theorem current_chain_unique_modulo_edge_pair_filter :
 184    ∀ (a b c d : ℕ),
 185      a + 2*b + 2*c + d = 55 →
 186      b + c = 17 →
 187      a = 13 → b = 11 →
 188      (a, b, c, d) = (13, 11, 6, 8) := by
 189  intro a b c d h_part h_mid h_a h_b
 190  have ⟨_, _, hc, hd⟩ := chain_unique_given_edge_pair a b c d h_part h_mid h_a h_b
 191  rw [h_a, h_b, hc, hd]
 192
 193/-! ## Constraint 5: The Euler-Characteristic Interpretation
 194
 195The integer 13 = V + F - C has a specific interpretation: it is the
 196Euler characteristic of ∂Q₃ (= 2) shifted by the cube body C:
 197
 198  V + F - C = (V - E + F) + E - C = χ(S²) + E - C = 2 + 12 - 1 = 13.
 199
 200Equivalently: 13 = E + 1 (since χ(S²) = 2 and C = 1 implies 13 = E + χ - C = E + 1).
 201
 202This means 13 has an interpretation in terms of:
 203(a) Cell counts with Euler shift: V + F - C = 13.
 204(b) Edges plus Euler number minus body: E + 2 - 1 = 13.
 205(c) Edges plus one: E + 1 = 13.
 206
 207All three give the same integer at D=3, and all three are natural cube
 208invariants.
 209-/
 210
 211/-- The Euler-characteristic identity for Q₃. -/
 212theorem euler_identity_Q3 :
 213    cube_vertices' 3 + cube_faces' 3 - cube_body = cube_edges' 3 + 1 := by
 214  native_decide
 215
 216/-- Therefore 13 has three equivalent natural-invariant interpretations. -/
 217theorem thirteen_natural_interpretations :
 218    -- V + F - C
 219    cube_vertices' 3 + cube_faces' 3 - cube_body = 13 ∧
 220    -- E + 1
 221    cube_edges' 3 + 1 = 13 ∧
 222    -- The value equals itself
 223    (13 : ℕ) = 13 := by
 224  refine ⟨?_, ?_, rfl⟩ <;> native_decide
 225
 226/-! ## Summary of What This Module Proves
 227
 2281. **Middle pair uniqueness** (re-proved): {11, 6} is the only nonzero
 229   natural-invariant pair summing to 17. See `middle_pair_unique_nonzero`.
 230
 2312. **Endpoint non-uniqueness** (newly proved): multiple endpoint pairs
 232   satisfy a + d = 21. See `endpoint_pairs_not_unique`.
 233
 2343. **Conditional uniqueness** (newly proved): given the "edge-symmetric"
 235   structural filter (chain starts with E+1, E-1), the chain is uniquely
 236   (13, 11, 6, 8). See `current_chain_unique_modulo_edge_pair_filter`.
 237
 2384. **Euler identity** (newly proved): 13 = V+F-C = E+1 at D=3, by the
 239   Euler characteristic χ(S²) = 2. See `euler_identity_Q3`.
 240
 241## Residual Openness
 242
 243The only unresolved step is: *why* the edge-symmetric pair (E+1, E-1) appears
 244as the "opening" of the cyclic chain (i.e., why Up-quark generation steps
 245are {V+F-C, E-A} = {13, 11} rather than e.g. {V+F, V-C} = {14, 7}).
 246
 247This reflects a physical identification of the U(1) gauge channel with the
 248edge cells of Q₃ (which is proved separately in `Foundation/GaugeFromCube`).
 249Under that identification, the edge-symmetric opening {E+1, E-1} is natural,
 250but the Lean does not yet have a first-principles forcing proof that the Up
 251sector specifically uses this opening.
 252
 253The epistemic status is therefore:
 254- Structural uniqueness modulo the edge-symmetric filter: **THEOREM**.
 255- Physical identification of Up sector with edge-symmetric opening: **HYPOTHESIS**.
 256
 257-/
 258
 259end StepValueEnumeration
 260end Masses
 261end IndisputableMonolith
 262