Masses Sector Dependent Torsion Closure Leading Step Reproduces Leading

The closure step

The declaration closureLeadingStep_reproduces_leading is a theorem in the framework's machine-checked library of formal theorems. It establishes that a specific algebraic rule, called the closure step, reproduces the leading numerical step in the up-quark generation ladder. The rule computes a cell count from a cube's vertices, faces, and edges, and the theorem shows that this computed value equals the previously identified up-quark step of 13. This is a formal, verified statement about integers, not a claim about physical measurements.

The framework models particle masses as numbers on a ladder, where each rung is a step between generations. Earlier work reduced six generation steps to a single scalar, the up leading-step excess, and showed that no duality-invariant rule could produce it. The closure step breaks duality in a specific way: it borrows a dual face because the recognition orbit is a 1-cycle, forcing the value V + F − C, which equals 13. The theorem closureLeadingStep_reproduces_leading verifies this arithmetic, and a companion theorem confirms the rule fails for the lepton and down-quark steps, which is what makes it specific to the up sector.

What the declaration does not claim is equally important. The assignment of cell-count pairs to specific fermion sectors, such as up quarks using {13, 11} and down quarks using {6, 8}, was identified from particle data, not derived from first principles. The framework's own documentation states this plainly: the quark assignments are hypotheses supported by data. The closure step supplies the required duality-breaker, but the physical reason why the up sector uses this particular rule, and why the down sector uses a different one, remains an open question. The theorem establishes the mathematics of the integers, not the physics of why each sector uses them.

In short, the declaration closes a gap in the algebraic chain: it shows that a single, forced rule can produce the leading up-quark step without fitting. But it does not derive the full sector assignment from scratch. The lepton torsion {11, 6} is fully derived, while the quark assignments remain hypotheses. The framework's library shows the numbers work; it does not yet show why nature chose them.

/-- **THEOREM (the up composite IS the dual-aware count).** The anomalous up leading step
    `V+F−C = 13` equals the dual-aware count `n(0)+n(2)−C` at the up coupling dimension — the
    vertex count plus its polar-dual face count minus the body. This is where the only
    non-atomic alphabet value comes from, and it is manifestly duality-aware. -/
theorem dualAware_reproduces_up : dualAwareStep12 0 = up_step_12 := 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 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 closure step does not derive the full assignment of cell-count pairs to all fermion sectors from first principles. The theorem does not show that the up-quark sector is physically distinct from the down-quark sector; that distinction remains a named convention. The rule's success for the up step does not imply it works for any other sector, as the theorem explicitly shows it fails for leptons and down quarks.

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: