ParamProps
plain-language theorem explainer
ParamProps defines the minimal non-negativity conditions on the ILG parameter record components alpha and Clag. Gravity and rotation modules cite it to guarantee non-negativity of time-kernels such as w_t. The declaration is a direct structure definition consisting of two field assertions.
Claim. For a parameter record $P$ with real components $P.alpha$ and $P.Clag$, the predicate ParamProps$(P)$ asserts $0 ≤ P.alpha$ and $0 ≤ P.Clag$.
background
The Params structure is the minimal record containing the fine-structure constant alpha (default value 1) and the lag constant Clag (default value 0), introduced for downstream ILG modules outside the sealed Relativity subtree. Upstream, alpha is defined as the electromagnetic fine-structure constant 1/alphaInv in Constants.Alpha, while Clag equals phi to the power -5 in Constants.ILG. This supplies the base positivity interface that Gravity.ILG extends with additional constraints on A and r0.
proof idea
The declaration is a direct structure definition that introduces the two fields alpha_nonneg and Clag_nonneg asserting non-negativity of the respective parameter components.
why it matters
This definition supplies the base positivity hypothesis used by the extended ParamProps structure in Gravity.ILG and by lemmas such as w_t_nonneg, w_t_ge_one, and w_t_nonneg_with that establish kernel bounds. It supports the rotation velocity existence theorem in Gravity.RotationILG. In the Recognition framework it anchors the ILG parameter interface to the phi-ladder constants alpha and Clag = phi^{-5}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.