Mass
plain-language theorem explainer
Mass supplies the real-number carrier for mass quantities inside the RS-native unit system. Workers deriving phi-ladder mass values or packaging PhysicalCertificate instances cite this abbreviation. The declaration is a direct type alias with no further reduction or proof obligations.
Claim. In the Recognition Science native units, mass is represented by an element of the real numbers $M : ℝ$.
background
The RS-Native Measurement System module introduces tick (τ₀) as the discrete time quantum and voxel (ℓ₀) as the spatial step with c = 1. Derived quanta are coh = φ^{-5} for energy and act = ħ for action. All quantities, including mass, sit on the φ-ladder where scaling proceeds by integer powers of φ. The module states that dimensionless ratios are fixed by φ alone and that SI conversion remains optional via ExternalCalibration.
proof idea
Direct abbreviation: Mass is introduced as the type ℝ with no lemmas or tactics applied.
why it matters
The abbreviation is referenced by PhysicalCertificate to hold explicit derived mass values, by information_balance_gives_phi to equate mass-event information to light-event information, and by ml_geometric_bounds to bound the mass-to-light ratio between 1 and 2. It supplies the M exponent in the Dimension structure and supports the mass formula yardstick · φ^(rung - 8 + gap(Z)) on the φ-ladder. The definition closes the base for all downstream mass-dependent certificates in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.