ParamProps
plain-language theorem explainer
ParamProps encodes the minimal non-negativity conditions on the fine-structure constant and the ILG lag parameter inside the relativity subtree. Rotation-curve and time-kernel lemmas cite it to guarantee that weights remain non-negative. The declaration is realized as a two-field structure directly on the parameter record.
Claim. For a parameter record $P$ with components $P.alpha$ and $P.Clag$, the predicate ParamProps$(P)$ asserts $P.alpha >= 0$ and $P.Clag >= 0$.
background
Params is the minimal record holding the fine-structure constant alpha (default value 1) and the lag parameter Clag (default value 0). Upstream, alpha is defined as the reciprocal of the fine-structure constant inverse while Clag equals phi to the power of minus five. The present module supplies a stripped-down version of the same structure for relativity modules, omitting the extra fields A and r0 that appear in the gravity counterpart.
proof idea
Direct structure definition that introduces exactly the two non-negativity fields alpha_nonneg and Clag_nonneg.
why it matters
This supplies the base positivity interface consumed by the extended ParamProps in Gravity.ILG and by the lemmas w_t_nonneg, w_t_ge_one and solution_exists. It anchors the constants alpha and Clag = phi^{-5} before they enter downstream calculations of time kernels and rotation velocities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.