magic_numbers_from_D3
plain-language theorem explainer
At spatial dimension three, the hypercube combinatorics fix the Recognition ledger integers: eight vertices, twelve edges, six faces, eleven passive field edges, and the seam pair 102 and 103. Anyone citing the geometric origin of the eight-tick period, the 1:11 active/passive split, or the geometric seed for alpha needs this certificate. The proof is pure closed arithmetic: six goals discharged by native decision on the combinatorial definitions.
Claim. For spatial dimension $D=3$, the $D$-cube has $2^D=8$ vertices, $D\cdot 2^{D-1}=12$ edges, and $2D=6$ faces; the passive field edge count is $11$, the seam denominator is $102$, and the seam numerator is $103$.
background
The module certifies the cube geometry that underpins Recognition Science's ledger at the forced spatial dimension $D=3$ (T8/T9). Hypercube counts are defined combinatorially: vertices $2^D$, edges $D\cdot 2^{D-1}$, faces $2D$. At $D=3$ these evaluate to 8, 12, and 6.
Passive field edges are the non-active edges in one atomic tick: one edge is traversed by the recognition event, the remaining eleven dress the interaction. The seam pair packages face counting with the seventeen wallpaper groups: denominator $6\times 17=102$, numerator $6\times 17+1=103$ (Euler closure). The module stresses non-circularity: $D=3$ is the sole input; everything else is arithmetic.
Upstream, cube_vertices, cube_edges, and cube_faces are the plain power-of-two formulas, and the constant $D$ is fixed at 3. The eight-tick octave in the constants layer is the same integer eight that appears here as the vertex count.
proof idea
Term-mode proof: refine splits the six-way conjunction into six goals, then each goal is closed by native_decide. No lemmas are invoked beyond the definitional unfolding of the combinatorial counts at the concrete natural number 3. The entire certificate is kernel-checked arithmetic with no axioms or measurement constants.
why it matters
This is the structural origin of the Recognition "magic numbers." Eight is the eight-tick octave (T7) identified with cube vertices; twelve is the full edge cycle; six is the face count that feeds wallpaper-group bookkeeping; eleven is the passive dressing that enters the geometric seed $4\pi\cdot 11$ and the 1:11 active/passive split underlying $\alpha$. The seam integers 102 and 103 close the curvature numerator with Euler characteristic.
The module frames the physical picture: during one tick $\tau_0$, one edge is active and eleven are passive field edges. Sibling certificates in the same file (eight_tick_is_cube_vertices, eleven_enters_geometric_seed) specialize pieces of this conjunction. No downstream consumers are recorded yet; the declaration is a leaf certificate meant to be cited wherever the ledger integers are taken as forced rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.