Q3_faces
plain-language theorem explainer
The declaration fixes the face count of the three-dimensional cube at six under the hypercube formula used in Recognition Science. Derivations of the recognition wavelength from ledger curvature costs cite this count when distributing a curvature packet over the geometry to obtain the 1/π factor. The proof is a direct reflexivity reduction to the general definition cube_faces D := 2D at D=3.
Claim. The three-dimensional cube has exactly six faces: $2D=6$ when $D=3$.
background
The PlanckScaleMatching module derives λ_rec ≈ 0.564 ℓ_P from the equality J_bit = J_curv(λ) at the ledger-curvature extremum. Here J_bit = J(φ) = cosh(ln φ) - 1 arises from the unique cost functional, while J_curv(λ) = 2λ² follows from distributing a ±4 curvature packet over the faces of the Q3 geometry in RS-native units. The general definition states that the number of faces of the D-hypercube equals 2D; the present result specializes this at the spatial dimension fixed by the eight-tick octave.
proof idea
This is a one-line wrapper that applies reflexivity to the definition cube_faces D := 2 * D evaluated at D=3.
why it matters
The identity supplies the face count required by AlphaFrameworkCert and by the LambdaRecDerivation of λ_rec. It closes the geometric step that converts the extremum condition into λ_rec = ℓ_P / √π after face-averaging restores SI dimensions. Downstream it is invoked in higher-order alpha corrections, delta_1_neg, and the numerological summary of spectral emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.