ILGCoercivityCert
plain-language theorem explainer
Empty certificate type whose verification predicate packages five ILG coercivity facts: c_min equals 49/162, the three ILG constants are positive, the kernel is always at least 1, the RS kernel exponent equals alphaLock, and c_min matches the CPM prediction. Gravity and RS auditors cite it as the single gate for ILG coercivity. The companion theorem discharges the predicate by refine plus named arithmetic and kernel lemmas.
Claim. An ILG coercivity certificate is a unit structure. It is verified precisely when: the ILG coercivity constant equals $49/162$; the net, projection, and energy constants are strictly positive; for every kernel parameter set and every real $k,a$, the ILG kernel is at least $1$; for every positive tick duration $\tau_0$, the RS kernel exponent equals the locked value $\alpha_{\mathrm{lock}}=(1-1/\varphi)/2$; and $49/162$ equals that same $c_{\min}$.
background
Infra-Luminous Gravity (ILG) is the RS modification of gravity whose kernel takes the form $w(k,a)=1+C\cdot(a/(k\tau_0))^\alpha$. The module certifies coercivity facts for eight-tick-aligned ILG: energy-gap control of defect mass, enhancement (never suppression) at large scales, and a fixed strength $c_{\min}=49/162$.
Upstream constants pin the numerics. The locked fine-structure value is $\alpha_{\mathrm{lock}}=(1-1/\varphi)/2$, and the fundamental tick $\tau_0$ is the RS-native duration of one tick. Kernel parameters built from a positive $\tau_0$ are required to carry exactly this locked exponent. Sibling facts supply positivity of $(K_{\mathrm{net}},C_{\mathrm{proj}},C_{\mathrm{eng}})$, the identity $c_{\min}=49/162$, kernel lower bound $\ge 1$, and the CPM match for $c_{\min}$.
The certificate itself carries no data; verification is a pure Prop conjunction over those five claims.
proof idea
The structure is an empty record (only Repr). The interesting content is the simp predicate verified (five-way conjunction) and the theorem verified_any.
verified_any opens with refine into seven goals. The first is discharged by ilg_cmin_value ($c_{\min}=49/162$). The next three are the three conjuncts of ilgConstants_pos (positivity of $K_{\mathrm{net}}$, $C_{\mathrm{proj}}$, $C_{\mathrm{eng}}$). The fifth introduces kernel parameters and applies kernel_ge_one. The sixth is definitional equality (rfl) that the RS kernel exponent is alphaLock. The last is ilg_c_matches_cpm, the CPM match for $49/162$. No axioms or measurement constants enter.
why it matters
ILG is the RS route to falsifiable gravitational predictions without dark-matter particles: the kernel factor $w$ forces specific large-scale deviations from GR, with strength fixed by $c_{\min}=49/162$. The module doc stresses non-circularity (arithmetic, kernel definition only).
The certificate sits in the Verification domain as the single Prop gate for those five claims. Downstream usage is currently empty in the graph, but sibling names (ilg_is_falsifiable, ilg_enhancement_bounded) show the intended consumers: falsifiability summaries and enhancement bounds. Framework landmarks in play are the eight-tick octave (alignment of the coercivity constant) and $\varphi$ through $\alpha_{\mathrm{lock}}=(1-1/\varphi)/2$. The certificate does not itself close an open physics question; it packages already-proved arithmetic so auditors can cite one verified object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.