Verification Wallpaper Sufficiency Mass Path

The sufficiency check

In the Recognition Science framework, the mass path is a sequence of formulas that connect the structure of a cube to particle masses. Some of those formulas use a constant called wallpaper_groups, which counts the seventeen plane symmetry groups. That constant was imported from conventional crystallography. The verification module asks a simple question: if the framework stops borrowing that number and instead derives it from its own geometry, do the mass formulas still work?

The module proves the answer is yes. It defines an endogenous replacement, W_from_cube, built from the passive energy E_passive and the total energy E_total of the cube at dimension D=3. The first theorem shows this derived value equals the imported one. The next three theorems show that the three canonical mass-path formulas, the ledger fraction, the base shift, and the mu-to-tau step, are unchanged when the imported constant is swapped for the endogenous one. The final theorem packages all four results into a single statement of closure.

What this establishes in plain language is that the mass path does not depend on an external input at this point. The framework can supply its own version of the crystallographic constant, and every formula that uses it remains identical. This is a consistency result, not a new physical prediction. It confirms that the mass framework is self-contained at D=3 with respect to this particular constant, and it removes a potential objection that the mass formulas secretly relied on an unexamined imported value.

/-- Endogenous and imported `W` coincide on the canonical dimension. -/
theorem W_endogenous_eq_massTopology_W : W_from_cube = W := by
  simpa [W] using W_from_cube_eq_wallpaper_groups

/-- The ledger-fraction formula is invariant under replacing `W` by `W_from_cube`. -/
theorem ledger_fraction_rewrite_endogenous :
    ledger_fraction = (W_from_cube + E_total) / (4 * E_passive) := by
  unfold ledger_fraction
  rw [W_endogenous_eq_massTopology_W]

/-- The base shift is invariant under the endogenous replacement of `W`. -/
theorem base_shift_rewrite_endogenous :
    base_shift = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) := by
  have hW : (W : ℝ) = (W_from_cube : ℝ) := by
    exact_mod_cast W_endogenous_eq_massTopology_W.symm
  calc
    base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by simp [base_shift]
    _ = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) := by
          simp [hW, ledger_fraction_rewrite_endogenous]

/-- The mu→tau step formula is invariant under the endogenous replacement of `W`. -/
theorem step_mu_tau_rewrite_endogenous :
    step_mu_tau = (cube_faces D : ℝ) - (2 * W_from_cube + D) / 2 * Constants.alpha := by
  have hW : wallpaper_groups = W_from_cube := by
    simpa [W] using W_endogenous_eq_massTopology_W.symm
  simp [step_mu_tau, hW]

/-- Packaged mass-path closure: all canonical `W`-bearing formulas used in the
mass path are invariant under replacing imported `wallpaper_groups` with
endogenous `W_from_cube`. -/
theorem mass_path_endogenous_replacement_complete :
    W_from_cube = W ∧
    ledger_fraction = (W_from_cube + E_total) / (4 * E_passive) ∧
    base_shift = 2 * (W_from_cube : ℝ) + ((W_from_cube + E_total) / (4 * E_passive) : ℚ) ∧
    step_mu_tau = (cube_faces D : ℝ) - (2 * W_from_cube + D) / 2 * Constants.alpha := by
  refine ⟨W_endogenous_eq_massTopology_W, ledger_fraction_rewrite_endogenous,
    base_shift_rewrite_endogenous, step_mu_tau_rewrite_endogenous⟩

What this page does not claim

This module does not derive the value of wallpaper_groups from first principles. This module does not prove that the mass path is complete or physically correct. This module does not establish the equivalence for dimensions other than D=3.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/WallpaperSufficiencyMassPath.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: