ParamsKernelVerified
plain-language theorem explainer
A predicate on ILG parameters holds exactly when the components satisfy non-negativity of alpha, Clag and A together with Clag at most one and r0 positive. Researchers in the gravity and relativity modules cite it to validate inputs prior to further derivations. The definition is realized as a direct abbreviation of the corresponding property structure.
Claim. Let $P$ be a parameter record with real components $alpha$, $C_{lag}$, $A$, $r_0$, $p$. Then the predicate holds if and only if $alpha geq 0$, $C_{lag} geq 0$, $C_{lag} leq 1$, $A geq 0$, and $r_0 > 0$.
background
The parameter record collects five real numbers: alpha scaling the fine structure, Clag a lag factor, A an amplitude, r0 a reference length, and p an exponent. The property structure requires alpha, Clag, and A to be non-negative, Clag to lie in the unit interval, and r0 to be strictly positive. This predicate is drawn from the Gravity.ILG submodule to ensure uniformity, while the local ILG.Params supplies a reduced record with defaults alpha equal to one and Clag equal to zero.
proof idea
The declaration is a one-line abbreviation that sets the predicate equal to the property structure applied to the input parameters.
why it matters
This definition acts as the verification gate for the parameter kernel and is invoked by the lemma establishing that any set satisfying the property structure satisfies the kernel predicate. It ensures parameter consistency in the ILG component of the Recognition Science framework, supporting derivations that rely on the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.