Masses Baseline Derivation

Baseline derivation

Masses baseline derivation is the step in Recognition Science where the starting integers for particle mass rungs stop being assumed and start being derived. The module takes one input, the dimension D = 3, and from the standard combinatorics of the 3-cube Q₃ it proves the baseline values for leptons, quarks, neutrinos, octave offset, color offset, and generation ordering. The derivation principle is that every integer in the file traces to a single input: D = 3.

The key results are concrete. The recognition cost J(x) = (x + 1/x)/2 - 1 is nonnegative and zero only at x = 1, so a zero-cost transition is unobservable. The octave offset is -2^D = -8. The neutrino baseline is -(V + E + F + E_pass + W) = -54. The lepton baseline is A + 1 = 2. The quark baseline is 2^(D-1) = 4. The color offset is also 4. Generation ordering is 0 < 11 < 17. Each of these was previously a boundary assumption; the proofs here upgrade them to derived status.

The module also proves the rung structure. Lepton rungs sit at 2, 13, and 19. Quark rungs sit at 4, 15, and 21. The Z-map monotonicity theorem guarantees that the polynomial Z(a, b, q) = aq² + bq⁴ is strictly increasing in q when a and b are at least 1, which establishes completeness of the rung ordering. The theorems also match the derived baselines to the anchor integers for up, down, and electron, confirming the identification with the particle ladder.

What this establishes in plain language is that the numerical skeleton of the particle mass spectrum is not fitted. It is forced by the geometry of a cube once the dimension is fixed at 3. The module does not derive the actual masses, only the baseline integers from which the mass ladder is built. The comparison against measured particle masses remains an empirical check, not a theorem.

THEOREM octave_offset_eq · IndisputableMonolith/Masses/BaselineDerivation.lean

THEOREM neutrino_baseline_eq · IndisputableMonolith/Masses/BaselineDerivation.lean

THEOREM lepton_baseline_eq · IndisputableMonolith/Masses/BaselineDerivation.lean

THEOREM quark_baseline_eq · IndisputableMonolith/Masses/BaselineDerivation.lean

THEOREM Z_strictly_increasing · IndisputableMonolith/Masses/BaselineDerivation.lean

THEOREM lepton_rungs · IndisputableMonolith/Masses/BaselineDerivation.lean

What this page does not claim

This answer does not claim that actual particle masses are derived here, only the baseline integers. This answer does not claim the physical recognition-to-linking bridge is closed; that bridge remains open. This answer does not claim the fine-structure constant alpha is derived.

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/BaselineDerivation.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: