vacuumKineticA_pos
plain-language theorem explainer
For every real $a$, the vacuum kinetic coefficient $A(a)=(1+a^2)^{-1}$ is strictly positive. Gravity workers on the kinetic-normalized HKT rigidity path (SevenGaps gap5) cite it to keep the vacuum kinetic weight invertible and sign-definite. The proof is a one-line wrapper: invert positivity of $1+a^2$ via `nlinarith` on $a^2\ge 0$.
Claim. For every real number $a$, $0 < (1+a^{2})^{-1}$.
background
In the kinetic-normalized HKT vacuum sector the coefficient $A$ is the reciprocal weight
$$A(a);:=;(1+a^{2})^{-1}.$$
It appears in the local kinetic profile and Hamiltonian density that implement KineticNormalizedCanonicalMom for the gap5 terminal. The module is the Wave C4/C5 gap5 stack: mod-vacuum kill plus kinetic-normalized rigidity, binding the Codex cross-family verdict and the C5 acceptance adjudication. FTC recovery is theorem-derived rather than an assumed class field.
Positivity of $A$ is the elementary analytic fact that keeps the vacuum kinetic weight strictly positive for every real amplitude $a$, so later non-vanishing and rigidity lemmas can treat $A$ as an invertible scalar field.
proof idea
One-line wrapper around Mathlib's inv_pos.mpr. The goal reduces to $0<1+a^{2}$. A short nlinarith step discharges that from mul_self_nonneg a (i.e. $a^{2}\ge 0$), hence $1+a^{2}\ge 1>0$. No sector-specific lemmas are needed.
why it matters
Immediate parent is vacuumKineticA_ne_zero, which rewrites positivity to $A(a)\ne 0$ and keeps the vacuum kinetic weight invertible in the normalized Hamiltonian density. That non-vanishing sits inside the kinetic-normalized rigidity half of gap5: after the mod-vacuum kill, the remaining ledger half needs a strictly positive, design-matched kinetic coefficient so that ftc_recovery_of_normalized and the constraint-recovery flip can close under Gap5ConstraintCloseStatus. The result is pure real analysis, but it is the sign gate for the vacuum kinetic sector of the SevenGaps gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.