sixJDimension
plain-language theorem explainer
The definition fixes the dimension of the 6j-symbol at the natural number 6. Quantum gravity researchers working with Ponzano-Regge or EPRL spin foams would cite it to anchor the path-integral amplitude to the geometry of a 3-cube. The assignment is a direct constant definition that matches the count of cube faces and the relation 2D at D=3.
Claim. The dimension of the 6j-symbol is defined to be the natural number 6, equal to twice the spatial dimension and to the number of faces of a cube.
background
Spin foam models supply a path-integral formulation of quantum gravity. In Recognition Science the spin foam is realized as the Freudenthal triangulation of the recognition lattice, and five canonical models (PR, EPRL, FK, BO, EL) correspond to configDim D = 5. The fundamental amplitude involves the 6j-symbol whose dimension is fixed at 6 because it equals the number of faces of the 3-cube, equivalently 2D when D=3.
proof idea
Direct definition that assigns the constant 6 to sixJDimension. No lemmas or tactics are invoked; the value is set by the geometric identification with cube faces.
why it matters
The definition supplies the concrete value required by the SpinFoamCert structure, which records five_models = 5 together with the two equalities sixJDimension = 6 and sixJDimension = 2 * 3. It implements the module statement that the 6j-symbol dimension equals |faces(Q₃)| = 2D at D=3, consistent with the T8 step that forces three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.