yardstick
plain-language theorem explainer
Yardstick aliases the sector yardstick A_s from the Anchor module inside the AnchorPolicy namespace. Mass modelers working on the phi-ladder cite this abbreviation when constructing rung-based predictions such as predict_mass. The declaration is a direct noncomputable abbreviation that performs no computation or reduction.
Claim. The yardstick for sector $s$ is the base scale $A_s = 2^{B_ {rm pow}(s)} E_{rm coh} phi^{r_0(s)}$.
background
AnchorPolicy imports the Anchor module to supply policy-level access to mass scales. The yardstick supplies the sector-dependent prefactor that multiplies phi-powers on the ladder to produce masses. Upstream Anchor.yardstick states: Sector yardstick A_s = 2^{B_pow} * E_coh * φ^{r0}. This prefactor enters every mass formula of the form yardstick times phi to a rung offset.
proof idea
This is a one-line alias that directly references the yardstick definition in IndisputableMonolith.Masses.Anchor.
why it matters
The abbreviation is referenced by twenty downstream declarations, including mass_rung and mass_rung_step in SpectralEmergence together with predict_mass and predict_mass_sdgt in AnchorPolicy and MassLaw. It supplies the base scale for the phi-ladder mass formula, consistent with the forcing chain that fixes phi via J-uniqueness and sets the eight-tick octave. It enables concrete mass predictions without addressing any open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.