worstRadicalBucket
plain-language theorem explainer
Names the canonical radical-row bucket (left slot 1, right slot 2, zero phase) used to stress-test the Regge TT Bloch interface audit. Citation target for anyone checking that raw Jacobian coefficients can be irrational while bucket-fiber aggregates stay rational. The body is a literal structure constructor with decidable Fin witnesses.
Claim. Define the worst-radical bucket representative as the triple $(f,g,u)=(1,2,0)$ in the six-slot Freudenthal indexing: left face index $1$, right face index $2$, and vanishing Bloch phase vector. This is the generator-selected radical row where the angle-Jacobian entry is nonzero and $\mathrm{freudenthalTetSqEdges}(1)=2$.
background
The module is the panel-locked C11 Regge TT Bloch interface audit (attempt 2). It deliberately keeps the first gate non-tautological: rawCellStencil is a literal triple sum over tetrahedra and ordered slot pairs, not definitionally wired to the rational table it audits. Full rational bucket aggregation and hinge-aware zero-mode cancellation remain open.
A Bucket is a representative triple (left, right, phase) with face indices in Fin 6 and a phase vector; the external convention only identifies $(f,g,u)$ with $(g,f,-u)$, and this attempt does not yet quotient fibers. The single-entry radical coefficient is rawJacobianCoefficient f g = flatAngleJacobian f g / (2 sqrt(freudenthalTetSqEdges f)), which is not a full fiber aggregate.
The sympy diagnostic selected $(f,g)=(1,2)$ as the genuine radical row: the Jacobian entry is $-\sqrt{2}/4$, and after the current normalization the same $\sqrt{2}$ cancels in the denominator, exposing an irrational raw coefficient at the row-Jacobian layer.
proof idea
Pure definitional constructor. Build a Bucket with left = ⟨1, _⟩, right = ⟨2, _⟩ (both Fin bounds discharged by decide), and phase the zero PhaseVector (fun _ => 0). No lemmas, no tactics beyond the two decidability proofs inside the Fin constructors.
why it matters
Supplies the concrete radical-row witness that the aggregation layer must reproduce. Downstream, table_matches_worstRadical proves that the rational stencil weight of this bucket equals $-1/8$ in $\mathbb{R}$, by rewriting through aggregate_raw_weight_eq_rational and the closed form of the raw Jacobian coefficient. That theorem records the kernel fact that the $-\sqrt{2}/4$ Jacobian entry normalizes to the rational $-1/8$.
In the audit status block this sits under Gate A2-full (aggregate_raw_weight_eq_rational over all buckets), which remains OPEN: individual raw coefficients are irrational here, while the panel's rationality claim lives only at bucket-fiber aggregation. The definition therefore pins the hardest single entry the ContinuumLimit cosine two-jet route must eventually match, without claiming the full aggregate or the hinge-aware zero-mode (Gate A3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.