ILGAsymptoticEnhancementCert
plain-language theorem explainer
The ILGAsymptoticEnhancementCert structure bundles positivity, strict monotonicity, and unbounded growth of the radial weight w_radial together with the Newtonian domination inequality and the BTFR slope identity. Galaxy rotation-curve analysts working in the Information-Limited Gravity model would cite it to certify that modified velocities exceed Newtonian predictions at every radius and diverge asymptotically. The declaration is a direct packaging of the module's prior enhancement lemmas with no additional reduction steps.
Claim. Let $w(R,r_0,n)$ denote the ILG radial weight. The certificate asserts $C>0$, $w(R,r_0,n)>0$ for all $R,r_0>0$, $w(R,r_0,n)>1$ for $n>0$, $w$ strictly increasing in $R$ for fixed $r_0,n>0$, $w$ unbounded above, $V^2_ {bar} ≤ w(R,r_0,n)·V^2_{bar}$ whenever $V^2_{bar}≥0$, and the BTFR identity $M=V^4_{flat}/(G a_0)$ if and only if $M·(G a_0)=V^4_{flat}$ for positive parameters.
background
The module defines the radial weight as $w(R)=1+C·(R/r_0)^n$ with locked amplitude $C=√(1/φ^3)$ and positive integer $n$ approximating the dynamical exponent α=1−1/φ. This yields the modified velocity squared $V^2(R)=w(R)·V^2_{bar}(R)$ where the Newtonian term is $V^2_{bar}=G M_{enc}/R$. The BTFRSlopeIdentity records the structural claim that baryonic mass satisfies $M=V^4_{flat}/(G a_0)$ equivalently in product form, arising from the deep-ILG limit that reproduces the MOND-like square-root acceleration relation.
proof idea
The declaration is a structure definition whose fields are verbatim the statements of enhancement_pos, enhancement_above_one, enhancement_strict_mono, enhancement_unbounded, the newtonian_dominated inequality, C_lock_pos, and BTFRSlopeIdentity. No tactics are executed; the structure simply collects these upstream lemmas into a single certificate object.
why it matters
The certificate is witnessed by ilgAsymptoticEnhancementCert_holds, which populates each field from the corresponding enhancement theorem. It supplies the structural backbone for Phase D9 of the φ-locked SPARC analysis by guaranteeing that rotation curves cannot decay Keplerianly. The BTFR component encodes the slope β=4 prediction that follows from the locked exponent in the acceleration term. It closes the discrete-n envelope while leaving the continuous real-exponent integration open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.