SectorLaw
plain-language theorem explainer
SectorLaw defines a composite structure that pairs sector parameters with a residue function from reals to reals for use in mass anchoring policies. Researchers constructing sector-specific mass predictions in the Recognition framework would reference this when assembling modular rules. The definition is a direct bundling of the two fields with no further axioms or proof steps.
Claim. A sector law consists of sector parameters together with a residue map $f : ℝ → ℝ$.
background
The AnchorPolicy module supplies modular structures for organizing mass predictions under the phi-ladder formula. ResidueLaw is the structure that supplies a single function $f$ from the reals to the reals, intended to encode residual corrections once the main yardstick and rung terms are applied. SectorParams holds the complementary sector data such as rung assignments and charge mappings. This local setting prepares complete policies that can be instantiated per sector before integration with the overall mass ladder.
proof idea
The declaration is a plain structure definition that directly composes the two fields. No lemmas are invoked and no tactics are used; the body consists solely of the field declarations.
why it matters
SectorLaw supplies the interface for sector-specific mass policies inside the AnchorPolicy submodule. It supports constructions such as predict_mass by providing the residue adjustment term. In the Recognition framework it contributes to the mass formula that multiplies a yardstick by phi raised to a rung offset plus gap(Z). No downstream theorems are yet recorded as users of this definition, leaving its role in larger mass theorems open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.