Verification Wallpaper Endogenous Bridge

The counting bridge

The 17 wallpaper groups are the distinct ways a flat surface can be tiled with a repeating pattern, a classification completed by Evgraf Fedorov in 1891. Recognition Science does not re-prove that classification. Instead, its machine-checked library of formal theorems builds a bridge: it shows that a simple count derived from cube combinatorics lands on the same number, 17, at three dimensions.

The count comes from two pieces of a cube. The first is the number of edges on a cube that are not part of the active recognition cycle, a recognition event being a discrete record of a comparison. The second is the number of faces. At three dimensions, those counts are 11 and 6, and their sum is 17. The module defines this as W_endogenous(D) = passive_field_edges(D) + cube_faces(D), and for D=3 the theorem W_endogenous_at_D3 proves the result equals 17.

The bridge then proves that this endogenous count matches the imported wallpaper constant. The theorem W_endogenous_matches_wallpaper_groups states W_endogenous(3) = wallpaper_groups. A further uniqueness result, wallpaper_slot_unique_from_endogenous_formula, shows that any number satisfying the cube formula at three dimensions is forced to equal the wallpaper constant. A finite computational scan up to dimension 64 confirms that only D=3 yields 17, making the match specific to three dimensions.

In Recognition Science, this is a bridge step, not a full derivation. The framework still imports the wallpaper classification as a classical fact; the module formalizes an endogenous candidate that agrees with it. The plain-language takeaway is that the number 17, long known from tiling theory, also emerges from counting cube structure, and the framework's library checks that agreement mechanically.

/-- At `D=3`, the endogenous candidate is exactly 17. -/
theorem W_endogenous_at_D3 : W_endogenous D = 17 := by
  native_decide

/-- At `D=3`, the endogenous candidate matches the imported wallpaper constant. -/
theorem W_endogenous_matches_wallpaper_groups :
    W_endogenous D = wallpaper_groups := by
  native_decide

/-- Uniqueness form: any `w` satisfying the endogenous wallpaper formula
at `D=3` is forced to the imported wallpaper constant. -/
theorem wallpaper_slot_unique_from_endogenous_formula (w : ℕ)
    (hw : w = passive_field_edges D + cube_faces D) :
    w = wallpaper_groups := by
  exact (wallpaper_slot_iff_endogenous_formula w).2 hw

theorem unique17ScanUpTo64_true : unique17ScanUpTo64 = true := by
  native_decide

What this page does not claim

This module does not re-prove the 1891 wallpaper classification. The match at D=3 is a bridge step, not a full derivation of the wallpaper constant from first principles. The computational scan up to dimension 64 does not prove uniqueness for all dimensions.

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/WallpaperEndogenousBridge.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: