Recog Spec Rsledger

The phi-ladder ledger

In physics, the masses of elementary particles are numbers you look up, not numbers you derive. The electron, muon, and tau lepton have masses that differ by factors of roughly 200, but no standard theory explains why those factors are what they are. Recognition Science approaches the problem with a different picture: particle masses occupy discrete rungs on a ladder, and the ratio of any two masses is the golden ratio φ raised to the difference in their rung numbers. The RSLedger structure defines this ladder and proves the arithmetic that connects it to the three generations of matter.

The core object is the ledger, a discrete record of events or values. The structure extends that idea into an RSLedger, which adds two pieces of data to the basic ledger: a base rung for each fermion sector (leptons, up quarks, down quarks) and a torsion offset for each generation. The full rung for a particle is the sum: rung = baseRung + torsion. The mass ratio between two particles in the same sector is then φ raised to the difference in their rungs, written as m_f / m_g = φ^(r_f - r_g). This is a definitional choice, a model, not a derived law.

The striking content of the structure is where the torsion offsets come from. They are not fitted to data; they are computed from the combinatorics of a three-dimensional cube. The first generation has torsion 0. The second generation has torsion 11, which is the number of passive field edges in the cube geometry minus one. The third generation has torsion 17, which adds the six faces of the cube to that same count. The structure proves these values by direct simplification: torsion_first, torsion_second, and torsion_third are theorems in the machine-checked library, each reducing to the definition by computation.

From those three numbers, the inter-generation mass ratios follow as theorems. The ratio of second to first generation mass is φ^11, the ratio of third to first is φ^17, and the ratio of third to second is φ^6. The structure proves these for any ledger whose torsion matches the canonical generation torsion, and it proves them for the specific canonical ledger. The theorems canonical_massRatio_21, canonical_massRatio_31, and canonical_massRatio_32 state these results in the library. A separate theorem, massRatios_from_torsion_structure, packages all three rung differences into a single statement.

What the structure establishes, in plain language, is a precise and checkable claim: if you accept the cube-geometry derivation of the torsion offsets, then the mass ratios between generations are forced to be powers of φ with exponents 11, 17, and 6. The exponents are not free parameters. The comparison against measured particle masses is an empirical check, not a theorem; the structure itself does not contain measured data. What it does contain is a clean arithmetic skeleton: three small integers, derived from a cube, that determine the spacing of the mass ladder.

/-- Mass ratio between generations from rung difference.

This is the key derivation: masses are φ^{rung}, so ratios are φ^{Δrung}.
-/
noncomputable def massRatioFromRungs (L : RSLedger) (φ : ℝ)
    (sector : FermionSector) (g1 g2 : Generation) : ℝ :=
  φ ^ (L.rungDiff sector g1 g2)

@[simp] lemma torsion_first : generationTorsion .first = 0 := rfl

@[simp] lemma torsion_second : generationTorsion .second = 11 := by
  simp [generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, D]

@[simp] lemma torsion_third : generationTorsion .third = 17 := by
  simp [generationTorsion, passive_field_edges, cube_edges, active_edges_per_tick, cube_faces, D]

/-- Canonical ledger mass ratios -/
theorem canonical_massRatio_21 (φ : ℝ) (sector : FermionSector) :
    massRatioFromRungs canonicalRSLedger φ sector .second .first = φ ^ (11 : ℤ) :=
  massRatio_21_canonical canonicalRSLedger φ sector canonicalRSLedger_torsion

theorem canonical_massRatio_31 (φ : ℝ) (sector : FermionSector) :
    massRatioFromRungs canonicalRSLedger φ sector .third .first = φ ^ (17 : ℤ) :=
  massRatio_31_canonical canonicalRSLedger φ sector canonicalRSLedger_torsion

What this page does not claim

This structure does not contain measured particle masses or any empirical comparison. The torsion offsets are derived from cube geometry, but the bridge proof is in a separate module, GenerationTorsionBridge. The mass ratio formula is a definitional model, not a derived law of the framework.

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/RecogSpec/RSLedger.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: