IndisputableMonolith.Verification.YardstickAssignmentChoiceSet
IndisputableMonolith/Verification/YardstickAssignmentChoiceSet.lean · 1007 lines · 80 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Masses.Anchor
3import IndisputableMonolith.Verification.YardstickAssignmentPrinciple
4
5/-!
6# Yardstick Assignment Choice-Set Enumeration (O1 Progress)
7
8This module makes the O1 discussion explicit as a finite combinatorial search:
9
10- Start from the four candidate `B_pow` values and the four candidate `r0` values.
11- Enumerate all sector-to-value assignments (all permutations).
12- Filter by structural constraints used in the Yardstick discussion.
13
14The resulting valid choice sets collapse to singletons for both `B_pow` and `r0`
15under these constraints.
16-/
17
18namespace IndisputableMonolith
19namespace Verification
20namespace YardstickAssignmentChoiceSet
21
22open Masses.Anchor
23
24/-! ## `B_pow` assignment search -/
25
26structure BPowAssignment where
27 lepton : ℤ
28 up : ℤ
29 down : ℤ
30 ew : ℤ
31 deriving Repr, DecidableEq
32
33def canonicalBPow : BPowAssignment :=
34 { lepton := -(2 * (E_passive : ℤ))
35 , up := -(A : ℤ)
36 , down := 2 * (E_total : ℤ) - 1
37 , ew := (A : ℤ) }
38
39/-- Orientation-reflected counterpart of `canonicalBPow` (same magnitudes, flipped active-edge sign). -/
40def mirroredBPow : BPowAssignment :=
41 { lepton := -(2 * (E_passive : ℤ))
42 , up := (A : ℤ)
43 , down := 2 * (E_total : ℤ) - 1
44 , ew := -(A : ℤ) }
45
46def bPowValuePool : List ℤ :=
47 [ -(2 * (E_passive : ℤ))
48 , -(A : ℤ)
49 , 2 * (E_total : ℤ) - 1
50 , (A : ℤ) ]
51
52theorem bpow_pool_matches_anchor_formulas :
53 bPowValuePool =
54 [B_pow .Lepton, B_pow .UpQuark, B_pow .DownQuark, B_pow .Electroweak] := by
55 rfl
56
57def listToBPowAssignment? : List ℤ → Option BPowAssignment
58 | [l, u, d, e] => some { lepton := l, up := u, down := d, ew := e }
59 | _ => none
60
61def allBPowAssignments : List BPowAssignment :=
62 (bPowValuePool.permutations.filterMap listToBPowAssignment?)
63
64/-- Structural B_pow sum target (`A = 1`). -/
65def bpowSumTarget : ℤ := (A : ℤ)
66
67theorem bpow_sum_target_eq_one : bpowSumTarget = 1 := by
68 native_decide
69
70theorem bpow_sum_target_matches_principle :
71 bpowSumTarget =
72 (B_pow .Lepton + B_pow .UpQuark + B_pow .DownQuark + B_pow .Electroweak) := by
73 calc
74 bpowSumTarget = 1 := bpow_sum_target_eq_one
75 _ = (B_pow .Lepton + B_pow .UpQuark + B_pow .DownQuark + B_pow .Electroweak) := by
76 symm
77 exact YardstickAssignmentPrinciple.B_pow_sum
78
79/-- Structural constraints used to filter `B_pow` assignments. -/
80def bpowStructuralConstraints (a : BPowAssignment) : Bool :=
81 decide (a.up = -a.ew) &&
82 decide ((Int.natAbs a.lepton : ℤ) + (Int.natAbs a.ew : ℤ) = a.down) &&
83 decide (a.up < 0) &&
84 decide (0 < a.ew) &&
85 decide (a.lepton + a.up + a.down + a.ew = bpowSumTarget)
86
87/-- Prop-level version of `bpowStructuralConstraints`. -/
88def bpowPrincipleConstraints (a : BPowAssignment) : Prop :=
89 a.up = -a.ew ∧
90 ((Int.natAbs a.lepton : ℤ) + (Int.natAbs a.ew : ℤ) = a.down) ∧
91 a.up < 0 ∧
92 0 < a.ew ∧
93 (a.lepton + a.up + a.down + a.ew = bpowSumTarget)
94
95def validBPowAssignments : List BPowAssignment :=
96 allBPowAssignments.filter bpowStructuralConstraints
97
98theorem all_bpow_assignments_count : allBPowAssignments.length = 24 := by
99 native_decide
100
101theorem valid_bpow_assignment_count : validBPowAssignments.length = 1 := by
102 native_decide
103
104theorem valid_bpow_assignments_are_singleton :
105 validBPowAssignments = [canonicalBPow] := by
106 native_decide
107
108theorem bpow_constraints_true_iff (a : BPowAssignment) :
109 bpowStructuralConstraints a = true ↔ bpowPrincipleConstraints a := by
110 unfold bpowStructuralConstraints bpowPrincipleConstraints
111 simp
112 tauto
113
114theorem bpow_constraints_force_canonical (a : BPowAssignment)
115 (ha : a ∈ allBPowAssignments)
116 (hP : bpowPrincipleConstraints a) :
117 a = canonicalBPow := by
118 have htrue : bpowStructuralConstraints a = true := (bpow_constraints_true_iff a).2 hP
119 have hmem : a ∈ validBPowAssignments := by
120 unfold validBPowAssignments
121 exact List.mem_filter.mpr ⟨ha, htrue⟩
122 rw [valid_bpow_assignments_are_singleton] at hmem
123 simpa using hmem
124
125/-- Normal form implied by `B_pow` principle constraints:
126 active-edge pair is fixed (`ew = 1`, `up = -1`), the down value is `1 - lepton`,
127 and lepton is necessarily nonpositive. -/
128theorem bpow_principle_normal_form (a : BPowAssignment)
129 (hP : bpowPrincipleConstraints a) :
130 a.ew = 1 ∧ a.up = -1 ∧ a.down = 1 - a.lepton ∧ a.lepton ≤ 0 := by
131 rcases hP with ⟨hSign, hComp, _hUpNeg, hEwPos, hSum⟩
132 have hsum' : a.lepton + a.down = bpowSumTarget := by
133 nlinarith [hSum, hSign]
134 have hsum1 : a.lepton + a.down = 1 := by
135 simpa [bpow_sum_target_eq_one] using hsum'
136 have hCompAbs : |a.lepton| + |a.ew| = a.down := by
137 simpa [Int.natCast_natAbs] using hComp
138 have hAbsEw : |a.ew| = a.ew := by
139 simpa using (abs_of_nonneg (le_of_lt hEwPos))
140 have hCore : a.lepton + |a.lepton| + a.ew = 1 := by
141 nlinarith [hsum1, hCompAbs, hAbsEw]
142 have hEwGe1 : (1 : ℤ) ≤ a.ew := by
143 simpa using (Int.add_one_le_iff.mpr hEwPos)
144 have hLe0sum : a.lepton + |a.lepton| ≤ 0 := by
145 nlinarith [hCore, hEwGe1]
146 have hTwoLeptonLe : 2 * a.lepton ≤ a.lepton + |a.lepton| := by
147 nlinarith [le_abs_self a.lepton]
148 have hLnonpos : a.lepton ≤ 0 := by
149 have h2l_le0 : 2 * a.lepton ≤ 0 := le_trans hTwoLeptonLe hLe0sum
150 nlinarith [h2l_le0]
151 have hAbsLnonpos : |a.lepton| = -a.lepton := by
152 simpa using (abs_of_nonpos hLnonpos)
153 have hEw1 : a.ew = 1 := by
154 nlinarith [hCore, hAbsLnonpos]
155 have hUpNegOne : a.up = -1 := by
156 nlinarith [hSign, hEw1]
157 have hDownForm : a.down = 1 - a.lepton := by
158 nlinarith [hsum1]
159 exact ⟨hEw1, hUpNegOne, hDownForm, hLnonpos⟩
160
161/-- Unrestricted forcing (no finite-pool membership): once the lepton sector is fixed
162 to passive-edge coupling `-2E_p`, the principle constraints force the full
163 canonical `B_pow` assignment. -/
164theorem bpow_unrestricted_forcing_from_passive_coupling (a : BPowAssignment)
165 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
166 (hP : bpowPrincipleConstraints a) :
167 a = canonicalBPow := by
168 rcases hP with ⟨hSign, hComp, hUpNeg, hEwPos, hSum⟩
169 have hsum' : a.lepton + a.down = bpowSumTarget := by
170 nlinarith [hSum, hSign]
171 have hsum1 : a.lepton + a.down = 1 := by
172 simpa [bpow_sum_target_eq_one] using hsum'
173 have hl22 : a.lepton = -22 := by
174 calc
175 a.lepton = -(2 * (E_passive : ℤ)) := hLepton
176 _ = -22 := by native_decide
177 have hd23 : a.down = 23 := by
178 nlinarith [hsum1, hl22]
179 have hLAbs : (Int.natAbs a.lepton : ℤ) = 22 := by
180 rw [hl22]
181 native_decide
182 have hEAbs : (Int.natAbs a.ew : ℤ) = 1 := by
183 nlinarith [hComp, hLAbs, hd23]
184 have hEAbsNat : Int.natAbs a.ew = Int.natAbs (1 : ℤ) := by
185 exact_mod_cast hEAbs
186 have hEw1 : a.ew = 1 := by
187 exact (Int.natAbs_inj_of_nonneg_of_nonneg (le_of_lt hEwPos) (by norm_num)).1 hEAbsNat
188 have hUpNegOne : a.up = -1 := by
189 nlinarith [hSign, hEw1]
190 rcases a with ⟨l, u, d, e⟩
191 simp at hl22 hUpNegOne hd23 hEw1
192 subst l
193 subst u
194 subst d
195 subst e
196 rfl
197
198/-- Unrestricted forcing with weaker role input: fixing the down-sector amplification
199 `2E_total - 1` plus principle constraints already forces the canonical `B_pow`. -/
200theorem bpow_unrestricted_forcing_from_down_role (a : BPowAssignment)
201 (hDown : a.down = 2 * (E_total : ℤ) - 1)
202 (hP : bpowPrincipleConstraints a) :
203 a = canonicalBPow := by
204 rcases hP with ⟨hSign, hComp, hUpNeg, hEwPos, hSum⟩
205 have hsum' : a.lepton + a.down = bpowSumTarget := by
206 nlinarith [hSum, hSign]
207 have hd23 : a.down = 23 := by
208 calc
209 a.down = 2 * (E_total : ℤ) - 1 := hDown
210 _ = 23 := by native_decide
211 have hl22 : a.lepton = -22 := by
212 have hsum1 : a.lepton + a.down = 1 := by simpa [bpow_sum_target_eq_one] using hsum'
213 nlinarith [hsum1, hd23]
214 have hLepton : a.lepton = -(2 * (E_passive : ℤ)) := by
215 calc
216 a.lepton = -22 := hl22
217 _ = -(2 * (E_passive : ℤ)) := by native_decide
218 exact bpow_unrestricted_forcing_from_passive_coupling a hLepton
219 ⟨hSign, hComp, hUpNeg, hEwPos, hSum⟩
220
221/-- From down-role fixation plus sign-duality and structural sum,
222 the lepton role is forced to passive-edge coupling. -/
223theorem bpow_lepton_forced_from_down_role_and_sign_sum (a : BPowAssignment)
224 (hDown : a.down = 2 * (E_total : ℤ) - 1)
225 (hSign : a.up = -a.ew)
226 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
227 a.lepton = -(2 * (E_passive : ℤ)) := by
228 have hsum' : a.lepton + a.down = bpowSumTarget := by
229 nlinarith [hSum, hSign]
230 have hsum1 : a.lepton + a.down = 1 := by
231 simpa [bpow_sum_target_eq_one] using hsum'
232 have hd23 : a.down = 23 := by
233 calc
234 a.down = 2 * (E_total : ℤ) - 1 := hDown
235 _ = 23 := by native_decide
236 have hl22 : a.lepton = -22 := by
237 nlinarith [hsum1, hd23]
238 calc
239 a.lepton = -22 := hl22
240 _ = -(2 * (E_passive : ℤ)) := by native_decide
241
242/-- Under sign-duality + structural sum, the passive-edge lepton role and down-role
243 amplification are equivalent assumptions. -/
244theorem bpow_lepton_role_iff_down_role_under_sign_sum (a : BPowAssignment)
245 (hSign : a.up = -a.ew)
246 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
247 (a.lepton = -(2 * (E_passive : ℤ))) ↔ (a.down = 2 * (E_total : ℤ) - 1) := by
248 have hsum' : a.lepton + a.down = bpowSumTarget := by
249 nlinarith [hSum, hSign]
250 have hsum1 : a.lepton + a.down = 1 := by
251 simpa [bpow_sum_target_eq_one] using hsum'
252 constructor
253 · intro hLepton
254 have hLepton22 : a.lepton = -22 := by
255 calc
256 a.lepton = -(2 * (E_passive : ℤ)) := hLepton
257 _ = -22 := by native_decide
258 have hDown23 : a.down = 23 := by
259 nlinarith [hsum1, hLepton22]
260 calc
261 a.down = 23 := hDown23
262 _ = 2 * (E_total : ℤ) - 1 := by native_decide
263 · intro hDown
264 have hDown23 : a.down = 23 := by
265 calc
266 a.down = 2 * (E_total : ℤ) - 1 := hDown
267 _ = 23 := by native_decide
268 have hLepton22 : a.lepton = -22 := by
269 nlinarith [hsum1, hDown23]
270 calc
271 a.lepton = -22 := hLepton22
272 _ = -(2 * (E_passive : ℤ)) := by native_decide
273
274/-- With passive-edge lepton role and down-role fixed, structural sum forces active-edge sign duality. -/
275theorem bpow_sign_forced_from_lepton_down_sum (a : BPowAssignment)
276 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
277 (hDown : a.down = 2 * (E_total : ℤ) - 1)
278 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
279 a.up = -a.ew := by
280 have hsum1 : a.lepton + a.up + a.down + a.ew = 1 := by
281 simpa [bpow_sum_target_eq_one] using hSum
282 have hLepton22 : a.lepton = -22 := by
283 calc
284 a.lepton = -(2 * (E_passive : ℤ)) := hLepton
285 _ = -22 := by native_decide
286 have hDown23 : a.down = 23 := by
287 calc
288 a.down = 2 * (E_total : ℤ) - 1 := hDown
289 _ = 23 := by native_decide
290 have hup_plus_ew_zero : a.up + a.ew = 0 := by
291 nlinarith [hsum1, hLepton22, hDown23]
292 nlinarith [hup_plus_ew_zero]
293
294/-- Under edge-role assumptions (down role, sign duality, active-edge unit magnitude
295 with positive EW orientation, and structural sum), the full `B_pow` principle
296 constraints are derived. -/
297theorem bpow_principle_constraints_forced_from_edge_roles (a : BPowAssignment)
298 (hDown : a.down = 2 * (E_total : ℤ) - 1)
299 (hSign : a.up = -a.ew)
300 (hEwPos : 0 < a.ew)
301 (hEwMag : Int.natAbs a.ew = A)
302 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
303 bpowPrincipleConstraints a := by
304 have hLepton : a.lepton = -(2 * (E_passive : ℤ)) :=
305 bpow_lepton_forced_from_down_role_and_sign_sum a hDown hSign hSum
306 have hDown23 : a.down = 23 := by
307 calc
308 a.down = 2 * (E_total : ℤ) - 1 := hDown
309 _ = 23 := by native_decide
310 have hLepton22 : a.lepton = -22 := by
311 calc
312 a.lepton = -(2 * (E_passive : ℤ)) := hLepton
313 _ = -22 := by native_decide
314 have hEwAbsNat : Int.natAbs a.ew = Int.natAbs (1 : ℤ) := by
315 have hA1 : A = 1 := by native_decide
316 rw [hA1] at hEwMag
317 simpa using hEwMag
318 have hEw1 : a.ew = 1 := by
319 exact (Int.natAbs_inj_of_nonneg_of_nonneg (le_of_lt hEwPos) (by norm_num)).1 hEwAbsNat
320 have hUpNegOne : a.up = -1 := by
321 nlinarith [hSign, hEw1]
322 have hUpNeg : a.up < 0 := by
323 nlinarith [hUpNegOne]
324 have hComp : (Int.natAbs a.lepton : ℤ) + (Int.natAbs a.ew : ℤ) = a.down := by
325 simp [hLepton22, hEw1, hDown23]
326 exact ⟨hSign, hComp, hUpNeg, hEwPos, hSum⟩
327
328/-- Same derivation using passive-edge lepton role instead of explicit down-role input. -/
329theorem bpow_principle_constraints_forced_from_passive_active_roles (a : BPowAssignment)
330 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
331 (hSign : a.up = -a.ew)
332 (hEwPos : 0 < a.ew)
333 (hEwMag : Int.natAbs a.ew = A)
334 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
335 bpowPrincipleConstraints a := by
336 have hDown : a.down = 2 * (E_total : ℤ) - 1 :=
337 (bpow_lepton_role_iff_down_role_under_sign_sum a hSign hSum).1 hLepton
338 exact bpow_principle_constraints_forced_from_edge_roles a hDown hSign hEwPos hEwMag hSum
339
340/-- Boolean-filter version of the previous derivation theorem. -/
341theorem bpow_bool_constraints_forced_from_edge_roles (a : BPowAssignment)
342 (hDown : a.down = 2 * (E_total : ℤ) - 1)
343 (hSign : a.up = -a.ew)
344 (hEwPos : 0 < a.ew)
345 (hEwMag : Int.natAbs a.ew = A)
346 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
347 bpowStructuralConstraints a = true := by
348 exact (bpow_constraints_true_iff a).2 <|
349 bpow_principle_constraints_forced_from_edge_roles a hDown hSign hEwPos hEwMag hSum
350
351/-- Boolean-filter version using passive-edge lepton role input. -/
352theorem bpow_bool_constraints_forced_from_passive_active_roles (a : BPowAssignment)
353 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
354 (hSign : a.up = -a.ew)
355 (hEwPos : 0 < a.ew)
356 (hEwMag : Int.natAbs a.ew = A)
357 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
358 bpowStructuralConstraints a = true := by
359 exact (bpow_constraints_true_iff a).2 <|
360 bpow_principle_constraints_forced_from_passive_active_roles a hLepton hSign hEwPos hEwMag hSum
361
362/-- Unrestricted canonical forcing from edge-role assumptions (no finite enumeration). -/
363theorem bpow_unrestricted_forcing_from_edge_roles (a : BPowAssignment)
364 (hDown : a.down = 2 * (E_total : ℤ) - 1)
365 (hSign : a.up = -a.ew)
366 (hEwPos : 0 < a.ew)
367 (hEwMag : Int.natAbs a.ew = A)
368 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
369 a = canonicalBPow := by
370 have hP := bpow_principle_constraints_forced_from_edge_roles a hDown hSign hEwPos hEwMag hSum
371 exact bpow_unrestricted_forcing_from_down_role a hDown hP
372
373/-- Unrestricted canonical forcing via passive-edge + active-edge role inputs. -/
374theorem bpow_unrestricted_forcing_from_passive_active_roles (a : BPowAssignment)
375 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
376 (hSign : a.up = -a.ew)
377 (hEwPos : 0 < a.ew)
378 (hEwMag : Int.natAbs a.ew = A)
379 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
380 a = canonicalBPow := by
381 have hDown : a.down = 2 * (E_total : ℤ) - 1 :=
382 (bpow_lepton_role_iff_down_role_under_sign_sum a hSign hSum).1 hLepton
383 exact bpow_unrestricted_forcing_from_edge_roles a hDown hSign hEwPos hEwMag hSum
384
385/-- Unrestricted canonical forcing via passive/down roles without an explicit sign assumption. -/
386theorem bpow_unrestricted_forcing_from_passive_down_roles (a : BPowAssignment)
387 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
388 (hDown : a.down = 2 * (E_total : ℤ) - 1)
389 (hEwPos : 0 < a.ew)
390 (hEwMag : Int.natAbs a.ew = A)
391 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
392 a = canonicalBPow := by
393 have hSign : a.up = -a.ew :=
394 bpow_sign_forced_from_lepton_down_sum a hLepton hDown hSum
395 exact bpow_unrestricted_forcing_from_edge_roles a hDown hSign hEwPos hEwMag hSum
396
397/-- Without an orientation choice, down-role + sign-duality + structural sum + active-unit
398 magnitude leaves exactly two `B_pow` branches: canonical and its mirrored orientation. -/
399theorem bpow_two_branch_under_down_role (a : BPowAssignment)
400 (hDown : a.down = 2 * (E_total : ℤ) - 1)
401 (hSign : a.up = -a.ew)
402 (hEwMag : Int.natAbs a.ew = A)
403 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget) :
404 a = canonicalBPow ∨ a = mirroredBPow := by
405 have hLepton : a.lepton = -(2 * (E_passive : ℤ)) :=
406 bpow_lepton_forced_from_down_role_and_sign_sum a hDown hSign hSum
407 have hDownForm : a.down = 2 * (E_total : ℤ) - 1 := hDown
408 have hA1 : A = 1 := by native_decide
409 have hEwAbsNat : Int.natAbs a.ew = Int.natAbs (1 : ℤ) := by
410 rw [hA1] at hEwMag
411 simpa using hEwMag
412 rcases Int.natAbs_eq_natAbs_iff.mp hEwAbsNat with hEwOne | hEwNegOne
413 · have hUp : a.up = -(A : ℤ) := by
414 have hEwA : a.ew = (A : ℤ) := by simpa [hA1] using hEwOne
415 nlinarith [hSign, hEwA]
416 rcases a with ⟨l, u, d, e⟩
417 simp at hLepton hUp hDownForm hEwOne
418 subst l
419 subst u
420 subst d
421 subst e
422 left
423 rfl
424 · have hUp : a.up = (A : ℤ) := by
425 have hEwNegA : a.ew = -(A : ℤ) := by simpa [hA1] using hEwNegOne
426 nlinarith [hSign, hEwNegA]
427 rcases a with ⟨l, u, d, e⟩
428 simp at hLepton hUp hDownForm hEwNegOne
429 subst l
430 subst u
431 subst d
432 subst e
433 right
434 rfl
435
436/-- Positive EW orientation selects the canonical branch from `bpow_two_branch_under_down_role`. -/
437theorem bpow_orientation_selects_canonical_from_two_branch (a : BPowAssignment)
438 (hDown : a.down = 2 * (E_total : ℤ) - 1)
439 (hSign : a.up = -a.ew)
440 (hEwMag : Int.natAbs a.ew = A)
441 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
442 (hEwPos : 0 < a.ew) :
443 a = canonicalBPow := by
444 rcases bpow_two_branch_under_down_role a hDown hSign hEwMag hSum with hcan | hmirror
445 · exact hcan
446 · exfalso
447 have hmirror_not_pos : ¬ (0 < mirroredBPow.ew) := by
448 native_decide
449 exact hmirror_not_pos (by simpa [hmirror] using hEwPos)
450
451/-- Passive/down roles + structural sum already determine sign-duality, so branch selection
452 can be stated without an explicit sign assumption. -/
453theorem bpow_orientation_selects_canonical_from_passive_down_roles (a : BPowAssignment)
454 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
455 (hDown : a.down = 2 * (E_total : ℤ) - 1)
456 (hEwMag : Int.natAbs a.ew = A)
457 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
458 (hEwPos : 0 < a.ew) :
459 a = canonicalBPow := by
460 have hSign : a.up = -a.ew :=
461 bpow_sign_forced_from_lepton_down_sum a hLepton hDown hSum
462 exact bpow_orientation_selects_canonical_from_two_branch a hDown hSign hEwMag hSum hEwPos
463
464/-- Under down-role + sign-duality + structural sum (+ positive EW orientation),
465 full `B_pow` principle constraints are equivalent to the active-edge unit
466 magnitude condition `natAbs ew = A`. -/
467theorem bpow_principle_iff_active_unit_under_down_role (a : BPowAssignment)
468 (hDown : a.down = 2 * (E_total : ℤ) - 1)
469 (hSign : a.up = -a.ew)
470 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
471 (hEwPos : 0 < a.ew) :
472 bpowPrincipleConstraints a ↔ Int.natAbs a.ew = A := by
473 constructor
474 · intro hP
475 rcases hP with ⟨_hSign', hComp, _hUpNeg, _hEwPos', _hSum'⟩
476 have hLepton : a.lepton = -(2 * (E_passive : ℤ)) :=
477 bpow_lepton_forced_from_down_role_and_sign_sum a hDown hSign hSum
478 have hLepton22 : a.lepton = -22 := by
479 calc
480 a.lepton = -(2 * (E_passive : ℤ)) := hLepton
481 _ = -22 := by native_decide
482 have hDown23 : a.down = 23 := by
483 calc
484 a.down = 2 * (E_total : ℤ) - 1 := hDown
485 _ = 23 := by native_decide
486 have hLAbs : (Int.natAbs a.lepton : ℤ) = 22 := by
487 rw [hLepton22]
488 native_decide
489 have hEAbsZ : (Int.natAbs a.ew : ℤ) = 1 := by
490 nlinarith [hComp, hLAbs, hDown23]
491 have hEAbsNat : Int.natAbs a.ew = 1 := by
492 exact_mod_cast hEAbsZ
493 have hA1 : A = 1 := by native_decide
494 simpa [hA1] using hEAbsNat
495 · intro hEwMag
496 exact bpow_principle_constraints_forced_from_edge_roles a hDown hSign hEwPos hEwMag hSum
497
498/-- Same equivalence using passive/down roles and structural sum, with sign derived internally. -/
499theorem bpow_principle_iff_active_unit_under_passive_down_roles (a : BPowAssignment)
500 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
501 (hDown : a.down = 2 * (E_total : ℤ) - 1)
502 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
503 (hEwPos : 0 < a.ew) :
504 bpowPrincipleConstraints a ↔ Int.natAbs a.ew = A := by
505 have hSign : a.up = -a.ew :=
506 bpow_sign_forced_from_lepton_down_sum a hLepton hDown hSum
507 exact bpow_principle_iff_active_unit_under_down_role a hDown hSign hSum hEwPos
508
509/-- Boolean-filter equivalence form of `bpow_principle_iff_active_unit_under_down_role`. -/
510theorem bpow_bool_constraints_iff_active_unit_under_down_role (a : BPowAssignment)
511 (hDown : a.down = 2 * (E_total : ℤ) - 1)
512 (hSign : a.up = -a.ew)
513 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
514 (hEwPos : 0 < a.ew) :
515 bpowStructuralConstraints a = true ↔ Int.natAbs a.ew = A := by
516 rw [bpow_constraints_true_iff]
517 exact bpow_principle_iff_active_unit_under_down_role a hDown hSign hSum hEwPos
518
519/-- Boolean-filter equivalence form using passive/down roles and structural sum. -/
520theorem bpow_bool_constraints_iff_active_unit_under_passive_down_roles (a : BPowAssignment)
521 (hLepton : a.lepton = -(2 * (E_passive : ℤ)))
522 (hDown : a.down = 2 * (E_total : ℤ) - 1)
523 (hSum : a.lepton + a.up + a.down + a.ew = bpowSumTarget)
524 (hEwPos : 0 < a.ew) :
525 bpowStructuralConstraints a = true ↔ Int.natAbs a.ew = A := by
526 rw [bpow_constraints_true_iff]
527 exact bpow_principle_iff_active_unit_under_passive_down_roles a hLepton hDown hSum hEwPos
528
529/-! ## `r0` assignment search -/
530
531structure R0Assignment where
532 lepton : ℤ
533 up : ℤ
534 down : ℤ
535 ew : ℤ
536 deriving Repr, DecidableEq
537
538def canonicalR0 : R0Assignment :=
539 { lepton := 4 * (W : ℤ) - 6
540 , up := 2 * (W : ℤ) + (A : ℤ)
541 , down := (E_total : ℤ) - (W : ℤ)
542 , ew := 3 * (W : ℤ) + 4 }
543
544def r0ValuePool : List ℤ :=
545 [ 4 * (W : ℤ) - 6
546 , 2 * (W : ℤ) + (A : ℤ)
547 , (E_total : ℤ) - (W : ℤ)
548 , 3 * (W : ℤ) + 4 ]
549
550theorem r0_pool_matches_anchor_formulas :
551 r0ValuePool =
552 [r0 .Lepton, r0 .UpQuark, r0 .DownQuark, r0 .Electroweak] := by
553 rfl
554
555def listToR0Assignment? : List ℤ → Option R0Assignment
556 | [l, u, d, e] => some { lepton := l, up := u, down := d, ew := e }
557 | _ => none
558
559def allR0Assignments : List R0Assignment :=
560 (r0ValuePool.permutations.filterMap listToR0Assignment?)
561
562/-- Structural r0 sum target (`V * W + E_passive = 147`). -/
563def r0SumTarget : ℤ :=
564 (Constants.AlphaDerivation.cube_vertices Constants.AlphaDerivation.D : ℤ) *
565 (Constants.AlphaDerivation.wallpaper_groups : ℤ) +
566 (Constants.AlphaDerivation.passive_field_edges Constants.AlphaDerivation.D : ℤ)
567
568theorem r0_sum_target_eq_147 : r0SumTarget = 147 := by
569 native_decide
570
571theorem r0_sum_target_matches_principle :
572 r0SumTarget =
573 (r0 .Lepton + r0 .UpQuark + r0 .DownQuark + r0 .Electroweak) := by
574 calc
575 r0SumTarget = 147 := r0_sum_target_eq_147
576 _ = (r0 .Lepton + r0 .UpQuark + r0 .DownQuark + r0 .Electroweak) := by
577 symm
578 exact YardstickAssignmentPrinciple.r0_sum
579
580/-- Structural constraints used to filter `r0` assignments. -/
581def r0StructuralConstraints (a : R0Assignment) : Bool :=
582 decide (a.down < 0) &&
583 decide (a.lepton > a.ew) &&
584 decide (a.ew > a.up) &&
585 decide (a.lepton + a.up + a.down + a.ew = r0SumTarget)
586
587/-- Prop-level version of `r0StructuralConstraints`. -/
588def r0PrincipleConstraints (a : R0Assignment) : Prop :=
589 a.down < 0 ∧
590 a.lepton > a.ew ∧
591 a.ew > a.up ∧
592 (a.lepton + a.up + a.down + a.ew = r0SumTarget)
593
594def validR0Assignments : List R0Assignment :=
595 allR0Assignments.filter r0StructuralConstraints
596
597theorem all_r0_assignments_count : allR0Assignments.length = 24 := by
598 native_decide
599
600theorem valid_r0_assignment_count : validR0Assignments.length = 1 := by
601 native_decide
602
603theorem valid_r0_assignments_are_singleton :
604 validR0Assignments = [canonicalR0] := by
605 native_decide
606
607theorem r0_constraints_true_iff (a : R0Assignment) :
608 r0StructuralConstraints a = true ↔ r0PrincipleConstraints a := by
609 unfold r0StructuralConstraints r0PrincipleConstraints
610 simp
611 tauto
612
613theorem r0_constraints_force_canonical (a : R0Assignment)
614 (ha : a ∈ allR0Assignments)
615 (hP : r0PrincipleConstraints a) :
616 a = canonicalR0 := by
617 have htrue : r0StructuralConstraints a = true := (r0_constraints_true_iff a).2 hP
618 have hmem : a ∈ validR0Assignments := by
619 unfold validR0Assignments
620 exact List.mem_filter.mpr ⟨ha, htrue⟩
621 rw [valid_r0_assignments_are_singleton] at hmem
622 simpa using hmem
623
624/-- Unrestricted forcing (no finite-pool membership): if the up/down affine roles and
625 lepton-vs-EW depth gap are fixed by the cube hierarchy, the structural sum target
626 already forces the full canonical `r0` assignment. -/
627theorem r0_unrestricted_forcing_from_affine_roles_and_sum (a : R0Assignment)
628 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
629 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
630 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10)
631 (hSum : a.lepton + a.up + a.down + a.ew = r0SumTarget) :
632 a = canonicalR0 := by
633 have hsum147 : a.lepton + a.up + a.down + a.ew = 147 := by
634 simpa [r0_sum_target_eq_147] using hSum
635 have hUp35 : a.up = 35 := by
636 calc
637 a.up = 2 * (W : ℤ) + (A : ℤ) := hUpRole
638 _ = 35 := by native_decide
639 have hDownNeg5 : a.down = -5 := by
640 calc
641 a.down = (E_total : ℤ) - (W : ℤ) := hDownRole
642 _ = -5 := by native_decide
643 have hGap7 : a.lepton - a.ew = 7 := by
644 calc
645 a.lepton - a.ew = (W : ℤ) - 10 := hDepthGap
646 _ = 7 := by native_decide
647 have hLeptonPlusEw : a.lepton + a.ew = 117 := by
648 nlinarith [hsum147, hUp35, hDownNeg5]
649 have hLepton62 : a.lepton = 62 := by
650 nlinarith [hLeptonPlusEw, hGap7]
651 have hEw55 : a.ew = 55 := by
652 nlinarith [hLeptonPlusEw, hGap7]
653 rcases a with ⟨l, u, d, e⟩
654 simp at hLepton62 hUp35 hDownNeg5 hEw55
655 subst l
656 subst u
657 subst d
658 subst e
659 rfl
660
661/-- Under fixed affine up/down roles and structural sum, the depth-gap condition is
662 equivalent to fixing the EW rung to its canonical affine formula. -/
663theorem r0_depth_gap_iff_ew_role_under_affine_roles_and_sum (a : R0Assignment)
664 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
665 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
666 (hSum : a.lepton + a.up + a.down + a.ew = r0SumTarget) :
667 (a.lepton - a.ew = (W : ℤ) - 10) ↔ (a.ew = 3 * (W : ℤ) + 4) := by
668 have hsum147 : a.lepton + a.up + a.down + a.ew = 147 := by
669 simpa [r0_sum_target_eq_147] using hSum
670 have hUp35 : a.up = 35 := by
671 calc
672 a.up = 2 * (W : ℤ) + (A : ℤ) := hUpRole
673 _ = 35 := by native_decide
674 have hDownNeg5 : a.down = -5 := by
675 calc
676 a.down = (E_total : ℤ) - (W : ℤ) := hDownRole
677 _ = -5 := by native_decide
678 have hLeptonPlusEw : a.lepton + a.ew = 117 := by
679 nlinarith [hsum147, hUp35, hDownNeg5]
680 constructor
681 · intro hDepthGap
682 have hGap7 : a.lepton - a.ew = 7 := by
683 calc
684 a.lepton - a.ew = (W : ℤ) - 10 := hDepthGap
685 _ = 7 := by native_decide
686 have hEw55 : a.ew = 55 := by
687 nlinarith [hLeptonPlusEw, hGap7]
688 calc
689 a.ew = 55 := hEw55
690 _ = 3 * (W : ℤ) + 4 := by native_decide
691 · intro hEwRole
692 have hEw55 : a.ew = 55 := by
693 calc
694 a.ew = 3 * (W : ℤ) + 4 := hEwRole
695 _ = 55 := by native_decide
696 have hLepton62 : a.lepton = 62 := by
697 nlinarith [hLeptonPlusEw, hEw55]
698 have hGap7 : a.lepton - a.ew = 7 := by
699 nlinarith [hLepton62, hEw55]
700 calc
701 a.lepton - a.ew = 7 := hGap7
702 _ = (W : ℤ) - 10 := by native_decide
703
704/-- Alternate unrestricted forcing route: fix affine up/down roles, EW affine role,
705 and structural sum; depth gap is then forced and canonical `r0` follows. -/
706theorem r0_unrestricted_forcing_from_affine_roles_and_ew_role (a : R0Assignment)
707 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
708 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
709 (hEwRole : a.ew = 3 * (W : ℤ) + 4)
710 (hSum : a.lepton + a.up + a.down + a.ew = r0SumTarget) :
711 a = canonicalR0 := by
712 have hDepthGap : a.lepton - a.ew = (W : ℤ) - 10 :=
713 (r0_depth_gap_iff_ew_role_under_affine_roles_and_sum a hUpRole hDownRole hSum).2 hEwRole
714 exact r0_unrestricted_forcing_from_affine_roles_and_sum a hUpRole hDownRole hDepthGap hSum
715
716/-- Unrestricted forcing (no finite-pool membership): under affine roles + depth gap,
717 the full principle constraints force canonical `r0`. -/
718theorem r0_unrestricted_forcing_from_affine_roles (a : R0Assignment)
719 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
720 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
721 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10)
722 (hP : r0PrincipleConstraints a) :
723 a = canonicalR0 := by
724 rcases hP with ⟨_hDownNeg, _hLeptonGtEw, _hEwGtUp, hSum⟩
725 exact r0_unrestricted_forcing_from_affine_roles_and_sum a hUpRole hDownRole hDepthGap hSum
726
727/-- Under fixed affine up/down roles and depth gap, full prop-level `r0` constraints
728 are equivalent to the structural sum target alone (order conjuncts become derived). -/
729theorem r0_principle_iff_sum_under_affine_roles_and_depth_gap (a : R0Assignment)
730 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
731 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
732 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10) :
733 r0PrincipleConstraints a ↔
734 (a.lepton + a.up + a.down + a.ew = r0SumTarget) := by
735 constructor
736 · intro hP
737 exact hP.2.2.2
738 · intro hSum
739 have hcanon : a = canonicalR0 :=
740 r0_unrestricted_forcing_from_affine_roles_and_sum a hUpRole hDownRole hDepthGap hSum
741 rw [hcanon]
742 unfold r0PrincipleConstraints canonicalR0
743 repeat' constructor <;> native_decide
744
745/-- Boolean filter form of `r0_principle_iff_sum_under_affine_roles_and_depth_gap`. -/
746theorem r0_bool_constraints_iff_sum_under_affine_roles_and_depth_gap (a : R0Assignment)
747 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
748 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
749 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10) :
750 r0StructuralConstraints a = true ↔
751 (a.lepton + a.up + a.down + a.ew = r0SumTarget) := by
752 rw [r0_constraints_true_iff]
753 exact r0_principle_iff_sum_under_affine_roles_and_depth_gap a hUpRole hDownRole hDepthGap
754
755/-- Once affine roles + depth gap + structural sum are fixed, the full
756 prop-level `r0` principle constraints are derived (no independent order axioms). -/
757theorem r0_principle_constraints_forced_from_affine_roles_and_sum (a : R0Assignment)
758 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
759 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
760 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10)
761 (hSum : a.lepton + a.up + a.down + a.ew = r0SumTarget) :
762 r0PrincipleConstraints a := by
763 have hcanon : a = canonicalR0 :=
764 r0_unrestricted_forcing_from_affine_roles_and_sum a hUpRole hDownRole hDepthGap hSum
765 rw [hcanon]
766 unfold r0PrincipleConstraints canonicalR0
767 repeat' constructor <;> native_decide
768
769/-- Boolean filter form of the previous theorem. -/
770theorem r0_bool_constraints_forced_from_affine_roles_and_sum (a : R0Assignment)
771 (hUpRole : a.up = 2 * (W : ℤ) + (A : ℤ))
772 (hDownRole : a.down = (E_total : ℤ) - (W : ℤ))
773 (hDepthGap : a.lepton - a.ew = (W : ℤ) - 10)
774 (hSum : a.lepton + a.up + a.down + a.ew = r0SumTarget) :
775 r0StructuralConstraints a = true := by
776 exact (r0_constraints_true_iff a).2 <|
777 r0_principle_constraints_forced_from_affine_roles_and_sum a hUpRole hDownRole hDepthGap hSum
778
779/-! ## Link to `Masses.Anchor` -/
780
781def anchorBPowAssignment : BPowAssignment :=
782 { lepton := B_pow .Lepton
783 , up := B_pow .UpQuark
784 , down := B_pow .DownQuark
785 , ew := B_pow .Electroweak }
786
787def anchorR0Assignment : R0Assignment :=
788 { lepton := r0 .Lepton
789 , up := r0 .UpQuark
790 , down := r0 .DownQuark
791 , ew := r0 .Electroweak }
792
793theorem anchor_bpow_matches_canonical :
794 anchorBPowAssignment = canonicalBPow := by
795 native_decide
796
797theorem anchor_r0_matches_canonical :
798 anchorR0Assignment = canonicalR0 := by
799 native_decide
800
801theorem anchor_is_unique_valid_bpow :
802 anchorBPowAssignment ∈ validBPowAssignments := by
803 rw [valid_bpow_assignments_are_singleton, anchor_bpow_matches_canonical]
804 simp
805
806theorem anchor_is_unique_valid_r0 :
807 anchorR0Assignment ∈ validR0Assignments := by
808 rw [valid_r0_assignments_are_singleton, anchor_r0_matches_canonical]
809 simp
810
811/-- The `B_pow` filter constraints are satisfied by the anchor assignment,
812 with each conjunct matching a proved structural identity from
813 `YardstickAssignmentPrinciple`. -/
814theorem anchor_bpow_structural_identities :
815 anchorBPowAssignment.up = -anchorBPowAssignment.ew ∧
816 ((Int.natAbs anchorBPowAssignment.lepton : ℤ) +
817 (Int.natAbs anchorBPowAssignment.ew : ℤ) = anchorBPowAssignment.down) ∧
818 anchorBPowAssignment.up < 0 ∧
819 0 < anchorBPowAssignment.ew ∧
820 (anchorBPowAssignment.lepton + anchorBPowAssignment.up +
821 anchorBPowAssignment.down + anchorBPowAssignment.ew = bpowSumTarget) := by
822 refine ⟨?_, ?_, ?_, ?_, ?_⟩
823 · simp [anchorBPowAssignment]
824 · simpa [anchorBPowAssignment] using
825 YardstickAssignmentPrinciple.lepton_ew_natAbs_complement_down
826 · simpa [anchorBPowAssignment] using
827 YardstickAssignmentPrinciple.up_negative_and_ew_positive.1
828 · simpa [anchorBPowAssignment] using
829 YardstickAssignmentPrinciple.up_negative_and_ew_positive.2
830 · simpa [anchorBPowAssignment, add_comm, add_left_comm, add_assoc] using
831 bpow_sum_target_matches_principle.symm
832
833theorem anchor_bpow_constraints_from_principle :
834 bpowStructuralConstraints anchorBPowAssignment = true := by
835 rcases anchor_bpow_structural_identities with ⟨hSign, _hComp, hUpNeg, hEwPos, hSum⟩
836 have hCompAbs : |anchorBPowAssignment.lepton| + |anchorBPowAssignment.ew| = anchorBPowAssignment.down := by
837 simpa [anchorBPowAssignment] using YardstickAssignmentPrinciple.lepton_ew_complement_down
838 have dSign : decide (anchorBPowAssignment.up = -anchorBPowAssignment.ew) = true :=
839 decide_eq_true hSign
840 have dUpNeg : decide (anchorBPowAssignment.up < 0) = true := decide_eq_true hUpNeg
841 have dEwPos : decide (0 < anchorBPowAssignment.ew) = true := decide_eq_true hEwPos
842 have dSum :
843 decide (anchorBPowAssignment.lepton + anchorBPowAssignment.up +
844 anchorBPowAssignment.down + anchorBPowAssignment.ew = bpowSumTarget) = true :=
845 decide_eq_true hSum
846 unfold bpowStructuralConstraints
847 simp [hCompAbs, dSign, dUpNeg, dEwPos, dSum]
848
849/-- The `r0` filter constraints are satisfied by the anchor assignment,
850 and each conjunct corresponds to proved ordering/sum identities. -/
851theorem anchor_r0_structural_identities :
852 anchorR0Assignment.down < 0 ∧
853 anchorR0Assignment.lepton > anchorR0Assignment.ew ∧
854 anchorR0Assignment.ew > anchorR0Assignment.up ∧
855 (anchorR0Assignment.lepton + anchorR0Assignment.up +
856 anchorR0Assignment.down + anchorR0Assignment.ew = r0SumTarget) := by
857 refine ⟨?_, ?_, ?_, ?_⟩
858 · simpa [anchorR0Assignment] using YardstickAssignmentPrinciple.r0_order_constraints.1
859 · simpa [anchorR0Assignment] using YardstickAssignmentPrinciple.r0_order_constraints.2.1
860 · simpa [anchorR0Assignment] using YardstickAssignmentPrinciple.r0_order_constraints.2.2
861 · simpa [anchorR0Assignment, add_comm, add_left_comm, add_assoc] using
862 r0_sum_target_matches_principle.symm
863
864theorem anchor_r0_constraints_from_principle :
865 r0StructuralConstraints anchorR0Assignment = true := by
866 rcases anchor_r0_structural_identities with ⟨hDownNeg, hLeptonGtEw, hEwGtUp, hSum⟩
867 have dDownNeg : decide (anchorR0Assignment.down < 0) = true := decide_eq_true hDownNeg
868 have dLeptonGtEw : decide (anchorR0Assignment.lepton > anchorR0Assignment.ew) = true :=
869 decide_eq_true hLeptonGtEw
870 have dEwGtUp : decide (anchorR0Assignment.ew > anchorR0Assignment.up) = true :=
871 decide_eq_true hEwGtUp
872 have dSum :
873 decide (anchorR0Assignment.lepton + anchorR0Assignment.up +
874 anchorR0Assignment.down + anchorR0Assignment.ew = r0SumTarget) = true :=
875 decide_eq_true hSum
876 unfold r0StructuralConstraints
877 simp [dDownNeg, dLeptonGtEw, dEwGtUp, dSum]
878
879/-- Enumerated-choice closure summary for O1 (current constraint set). -/
880theorem yardstick_choice_sets_collapsed :
881 validBPowAssignments = [canonicalBPow] ∧
882 validR0Assignments = [canonicalR0] := by
883 exact ⟨valid_bpow_assignments_are_singleton, valid_r0_assignments_are_singleton⟩
884
885/-- Joint unrestricted forcing: once the cube-role couplings are fixed, both
886 yardstick layers are forced by role-kernel assumptions plus structural sums,
887 without finite enumeration and without directly assuming full filter bundles. -/
888theorem yardstick_unrestricted_forcing_from_role_kernels_and_sums
889 (b : BPowAssignment) (r : R0Assignment)
890 (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
891 (hbDown : b.down = 2 * (E_total : ℤ) - 1)
892 (hbEwPos : 0 < b.ew)
893 (hbEwMag : Int.natAbs b.ew = A)
894 (hbSum : b.lepton + b.up + b.down + b.ew = bpowSumTarget)
895 (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
896 (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
897 (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
898 (hrSum : r.lepton + r.up + r.down + r.ew = r0SumTarget) :
899 b = canonicalBPow ∧ r = canonicalR0 := by
900 exact
901 ⟨ bpow_unrestricted_forcing_from_passive_down_roles
902 b hbLepton hbDown hbEwPos hbEwMag hbSum
903 , r0_unrestricted_forcing_from_affine_roles_and_sum
904 r hrUpRole hrDownRole hrDepthGap hrSum ⟩
905
906/-- Joint unrestricted forcing: once the cube-role couplings are fixed, both
907 yardstick layers are forced to their canonical assignments without finite enumeration.
908 This version uses only the structural sum on the `r0` side (order/filter conjuncts
909 are derived under affine roles + depth gap). -/
910theorem yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum
911 (b : BPowAssignment) (r : R0Assignment)
912 (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
913 (hbP : bpowPrincipleConstraints b)
914 (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
915 (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
916 (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
917 (hrSum : r.lepton + r.up + r.down + r.ew = r0SumTarget) :
918 b = canonicalBPow ∧ r = canonicalR0 := by
919 exact
920 ⟨ bpow_unrestricted_forcing_from_passive_coupling b hbLepton hbP
921 , r0_unrestricted_forcing_from_affine_roles_and_sum r hrUpRole hrDownRole hrDepthGap hrSum ⟩
922
923/-- Joint unrestricted forcing: once the cube-role couplings are fixed, both
924 yardstick layers are forced to their canonical assignments without finite enumeration. -/
925theorem yardstick_unrestricted_forcing_from_cube_roles
926 (b : BPowAssignment) (r : R0Assignment)
927 (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
928 (hbP : bpowPrincipleConstraints b)
929 (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
930 (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
931 (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
932 (hrP : r0PrincipleConstraints r) :
933 b = canonicalBPow ∧ r = canonicalR0 := by
934 exact yardstick_unrestricted_forcing_from_cube_roles_and_r0_sum
935 b r hbLepton hbP hrUpRole hrDownRole hrDepthGap hrP.2.2.2
936
937/-- Cube-partition principle packaging:
938 role-kernel assumptions plus structural sums force the full admissibility filter
939 family for both `B_pow` and `r0` (without finite enumeration). -/
940theorem yardstick_filter_family_forced_from_cube_partition_principle
941 (b : BPowAssignment) (r : R0Assignment)
942 (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
943 (hbDown : b.down = 2 * (E_total : ℤ) - 1)
944 (hbEwPos : 0 < b.ew)
945 (hbEwMag : Int.natAbs b.ew = A)
946 (hbSum : b.lepton + b.up + b.down + b.ew = bpowSumTarget)
947 (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
948 (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
949 (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
950 (hrSum : r.lepton + r.up + r.down + r.ew = r0SumTarget) :
951 bpowPrincipleConstraints b ∧ r0PrincipleConstraints r := by
952 refine ⟨?_, ?_⟩
953 · have hbSign : b.up = -b.ew :=
954 bpow_sign_forced_from_lepton_down_sum b hbLepton hbDown hbSum
955 exact bpow_principle_constraints_forced_from_edge_roles
956 b hbDown hbSign hbEwPos hbEwMag hbSum
957 · exact r0_principle_constraints_forced_from_affine_roles_and_sum
958 r hrUpRole hrDownRole hrDepthGap hrSum
959
960/-- Cube-partition first-principles forcing:
961 once the role kernels and structural sums are fixed, sector yardstick assignments
962 are uniquely forced to the canonical formulas. -/
963theorem yardstick_assignment_forced_from_cube_partition_principle
964 (b : BPowAssignment) (r : R0Assignment)
965 (hbLepton : b.lepton = -(2 * (E_passive : ℤ)))
966 (hbDown : b.down = 2 * (E_total : ℤ) - 1)
967 (hbEwPos : 0 < b.ew)
968 (hbEwMag : Int.natAbs b.ew = A)
969 (hbSum : b.lepton + b.up + b.down + b.ew = bpowSumTarget)
970 (hrUpRole : r.up = 2 * (W : ℤ) + (A : ℤ))
971 (hrDownRole : r.down = (E_total : ℤ) - (W : ℤ))
972 (hrDepthGap : r.lepton - r.ew = (W : ℤ) - 10)
973 (hrSum : r.lepton + r.up + r.down + r.ew = r0SumTarget) :
974 b = canonicalBPow ∧ r = canonicalR0 := by
975 exact yardstick_unrestricted_forcing_from_role_kernels_and_sums
976 b r hbLepton hbDown hbEwPos hbEwMag hbSum hrUpRole hrDownRole hrDepthGap hrSum
977
978/-- O1' uniqueness surface (iff form):
979 canonical yardstick assignments are equivalent to the cube-partition
980 role-kernel + structural-sum principle package. -/
981theorem yardstick_assignment_iff_cube_partition_principle
982 (b : BPowAssignment) (r : R0Assignment) :
983 (b = canonicalBPow ∧ r = canonicalR0) ↔
984 (b.lepton = -(2 * (E_passive : ℤ)) ∧
985 b.down = 2 * (E_total : ℤ) - 1 ∧
986 0 < b.ew ∧
987 Int.natAbs b.ew = A ∧
988 (b.lepton + b.up + b.down + b.ew = bpowSumTarget) ∧
989 r.up = 2 * (W : ℤ) + (A : ℤ) ∧
990 r.down = (E_total : ℤ) - (W : ℤ) ∧
991 r.lepton - r.ew = (W : ℤ) - 10 ∧
992 (r.lepton + r.up + r.down + r.ew = r0SumTarget)) := by
993 constructor
994 · intro h
995 rcases h with ⟨hb, hr⟩
996 subst hb
997 subst hr
998 repeat' constructor <;> native_decide
999 · intro h
1000 rcases h with ⟨hbLepton, hbDown, hbEwPos, hbEwMag, hbSum, hrUpRole, hrDownRole, hrDepthGap, hrSum⟩
1001 exact yardstick_assignment_forced_from_cube_partition_principle
1002 b r hbLepton hbDown hbEwPos hbEwMag hbSum hrUpRole hrDownRole hrDepthGap hrSum
1003
1004end YardstickAssignmentChoiceSet
1005end Verification
1006end IndisputableMonolith
1007