Pith. sign in
module module high

IndisputableMonolith.Verification.WallpaperEndogenousBridge

show as:
view Lean formalization →

Endogenous bridge from RS cube combinatorics to the crystallographic W-count. Defines W from passive edges plus faces at D=3, proves it equals 17 and matches the imported wallpaper-group constant, and records uniqueness of that slot under a finite scan. Mass-path verification cites it to swap the external wallpaper constant for a cube-derived one without changing formulas.

claimAt spatial dimension $D=3$, the endogenous count $W_{\mathrm{from\,cube}}:=E_{\mathrm{passive}}+F$ equals $17$, coincides with the standard wallpaper-group count, and is the unique slot compatible with the endogenous formula under the finite scan up to $64$.

background

Recognition Science forces $D=3$ spatial dimensions (forcing chain T8) and works with cubic-ledger combinatorics rather than importing crystallography as a primitive. The upstream AlphaDerivation module builds seed geometry from that ledger; this module isolates the parallel construction for the wallpaper count $W$.

The endogenous candidate is assembled as passive edge count plus face count on the cube at $D=3$. Sibling definitions package the closed formula, its specialization at $D=3$, and the comparison to the classical count of $17$ wallpaper groups. A finite uniqueness scan (up to $64$) supports that this slot is not an accidental match among nearby integers.

Notation: $W$ is the integer slot that mass-path and related formulas treat as the crystallographic multiplicity; the bridge replaces an external constant with a cube-derived equal.

proof idea

Definition-heavy bridge module. It introduces $W_{\mathrm{endogenous}}$ and $W_{\mathrm{from,cube}}$ via the $E_{\mathrm{passive}}+F$ decomposition at $D=3$, then proves numerical identity with $17$ and with the imported wallpaper-group constant. Matching and uniqueness lemmas (including the scan up to $64$ and the iff between wallpaper slot and endogenous formula) are elementary equalities and finite checks rather than deep analysis. No single master theorem; the module is a certified dictionary from cube counts to $W$.

why it matters in Recognition Science

Feeds WallpaperSufficiencyMassPath, which formalizes the O6 sufficiency route: canonical mass-path formulas stay unchanged when the imported wallpaper_groups constant is replaced by endogenous $W_{\mathrm{from,cube}}=E_{\mathrm{passive}}+F$ at $D=3$. That closes a cleanliness gap in the mass framework: $W$ is no longer an external crystallographic input but a cube-combinatorial output aligned with RS geometry (T8, $D=3$).

Within Verification, the module is the hinge between ledger combinatorics and mass-path audits. It does not derive the continuum classification of wallpaper groups from first principles; it certifies that the RS cube count lands on the same integer those formulas already use.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)