components_at_D3
plain-language theorem explainer
The theorem verifies that passive field edges total 11 and cube faces total 6 when the dimension parameter equals 3. Researchers deriving the uniqueness of three-dimensional space from the Recognition Science wallpaper count would cite this arithmetic check. The proof is a one-line term-mode wrapper that splits the conjunction and applies native_decide to evaluate the definitions.
Claim. $passive_field_edges(3) = 11$ and $cube_faces(3) = 6$, where $cube_faces(D) := 2D$ and $passive_field_edges(D) := cube_edges(D) - active_edges_per_tick$.
background
The W_endo forcing module defines the endogenous wallpaper count as $W_endo(D) := passive_field_edges(D) + cube_faces(D)$. Passive field edges count the edges that dress the interaction after subtracting the active component per tick, while cube_faces counts the faces of the D-hypercube. The module states that this sum equals 17 if and only if D equals 3, which is the paper's Tr7 argument. Upstream definitions supply $cube_faces(d) := 2d$ and the subtraction form for passive_field_edges.
proof idea
The term proof applies constructor to split the conjunction into two separate goals. Each goal is discharged by native_decide, which reduces the definitions of passive_field_edges and cube_faces at the concrete argument 3 to the integers 11 and 6.
why it matters
This supplies the concrete numerical values required for the Tr7 step that forces D equals 3 in the Recognition Science framework. It directly supports the eight-tick octave and spatial dimension result (T8) by confirming W_endo reaches exactly 17 only at D=3. The verification closes the arithmetic case for the three-dimensional wallpaper decomposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.