quartic_coeff
plain-language theorem explainer
Records the elementary identity 1/24 = 1/4! over the reals, pinning the quartic Taylor coefficient of the J-cost. Anyone citing the cubic-lattice Regge expansion J(exp ε) = ε²/2 + ε⁴/24 + ε⁶/720 + ⋯ needs this equality as a named fact. The proof is a one-line numerical normalization.
Claim. Over the reals, $\frac{1}{24} = \frac{1}{4!}$.
background
The module replaces the general Cheeger–Müller–Schrader convergence axiom by a direct argument for Recognition Science: J-cost interactions on the cubic lattice $\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$. Naming the quartic prefactor as $1/4!$ keeps that bound aligned with the factorial form of the remainder in the cosh expansion.
No upstream lemmas are required; the identity is pure arithmetic on $\mathbb{R}$.
proof idea
One-line tactic proof: norm_num evaluates both sides as concrete rationals and closes the equality. No lemmas are invoked.
why it matters
Feeds the certificate cubic_regge_convergence_cert, which assembles action-quadratic approximation, EL linearization to the lattice Laplacian, and continuum limit into a zero-axiom, zero-sorry package. The module doc lists the fixed Taylor structure $\varepsilon^2/2+\varepsilon^4/24+\varepsilon^6/720+\cdots$ as one of the four reasons the RS cubic case is elementary compared with general CMS. Pinning $1/24=1/4!$ makes that coefficient a first-class named fact rather than an inline numeral, so the quartic remainder bound stays transparent. Framework landmark: this is part of the gravity-side continuum limit that sits downstream of T5 J-uniqueness ($J(x)=\cosh(\log x)-1$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.