sixJ_eq_2D
plain-language theorem explainer
The equality establishes that the 6j-symbol dimension equals twice the spatial dimension count. Researchers assembling spin-foam amplitudes in quantum gravity cite this when confirming the combinatorial structure of the recognition lattice triangulation. The proof is a direct numerical verification performed by the decide tactic on the arithmetic identity.
Claim. The dimension of the 6j-symbol satisfies $6jDimension = 2D$ at $D=3$, or equivalently $6jDimension = 2*3$.
background
In the SpinFoamFromRS module the spin foam is the Freudenthal triangulation of the recognition lattice. The fundamental amplitude is built from the 6j-symbol whose dimension is introduced by the upstream definition sixJDimension : ℕ := 6, carrying the explicit gloss “6j-symbol dimension = 6 = 2D = cube faces.” MODULE_DOC states that five canonical models correspond to configDim D = 5 and that Lean records 6 = |faces(Q₃)| = 2D at D = 3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the arithmetic equality between the constant definition sixJDimension and the product 2 * 3.
why it matters
The result is consumed by spinFoamCert, which packages the model parameters including sixJ_faces and sixJ_2D. It supplies the concrete link 6 = 2D that realizes T8 (D = 3 spatial dimensions) inside the spin-foam construction and thereby closes the combinatorial count of cube faces required by the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.