pith. machine review for the scientific record.
sign in
module module high

IndisputableMonolith.RecogSpec.MassLawFromLedger

show as:
view Lean formalization →

The module derives particle mass ratios from rung differences inside the tiered ledger structure instead of writing explicit powers of phi. It supplies functions that extract those ratios and package them into typed observable payloads. Researchers modeling the discrete mass spectrum in Recognition Science cite the module to keep derivations ledger-native. The module organizes its content as definitions that bridge RSLedger tiers to mass-ratio records while importing the base time quantum from Constants.

claimMass ratios between particles are obtained as $m_i/m_j = phi^{r_i - r_j}$, where the rung indices $r_i$ and $r_j$ are read from the tier structure of the recognition ledger rather than supplied as literal phi formulas.

background

Recognition Science places particle masses on discrete rungs of the phi-ladder. The RSLedger module supplies the rich ledger structure that encodes these tiers and the torsion that generates them. ObservablePayloads provides the strongly typed records that carry the resulting dimensionless mass ratios and mixing angles, replacing earlier raw lists. Constants supplies the fundamental RS time quantum tau_0 equal to one tick.

proof idea

This is a definition module, no proofs. It introduces helper functions that read rung differences from ledger tiers and compute the corresponding phi-powers for the mass ratios.

why it matters in Recognition Science

The module supplies the mass-ratio component required for the full mass-law derivation in the Recognition framework. It grounds ratios in the phi-tier ledger structure, supporting the mass formula that multiplies a yardstick by phi raised to a rung offset. It feeds spectrum calculations consistent with the eight-tick octave and the three spatial dimensions fixed by the forcing chain.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (4)