ParamProps
plain-language theorem explainer
ParamProps packages the six inequalities that keep the ILG parameter record inside the domain where the time kernel stays non-negative and bounded below by one. Rotation-curve and fixed-point existence proofs cite it to discharge the non-negativity hypotheses on alpha, Clag, A, r0 and p. The declaration is a pure structure definition with an empty proof body.
Claim. Let $P$ be a record of real numbers containing components $alpha$, $C_{lag}$, $A$, $r_0$ and $p$. The predicate ParamProps$(P)$ holds precisely when $alpha geq 0$, $C_{lag} geq 0$, $C_{lag} leq 1$, $A geq 0$, $r_0 > 0$ and $p > 0$.
background
Params is the five-field record (alpha, Clag, A, r0, p) that supplies the numerical inputs to the ILG time-weight function w_t. Alpha is the fine-structure constant, Clag is the constant 1/phi^5, A is the fixed active-edge count 1, r0 is a reference length scale, and p is a positive exponent. The structure ParamProps strengthens the minimal positivity conditions already recorded in the sibling ILG.Params module by adding the upper bound Clag leq 1 together with strict positivity on r0 and p.
proof idea
This is a structure definition; it introduces no lemmas and contains no proof body. The six fields are simply listed as the components of the Prop.
why it matters
ParamProps supplies the hypothesis bundle required by the non-negativity lemmas w_t_nonneg, w_t_ge_one and w_t_nonneg_with, and by the existence theorem solution_exists for rotation velocities. It therefore bridges the symbolic constants (alpha and Clag = phi^{-5}) to the concrete bounds needed for the ILG fixed-point equation to admit positive solutions. The structure sits at the interface between the constant definitions in Constants.ILG and the dynamical statements in Gravity.RotationILG.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.