Pith. sign in
theorem

endogenous_wallpaper_bridge_complete

proved
show as:
module
IndisputableMonolith.Verification.WallpaperEndogenousBridge
domain
Verification
line
102 · github
papers citing
none yet

plain-language theorem explainer

The cube-derived endogenous wallpaper count equals 17, matches the classical wallpaper-group constant, and that constant is characterized exactly by passive edges plus faces at D=3. Cite this when closing the counting-layer bridge from hypercube combinatorics to W=17. Proof is a three-way conjunction from two equality lemmas and one universal biconditional.

Claim. The endogenous cube-derived wallpaper count equals $17$, equals the classical number of wallpaper groups, and for every natural number $w$, $w$ equals the wallpaper-group count if and only if $w$ equals the sum of passive field edges and cube faces evaluated at spatial dimension $D=3$.

background

Recognition Science forces spatial dimension $D=3$. The $D$-hypercube then has $F=2D$ faces (hence 6 at $D=3$). Passive field edges are total cube edges minus the single active edge per tick; at $D=3$ that count is 11. These are the edges that dress the interaction rather than carry the active hop.

This module defines an endogenous candidate $W_{\mathrm{endogenous}}(D):=E_{\mathrm{passive}}(D)+F(D)$. At $D=3$ one obtains the counting identity $11+6=17$. Classically, the number of distinct 2D wallpaper groups is the Fedorov constant 17 (1891), imported as a named constant rather than re-derived here.

The named cube-derived constant is simply that endogenous candidate evaluated at the forced $D$. The bridge goal is to make the match $W_{\mathrm{endogenous}}(3)=17=$ wallpaper groups fully explicit and machine-checked.

proof idea

Term proof that builds a three-component conjunction. The first conjunct is the sibling equality that the cube-derived count is 17. The second is the sibling equality that the cube-derived count equals the imported wallpaper-group constant. The third is introduced over an arbitrary natural $w$ and closed by the sibling biconditional equating the wallpaper slot with equality to the passive-edge-plus-faces formula at $D$.

why it matters

Pass-2 endogenous closure package for the counting-layer wallpaper slot. It does not re-prove Fedorov's classification; it certifies that RS cube combinatorics $E_{\mathrm{passive}}+F$ at the forced $D=3$ lands on 17 and matches the imported crystallographic constant. Face-wallpaper pairs enter the alpha stack as the denominator of the curvature fraction, so this identity anchors that counting layer. Framework landmarks: T8 forces $D=3$; passive-edge dressing and the eight-tick octave sit upstream in the alpha derivation. No downstream consumers are recorded yet. The remaining open direction is full endogeneity of $W$ without importing the classical 17.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.