Pith. sign in
module module moderate

IndisputableMonolith.Verification.WallpaperSufficiencyMassPath

show as:
view Lean formalization →

Verification module showing the endogenous crystallographic weight W from cube combinatorics equals the imported W used in mass topology, on the canonical dimension. It rewrites ledger fraction, base shift, and μ–τ step in endogenous form, then packages full mass-path replacement. Cite when auditing that lepton mass scaffolding no longer depends on an external wallpaper constant. Argument is a chain of equality rewrites from the endogenous bridge.

claimOn the canonical dimension, the endogenous crystallographic weight $W_{\mathrm{end}}$ equals the imported mass-topology weight $W$. Consequently the refined ledger fraction, base shift, and $\mu$–$\tau$ step admit endogenous rewrites, and the mass path is fully replaceable by endogenous data.

background

Recognition Science builds lepton masses on a φ-ladder with topological corrections from the cubic ledger $Q_3$. Mass topology (T9) supplies the refined ledger fraction

$$\delta = 2W + \frac{W + E_{\mathrm{total}}}{4 E_{\mathrm{passive}}} + \alpha^2 + E_{\mathrm{total}}\alpha^3,$$

where $W$ has historically been the classical count of wallpaper groups ($W=17$).

WallpaperEndogenousBridge (Pass 2) constructs that same integer from cube combinatorics rather than importing it as external mathematics. AlphaDerivation contributes the cubic-ledger seed and φ-dressing used around the fine-structure sector; lepton-generation defs isolate the mass-path primitives so import cycles stay broken.

This module sits in Verification: it checks that the endogenous $W$ and the $W$ already wired into MassTopology agree, then pushes that equality through every intermediate quantity on the mass path.

proof idea

Not a definition-only file. Structure is a short equality cascade:

  1. Prove endogenous $W$ equals MassTopology's $W$ on the canonical dimension (bridge equality).
  2. Rewrite the ledger fraction by substituting that equality.
  3. Rewrite the base shift the same way.
  4. Rewrite the μ–τ generation step.
  5. Bundle the four facts into a single completeness statement that the mass path is endogenously replaceable.

Each step is an algebraic transport of equality along the definitions already fixed in MassTopology and LeptonGenerations, using the WallpaperEndogenousBridge identification of $W$.

why it matters in Recognition Science

Closes a honesty gap flagged by WallpaperEndogenousBridge: the framework had imported wallpaper_groups = 17 as classical input. After this module, the mass-path formulas that feed T9/T10 lepton work can cite an endogenous cube-combinatorial $W$ instead.

No downstream Lean consumers are recorded yet (used_by empty); the payload is the sibling completeness lemma mass_path_endogenous_replacement_complete and the four supporting equalities. In the broader chain this supports the audit claim that mass topology corrections are RS-native rather than smuggled classical crystallography, sitting beside the alpha seed assembly and the φ-ladder mass formula.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (5)