worstRadical_rawJacobianCoefficient_closedForm
plain-language theorem explainer
The raw Jacobian coefficient at the genuine radical-bearing edge pair (indices 1 and 2) equals exactly $-1/8$. Interface auditors and the rational bucket aggregation cite this closed form when matching the stencil table to the radical row. The proof unfolds the coefficient, substitutes the known flat-angle Jacobian value, and clears the remaining square-root denominator by field arithmetic.
Claim. The raw Jacobian coefficient for Freudenthal edge indices $1$ and $2$ equals $-1/8$. Explicitly, if the coefficient is the flat-angle Jacobian entry divided by twice the square root of the corresponding squared edge length, then that normalized value is $-1/8$.
background
This module is the panel-locked C11 interface audit for the Regge transverse-traceless (TT) Bloch analysis. It deliberately keeps the raw cell stencil as a literal triple sum over tetrahedra and ordered slot pairs, rather than wiring it definitionally to the objects under audit. The reduced second variation equals that stencil (with the sign of the live A2 theorem: negative Schlaefli-reduced contraction).
The raw Jacobian coefficient is the flat-angle Jacobian entry divided by $2\sqrt{a^}$, where $a^$ comes from the local squared-edge tuple of a Freudenthal tetrahedron in the unit cube (three unit steps, two face diagonals, one body diagonal). For edge index $1$ that squared length is $2$. The flat-angle Jacobian itself is the algebraic Schlaefli summand over the flat hinge area, used by the directional kill in the pathwise Regge 4D analysis.
The "worst radical" row is the genuine radical-bearing numerator entry at slot pair $(1,2)$; the audit keeps that radical visible before proving the normalized coefficient collapses to a pure rational.
proof idea
Unfold the raw coefficient to the quotient
$\mathrm{flatAngleJacobian}(1,2),/,(2\sqrt{\mathrm{freudenthalTetSqEdges}(1)})$.
Rewrite the numerator by the already-proved value of the worst-radical flat-angle Jacobian. Evaluate the squared-edge lookup (freudenthalTetSqEdges 1 = 2) by norm_num, record $\sqrt{2}\neq 0$ by positivity, then field_simp clears the denominator and a final norm_num yields $-1/8$.
why it matters
Closes the exact radical-row coefficient that the bucket aggregation must reproduce. Downstream, table_matches_worstRadical rewrites the rational stencil weight of the worst-radical bucket through the raw-to-rational aggregation gate and lands on this identity, confirming the table matches the interface audit's $-1/8$ (kernel-recorded via the $-\sqrt{2}/4$ Jacobian entry).
In the broader Regge TT continuum program this is a narrow Gate-A2 building block: the stencil-only constant block does not yet vanish, and full bucket aggregation plus hinge-aware zero-mode cancellation remain open. No ContinuumLimit or spike certificate is claimed here; the result only pins one audited radical entry so later cosine two-jet work can trust the rational table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.