paramsKernel_verified_any
plain-language theorem explainer
The lemma shows that any ILG parameter record meeting the basic non-negativity conditions on alpha and Clag automatically satisfies the kernel verification predicate. Researchers handling parameter consistency in ILG modules would cite it to simplify verified-parameter expressions. The proof is a direct term application of the hypothesis, since the verification predicate is defined to coincide exactly with the positivity property.
Claim. Let $P$ be a parameter record with components alpha and Clag. If $0 ≤ P.alpha$ and $0 ≤ P.Clag$, then the kernel verification predicate holds for $P$.
background
The ILG.Params module defines a minimal parameter record consisting of alpha (default 1) and Clag (default 0). ParamProps encodes the basic positivity conditions: alpha and Clag are non-negative. The kernel verification predicate is defined exactly as ParamProps P, providing a well-formedness check for the parameter kernel in the local ILG setting. This is distinct from the extended ParamProps in Gravity.ILG, which adds non-negativity of A, positivity of r0, and Clag ≤ 1.
proof idea
The proof is a one-line term wrapper that applies the hypothesis h directly. Because ParamsKernelVerified is defined to be identical to ParamProps, the implication holds by definition.
why it matters
This lemma supplies a simp rule that equates the basic positivity property with kernel verification inside ILG parameter handling. It allows downstream ILG proofs to treat verified parameters as interchangeable with those satisfying non-negativity without extra steps. In the Recognition framework it closes a minor interface between the minimal Params record and the kernel predicate, supporting consistent use across ILG submodules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.