rawJacobianCoefficient_eval
plain-language theorem explainer
Every raw stencil coefficient J_fg/(2√a*_f) on the six tetrahedron edge slots equals the real cast of an independent literal rational table entry. Gravity analysts cite this when discharging Gate C-A2f radical cancellations without numerics. The proof rewrites via the radical-free normal form, then closes all 36 Fin-6 pairs by kernel rational arithmetic on the flat Freudenthal edge tuple.
Claim. For every pair of edge slots $f,g\in\{0,\ldots,5\}$, the raw Jacobian stencil coefficient $J_{fg}/(2\sqrt{a^*_f})$ (flat-angle Jacobian over twice the square root of the flat squared edge length) equals the real embedding of the independent literal rational table entry at the zero-phase bucket $(f,g,0)$.
background
Gate C-A2f sits in the Regge TT bucket-fiber aggregation lane of Paper C / Pillar 1. The raw coefficient is built in the Bloch interface audit from the kernel-proved flat-angle Jacobian $J$ and the flat squared-edge tuple $a^*=\mathrm{freudenthalTetSqEdges}$. The independent right-hand side is a bare 36-branch match on slot pairs with literal rationals in ${0,1/12,\pm1/8,\pm1/4}$; it is not defined as a fiber sum or alias of the Jacobian side.
The Schlaefli radical bridge packages the identity $\sqrt{a^f},(\partial\theta_f/\partial a_g)=(1/\sqrt{2,c{m3}})\cdot N_f$, and at the flat tuple $\sqrt{2,c_{m3}}=4$, so each entry reduces to a radical-free cofactor expression over $8,a^_f$. Sibling rawJacobianCoefficient_eq_norm_div records that normal form. The present lemma evaluates it on every slot pair against the zero-phase table row.
proof idea
Rewrite the left-hand side by rawJacobianCoefficient_eq_norm_div, exposing the radical-free quotient of Schlaefli poly-summand norms and cofactor polynomials over the flat edge lengths. Then exhaust both Fin 6 indices by fin_cases and close each of the 36 goals with norm_num on the literal table, schlaefliPolySummandNorm, the two cofactor polynomials, and freudenthalTetSqEdges. No native_decide and no floating-point path: pure kernel rational arithmetic.
why it matters
This is the per-slot engine under the Gate C-A2f headline aggregate_raw_weight_eq_rational, which lifts the equality from the zero-phase bucket to every integer phase key. Downstream, table_matches_worstRadical recovers the interface audit's recorded $-1/8$ entry, and coreWeight_eq_raw in the Gate B bridge identifies the core weight table with the actual Jacobian coefficients rather than a transcribed copy. Hinge-aware zero-mode lemmas (w00, w01, ...) use the same rewrite to ground each private coefficient. In the broader RS gravity stack this closes the open radical-bearing fiber left by the Bloch interface audit, so later TT mode analysis can treat stencil weights as exact rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.