row0Smoke_table_value
plain-language theorem explainer
The independent rational stencil table assigns weight 1/4 to the row-0 smoke-test bucket (slots 0 and 5, zero phase), and that value survives casting from rationals to reals. Gravity auditors of the Regge TT Bloch interface cite this as the first non-tautological table check. The proof is a one-line numerical normalization of the match clauses for the table and the smoke bucket.
Claim. Casting the rational stencil weight of the row-0 smoke-test bucket (left slot index $0$, right slot index $5$, vanishing phase) from $\mathbb{Q}$ to $\mathbb{R}$ yields exactly $1/4$.
background
This module is the panel-locked C11 interface audit for Regge transverse-traceless (TT) second variation on a Freudenthal triangulation of the unit cube. Attempt 1 was rejected for wiring the raw stencil definitionally to the objects under audit; attempt 2 keeps the first gate narrow and non-tautological.
Buckets index ordered slot pairs together with a phase vector. The rational stencil weight is an independent literal match table (not a fiber sum): the pair of slots $(0,5)$ and its swap each carry weight $1/4$, and every other pair is zero in this quarantine table. The row-0 smoke bucket is the radical-trivial case $J_{05}/(2\sqrt{a^*_0})$ with squared edge length $1$ on the first Freudenthal edge class.
Upstream, the Freudenthal squared-edge tuple supplies the local edge lengths (unit steps, face diagonals, body diagonal). The full 36-entry rational table lives in the sibling aggregation module; only the smoke row is certified here.
proof idea
One-line term proof by norm_num after unfolding the two local definitions. The smoke bucket matches left index $0$ and right index $5$, so the rational table clause returns $1/4$; casting to reals and numerical normalization close the equality. No external lemmas are required beyond the definitional match.
why it matters
Closes the isolated smoke-test agreement demanded by the C11 audit surface: the independent rational table agrees with the row-0 bucket after real casting, without tautological wiring. The module doc keeps Gate A2-full (aggregate raw weight equals the full rational table over all buckets) OPEN, Gate A3 (hinge-aware zero-mode) OPEN, and Gate B (spike convention bridge) OPEN. Downstream ContinuumLimit work is deliberately not imported; the same-day sympy diagnostic already showed the stencil-only constant block does not vanish, so the cosine two-jet route remains the intended path once the hinge/diagonal block is connected. This lemma is a quarantine checkpoint, not a substitute for the full aggregation gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.