Bands
plain-language theorem explainer
The bands schema supplies a record type holding three non-negative real couplings for post-Newtonian, lensing, and gravitational-wave observables in the ILG framework. Model builders cite it when mapping lag parameters to observable bands via the toy scaling with absolute value of the product of lag coupling and alpha. The declaration is a bare structure with embedded non-negativity hypotheses and no further computation.
Claim. A record type consisting of real numbers $k_{ppn}$, $k_{lensing}$, $k_{gw}$ together with proofs that each satisfies $k_{ppn}geq 0$, $k_{lensing}geq 0$, and $k_{gw}geq 0$.
background
ILG.Action re-exports geometry and field types for use in the induced linear gravity model. The structure consolidates observable bands as a schema for post-Newtonian, lensing, and gravitational wave sectors. Upstream, C_lag is defined as $phi^{-5}approx 0.09$, the RS-derived lag coupling from the eight-tick resonance. The Map structure provides a minimal scaffold for measurement maps from states to observables.
proof idea
The declaration is a direct structure definition introducing the three coupling fields and their non-negativity hypotheses. No lemmas are applied; it serves as a type constructor for downstream parameter mapping.
why it matters
This definition provides the target type for bandsFromParams, which constructs instances from ILGParams using the absolute value of the product of the lag coupling and alpha. It supports the toy model for observable bands in the Recognition Science framework, linking to the phi-ladder and lag parameters from EightTickResonance. It remains a scaffold without full physical derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.