bandsFromParams
plain-language theorem explainer
bandsFromParams supplies a concrete Bands instance for ILG models by equating all three coupling constants to the absolute value of the product of the lag parameter and the fine-structure constant. Modelers initializing observable bands from global ILG parameters would invoke this definition. The implementation directly constructs the record and discharges the non-negativity conditions via the built-in property of absolute value.
Claim. For an ILG parameter bundle $p = (α, C_{lag})$, the bands are given by $κ_{ppn} = κ_{lensing} = κ_{gw} = |C_{lag} · α|$, where each $κ$ satisfies $κ ≥ 0$.
background
ILGParams is the structure holding the fine-structure constant $α$ and lag constant $C_{lag}$ as real numbers. Bands is the scaffold structure collecting three coupling constants $κ_{ppn}$, $κ_{lensing}$, $κ_{gw}$ together with explicit proofs that each is nonnegative. The module re-exports geometry and field types to support ILG action constructions. Upstream, alpha is defined as the reciprocal of its inverse in the Constants.Alpha module.
proof idea
The definition computes $κ$ as the absolute value of the product of the two parameters from ILGParams and assigns this value to all three fields of Bands. Non-negativity for each field is witnessed by applying abs_nonneg to the computed $κ$.
why it matters
This definition provides the parameter-to-bands mapping required for the ILG action. It links the global constants module to the relativity action by supplying the toy proportionality to $|C_{lag} · α|$. No downstream uses are recorded; it supports the scaffold for Einstein equations moved to the Variation submodule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.