taylor_coefficients_positive

The module gives a direct cubic-lattice proof that J-cost Regge calculus on $\mathbb{Z}^D$ converges to the continuum variational principle, replacing the general Cheeger–Müller–Schrader axiom. The cost is fixed: $J(e^\varepsilon)=\cosh(\varepsilon)-1$, with Taylor structure $\varepsilon^2/2+\varepsilon^4/24+\varepsilon^6/720+\cdots$.

Coefficients of that expansion are exactly $1/(2n)!$ for $n\ge 1$. Positivity of every coefficient means the series has no alternating signs, so truncation errors are one-sided and convergence of the action difference is monotonic once a remainder bound is in hand (Tier 1 of the module strategy).

The local setting is RS gravity on a cubic mesh with known analytic cost, not arbitrary simplicial complexes; the Euler–Lagrange side linearizes via $\sinh'(0)=1$ and the lattice Laplacian continuum limit.

One-line tactic proof. The goal is $0 < 1/(2n)!$ in $\mathbb{R}$ under the hypothesis $n\ge 1$. The positivity tactic closes it: $2n\ge 2$ so $\mathrm{Nat.factorial}(2n)$ is a positive natural, its real cast is positive, and the reciprocal of a positive real is positive. No intermediate lemmas are invoked.

Tier 1 of the cubic Regge program needs the J-cost action to sit above its quadratic truncation with a controlled, sign-stable remainder. Strict positivity of every $1/(2n)!$ is the elementary algebraic fact that makes the cosh expansion free of cancelling terms and therefore monotonically convergent for small strain.

That feeds the module claim that $|S_{J\mathrm{-cost}}-S_{\mathrm{quadratic}}|\le C,\varepsilon_{\max}^4$ and, with EL linearization and lattice-to-continuum Laplacian limits, that the discrete variational principle converges to linearized Einstein gravity at $O(a^2)$. In the broader RS chain this is the gravity-side use of the forced cost $J(x)=\cosh(\log x)-1$ (T5) on the eight-tick cubic lattice (T7–T8).

No downstream consumers are wired yet in the graph; the lemma is infrastructure for the direct CMS replacement.