Masses Anchor Derivation

The anchor derivation

Masses anchor derivation is the part of Recognition Science that fixes the yardsticks for the particle mass sectors. A sector is a family of particles, such as leptons or quarks, that share a common scale. The derivation shows that each sector's two constants, the power B_pow and the offset r0, are forced by a small set of geometric facts. No free parameters are fitted to mass data.

The forcing chain begins with three spatial dimensions, D = 3, which itself comes from the linking closure theorem. From that dimension, a hypercube has 12 edges. One edge is active per tick, the atomic recognition step, leaving 11 passive field edges. The crystallographic wallpaper groups number 17. These five integers, 3, 12, 1, 11, and 17, are the only ingredients.

Each sector constant is a plain arithmetic combination of those ingredients. For the lepton sector, B_pow is -(2 × 11) = -22 and r0 is 4 × 17 - 6 = 62. For the up quark, B_pow is -1 and r0 is 35. For the down quark, B_pow is 23 and r0 is -5. For the electroweak sector, B_pow is 1 and r0 is 55. These values are not chosen; they are the outputs of the formulas.

The module AnchorDerivation.lean proves that the main definitions of these constants are definitionally equal to the alternative formulas built from the five geometric facts. Two theorems, B_pow_eq_alt and r0_eq_alt, check this equality for every sector. The proof is axiom-clean and uses only the standard Lean kernel postulates. This establishes, in formal terms, that the sector constants are parameter-free.

What this changes is the status of the mass ladder. The ladder itself is a established scaling law, and the comparison to measured particle masses is an empirical check. The anchor derivation removes the last suspicion that the sector yardsticks were tuned to make that check pass. The yardsticks are forced by geometry before any measurement is consulted.

THEOREM B_pow_eq_alt · r0_eq_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

THEOREM B_pow_alt · r0_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

THEOREM B_pow_alt · r0_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

THEOREM B_pow_alt · r0_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

THEOREM B_pow_alt · r0_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

THEOREM B_pow_eq_alt · r0_eq_alt · IndisputableMonolith/Masses/AnchorDerivation.lean

What this page does not claim

This answer does not claim that any particle mass itself is established in Lean. This answer does not claim that the anchor derivation fixes the fine-structure constant alpha. This answer does not claim that the physical bridge from recognition to linking is closed.

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