CubeGeometryCert
plain-language theorem explainer
Certificate that three-dimensional cube combinatorics forces the Recognition Science integers 8, 12, 6, 11, 102, and 103. Anyone tracing the geometric seed of α, the eight-tick period, or seam curvature numerics cites it. Verification is a finite conjunction of pure arithmetic identities at D = 3, discharged by named evaluation lemmas and rfl.
Claim. A cube-geometry certificate is verified precisely when the spatial dimension equals $3$, the $3$-cube has $2^3 = 8$ vertices, $3 \cdot 2^{2} = 12$ edges and $2 \cdot 3 = 6$ faces, the passive field-edge count is $12 - 1 = 11$, the geometric seed factor equals $11$, the seam denominator and numerator are $102$ and $103$, the provenance identities $11 = 12 - 1$, $102 = 6 \cdot 17$, $103 = 6 \cdot 17 + 1$ hold, there are $17$ wallpaper groups, and the Euler closure equals $1$. Every such certificate satisfies the predicate.
background
The module packages the cube-geometry facts that underwrite the Recognition Science ledger. Spatial dimension is fixed at the constant $D := 3$ (forced upstream by linking, T8/T9). Hypercube counts are the standard combinatorial definitions: vertices $2^D$, edges $D \cdot 2^{D-1}$, faces $2D$.
Passive field edges subtract the single active edge traversed in one atomic tick $\tau_0$, leaving $11$ dressing edges. The geometric seed factor is that same $11$. Seam denominator and numerator fold faces against the crystallographic constant of $17$ wallpaper groups, with Euler closure $+1$ on the numerator: $6 \cdot 17 = 102$ and $103 = 102 + 1$.
Module stance is non-circular arithmetic: $D = 3$ is the only structural input; everything else is combinatorics, with no measurement constants or axioms in the certificate itself.
proof idea
The structure is a unit carrier. The predicate verified is the thirteen-way conjunction listed in the signature. The top-level theorem builds that conjunction by refine with thirteen goals.
Dimension is rfl on $D = 3$. Vertex, edge, face, passive-edge, seed, denominator, and numerator goals are closed by the evaluation lemmas vertices_at_D3, edges_at_D3, faces_at_D3, passive_edges_at_D3, geometric_seed_factor_eq_11, seam_denominator_at_D3, and seam_numerator_at_D3. Provenance goals use eleven_is_forced, one_oh_three_is_forced, and one_oh_two_is_forced. Wallpaper groups and Euler closure are definitional rfl.
why it matters
This certificate is the geometric origin story for the integers that appear throughout Recognition Science. The eight vertices are the eight-tick octave (T7). The twelve edges and single active edge give the $1:11$ active-to-passive ratio that seeds $\alpha$ via the geometric factor $4\pi \cdot 11$. Faces times wallpaper groups produce the seam pair $(102, 103)$ used in curvature bookkeeping.
Sibling results in the same module (magic_numbers_from_D3, eight_tick_is_cube_vertices, eleven_enters_geometric_seed) unpack the same arithmetic for narrower citations. The module imports AlphaDerivation, so the certificate sits directly under the fine-structure derivation chain rather than as an isolated combinatorics note. No downstream dependents are recorded yet; the value is as a single verified bundle a referee can discharge before accepting the magic-number inputs to $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.