sextic_coeff
plain-language theorem explainer
Identifies the sextic Taylor coefficient of the J-cost as exactly 1/6! on the reals: 1/720 = 1/720. Anyone tracking the fixed expansion J(exp ε) = ε²/2 + ε⁴/24 + ε⁶/720 + ⋯ in cubic Regge convergence cites this. The proof is a one-line numerical normalization of factorial arithmetic.
Claim. As real numbers, $\frac{1}{720} = \frac{1}{6!}$.
background
The module gives a direct cubic-lattice Regge convergence argument for Recognition Science, replacing the general Cheeger–Müller–Schrader axiom by an RS-specific case: J-cost interactions on $\mathbb{Z}^D$. The cost is known explicitly, $J(e^{\varepsilon})=\cosh\varepsilon-1$, so its Taylor series is fixed: $\varepsilon^2/2+\varepsilon^4/24+\varepsilon^6/720+\cdots$.
Tier 1 of the strategy bounds the gap between the full J-cost action and its quadratic truncation by a multiple of $\varepsilon_{\max}^4$, using that higher even powers remain controlled. The coefficient of $\varepsilon^6$ is the classical $1/6!$ term in the expansion of $\cosh$. Recording $1/720=1/6!$ pins that constant in Lean without floating-point ambiguity.
Sibling material in the same file treats positivity of all $1/(2n)!$ coefficients and the linearized Euler–Lagrange equation (sinh linearizes to the lattice Laplacian). This lemma is only the arithmetic identity for the sixth-order term.
proof idea
One-line tactic proof: norm_num evaluates Nat.factorial 6 to 720 and closes the real equality $1/720=1/720$. No lemmas from the gravity stack are required; the depends-on edges are incidental name collisions, not proof ingredients.
why it matters
The module’s Taylor structure is part of why a direct proof suffices for RS: cubic lattice, known J, fixed series, trivial linearization of sinh. Naming the sextic coefficient as $1/6!$ keeps that series fully explicit in the formal development.
Downstream, cubic_regge_convergence_cert packages the proved certificate (action quadratic approximation, symmetry, vacuum, EL equals minus Laplacian, flat solutions) with zero axioms and zero sorry. The sextic identity supports the action-side bookkeeping that feeds that certificate’s quadratic-approximation tier, even though the cert fields do not quote this lemma by name.
In the broader RS picture this sits under gravity continuum recovery on $\mathbb{Z}^D$, not under the T0–T8 forcing chain itself. It does not touch open scaffolding; it is a closed arithmetic fact inside an already-proved module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.