ResidueLaw
plain-language theorem explainer
ResidueLaw packages a single real-to-real function f as the residue component inside mass sector policies. Mass modelers in Recognition Science cite it when building complete anchor policies from rung and gap data on the phi-ladder. The declaration is a bare structure definition with no proof obligations or computational content.
Claim. A residue law is a function $f : ℝ → ℝ$.
background
The AnchorPolicy module supplies structures for mass anchoring that rest on the phi-ladder definitions in sibling declarations such as rung, gap, and predict_mass. The mass formula used throughout is yardstick ⋅ ϕ^(rung − 8 + gap(Z)), with constants drawn from the imported Constants module. ResidueLaw supplies the adjustable function f that captures sector-specific residuals after the main phi-powered term is fixed.
proof idea
The declaration is a structure definition that introduces the type ResidueLaw with one field f of type ℝ → ℝ. No lemmas or tactics are applied.
why it matters
SectorLaw consumes ResidueLaw to pair SectorParams with the residue function, completing the policy object used for mass predictions. The structure therefore supports the framework's application of the T5 J-uniqueness and T6 phi fixed point to particle masses while remaining compatible with the eight-tick octave and D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.