Encyclopedia Masses Masses Sector Dependent Torsion Closure Leading Step Breaks Duality As Required
ARTICLE 3 claims 2 theorems 1 hypothesis
Masses Sector Dependent Torsion Closure Leading Step Breaks Duality As Required
A machine-checked proof shows why the first step in a particle mass ladder must break a symmetry, and what that symmetry breaking is not allowed to do.
The duality-breaking step
In geometry, duality is a mirror: a cube has 8 vertices and 6 faces, and swapping the two lists gives another valid shape. The Recognition Science framework models particle masses as a ladder of steps, each step a count of cube cells at a certain dimension. The declaration closureLeadingStep_breaks_duality_as_required proves that the first step of the up-quark ladder, the number 13, cannot be produced by any rule that respects this mirror symmetry. The proof is a theorem in the framework's machine-checked library of formal theorems.
The reason is a counting argument. The up-quark step 13 equals the number of vertices plus faces minus edges of a 3-dimensional cube: 8 + 6 - 12 = 2, which is not 13. The framework instead derives the step from a closure principle: the recognition orbit is a 1-cycle, so closed loops live at dimension 1; only the vertex coupling dimension 0 lies below it and cannot host the loop, so it must borrow its dual face, producing exactly V + F - C. The threshold sits at the self-dual fixed point 1 = 2 - 1, which is why the rule is duality-breaking yet not free. The theorem dualAware_reproduces_up_only confirms that this rule reproduces the up step 13 but fails for the lepton step 11 and the down step 8.
What the declaration does not claim is that the framework derives which fermion sector uses which cell-count pair from first principles. The assignment of the pairs {13, 11} to up quarks, {11, 6} to leptons, and {6, 8} to down quarks was identified from particle data, not forced by the mathematics. The Lean proofs verify the algebraic properties of these integers, not the physical reason each sector uses them. The framework proves that the up excess is not duality-forced, and that the closure principle supplies the required duality-breaker, but the naming of the sectors remains conventional.
THEOREM up_excess_not_duality_forced · dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- **THEOREM (OBSTRUCTION: the colored step asymmetry is not fixed by any duality-invariant rule).**
The colored sectors sit at the duality-dual extreme coupling dimensions `d=0` (up) and `d=2`
(down). Any rule `r : ℕ → ℕ` that is a function of the duality-invariant data (`r d = r (2−d)` for
all `d`) and matches the observed colored leading steps (`r 0 = up_step_12`, `r 2 = down_step_12`)
is CONTRADICTORY: duality-invariance forces `r 0 = r 2`, but `up_step_12 = 13 ≠ 6 = down_step_12`.
Hence the selection that gives the up sector the dual-aware count and the down sector the bare
passive count is a duality-BREAKING choice — it cannot be read off the cube's duality-invariant
combinatorics. The residual up excess `F−C` is therefore the measured physical up/down
generation-spread asymmetry, a MODEL input, not a derivation gap. This CLOSES the generation
step alphabet modulo exactly one named, code-cited physical datum. Kernel axioms only. -/
theorem up_excess_not_duality_forced
(r : ℕ → ℕ) (hr : ∀ d, r d = r (2 - d))
(hup : r 0 = up_step_12) (hdown : r 2 = down_step_12) : False := by
have h02 : r 0 = r 2 := by have h := hr 0; simpa using h
rw [hup, hdown] at h02
exact absurd h02 (by decide)
/-- **OBSTRUCTION (dual-aware rule reproduces up only).** The dual-aware leading-step rule
`n(d)+n(2−d)−C` uniquely DERIVES the anomalous up composite `V+F−C` at `d=0` but fails for
lepton and down. So even the duality-aware refinement of the CW rule is non-uniform: the up
composite is dual-aware (connecting the alphabet to the cube↔octahedron pairing), yet the
alphabet as a whole is generated by neither the uniform-CW nor the uniform dual-aware rule.
The residual external input on the step values is genuinely non-uniform. Kernel axioms only. -/
theorem dualAware_reproduces_up_only :
dualAwareStep12 0 = up_step_12 ∧
dualAwareStep12 1 ≠ lepton_step_12 ∧
dualAwareStep12 2 ≠ down_step_12 :=
⟨dualAware_reproduces_up, dualAware_fails_lepton, dualAware_fails_down⟩
THEOREM dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- **OBSTRUCTION (dual-aware rule reproduces up only).** The dual-aware leading-step rule
`n(d)+n(2−d)−C` uniquely DERIVES the anomalous up composite `V+F−C` at `d=0` but fails for
lepton and down. So even the duality-aware refinement of the CW rule is non-uniform: the up
composite is dual-aware (connecting the alphabet to the cube↔octahedron pairing), yet the
alphabet as a whole is generated by neither the uniform-CW nor the uniform dual-aware rule.
The residual external input on the step values is genuinely non-uniform. Kernel axioms only. -/
theorem dualAware_reproduces_up_only :
dualAwareStep12 0 = up_step_12 ∧
dualAwareStep12 1 ≠ lepton_step_12 ∧
dualAwareStep12 2 ≠ down_step_12 :=
⟨dualAware_reproduces_up, dualAware_fails_lepton, dualAware_fails_down⟩
HYPOTHESIS forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- The forced chain's three windows are exactly the up / lepton / down sector
step-pairs. Reads the chain `[13,11,6,8]` off as (up, lepton, down). Kernel
axioms only. -/
theorem forced_chain_windows :
(13, 11) = (up_step_12, up_step_23) ∧
(11, 6) = (lepton_step_12, lepton_step_23) ∧
(6, 8) = (down_step_12, down_step_23) := by
refine ⟨?_, ?_, ?_⟩ <;> (apply Prod.ext <;> decide)
What this page does not claim
The framework does not derive which fermion sector uses which cell-count pair from first principles. The declaration does not prove that the up-quark step 13 is physically realized; it proves a mathematical property of the integers. The framework does not claim that the duality-breaking rule is unique; it shows that one specific duality-invariant rule fails.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/SectorDependentTorsion.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What physical principle, if any, forces the assignment of specific cell-count pairs to specific fermion sectors?
- How does the closure principle generalize to other dimensions beyond the 3-dimensional cube?
- What experimental measurement would falsify the hypothesis that up quarks use the pair {13, 11}?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM up_excess_not_duality_forced · dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- **THEOREM (OBSTRUCTION: the colored step asymmetry is not fixed by any duality-invariant rule).** The colored sectors sit at the duality-dual extreme coupling dimensions `d=0` (up) and `d=2` (down). Any rule `r : ℕ → ℕ` that is a function of the duality-invariant data (`r d = r (2−d)` for all `d`) and matches the observed colored leading steps (`r 0 = up_step_12`, `r 2 = down_step_12`) is CONTRADICTORY: duality-invariance forces `r 0 = r 2`, but `up_step_12 = 13 ≠ 6 = down_step_12`. Hence the selection that gives the up sector the dual-aware count and the down sector the bare passive count is a duality-BREAKING choice — it cannot be read off the cube's duality-invariant combinatorics. The residual up excess `F−C` is therefore the measured physical up/down generation-spread asymmetry, a MODEL input, not a derivation gap. This CLOSES the generation step alphabet modulo exactly one named, code-cited physical datum. Kernel axioms only. -/ theorem up_excess_not_duality_forced (r : ℕ → ℕ) (hr : ∀ d, r d = r (2 - d)) (hup : r 0 = up_step_12) (hdown : r 2 = down_step_12) : False := by have h02 : r 0 = r 2 := by have h := hr 0; simpa using h rw [hup, hdown] at h02 exact absurd h02 (by decide)/-- **OBSTRUCTION (dual-aware rule reproduces up only).** The dual-aware leading-step rule `n(d)+n(2−d)−C` uniquely DERIVES the anomalous up composite `V+F−C` at `d=0` but fails for lepton and down. So even the duality-aware refinement of the CW rule is non-uniform: the up composite is dual-aware (connecting the alphabet to the cube↔octahedron pairing), yet the alphabet as a whole is generated by neither the uniform-CW nor the uniform dual-aware rule. The residual external input on the step values is genuinely non-uniform. Kernel axioms only. -/ theorem dualAware_reproduces_up_only : dualAwareStep12 0 = up_step_12 ∧ dualAwareStep12 1 ≠ lepton_step_12 ∧ dualAwareStep12 2 ≠ down_step_12 := ⟨dualAware_reproduces_up, dualAware_fails_lepton, dualAware_fails_down⟩The declaration closureLeadingStep_breaks_duality_as_required proves that the first step of the up-quark ladder, the number 13, cannot be produced by any rule that respects this mirror symmetry. up_excess_not_duality_forced · dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.leanTHEOREM dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- **OBSTRUCTION (dual-aware rule reproduces up only).** The dual-aware leading-step rule `n(d)+n(2−d)−C` uniquely DERIVES the anomalous up composite `V+F−C` at `d=0` but fails for lepton and down. So even the duality-aware refinement of the CW rule is non-uniform: the up composite is dual-aware (connecting the alphabet to the cube↔octahedron pairing), yet the alphabet as a whole is generated by neither the uniform-CW nor the uniform dual-aware rule. The residual external input on the step values is genuinely non-uniform. Kernel axioms only. -/ theorem dualAware_reproduces_up_only : dualAwareStep12 0 = up_step_12 ∧ dualAwareStep12 1 ≠ lepton_step_12 ∧ dualAwareStep12 2 ≠ down_step_12 := ⟨dualAware_reproduces_up, dualAware_fails_lepton, dualAware_fails_down⟩The theorem dualAware_reproduces_up_only confirms that this rule reproduces the up step 13 but fails for the lepton step 11 and the down step 8. dualAware_reproduces_up_only · IndisputableMonolith/Masses/SectorDependentTorsion.leanHYPOTHESIS forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean
/-- The forced chain's three windows are exactly the up / lepton / down sector step-pairs. Reads the chain `[13,11,6,8]` off as (up, lepton, down). Kernel axioms only. -/ theorem forced_chain_windows : (13, 11) = (up_step_12, up_step_23) ∧ (11, 6) = (lepton_step_12, lepton_step_23) ∧ (6, 8) = (down_step_12, down_step_23) := by refine ⟨?_, ?_, ?_⟩ <;> (apply Prod.ext <;> decide)The assignment of the pairs {13, 11} to up quarks, {11, 6} to leptons, and {6, 8} to down quarks was identified from particle data, not forced by the mathematics. forced_chain_windows · IndisputableMonolith/Masses/SectorDependentTorsion.lean