Holography Pixel Local Face Stabilizer

The face stabilizer

The face stabilizer is a symmetry rule applied to the corner patterns of a square. A square has eight symmetries: four rotations (0, 90, 180, 270 degrees) and four reflections (across its two diagonals and its two midlines). The rule says that two corner patterns that differ only by one of these eight moves are the same physical sector, not different states. This is a standard mathematical maneuver: quotienting a set by a group's action to count genuinely distinct shapes.

The framework applies this rule inside a specific counting problem. In Recognition Science, a boundary recognition pixel is modeled as one face of a cube, with a recognition bit placed on each of its four corners. A recognition bit is a single binary value, 0 or 1, representing whether a recognition event occurred at that corner. A configuration is admissible only if its four bits satisfy a ledger closure condition: a closed recognition loop posts a balanced, zero-sum ledger around the face, which here means the four bits must XOR to 0, an even parity condition. This admissibility condition comes from the recognition ledger, not from geometry.

Combining these two rules, the framework defines the face stabilizer as the list of the square's eight vertex permutations. It then counts the admissible corner patterns modulo these symmetries, retaining only the numerically smallest pattern in each orbit as its canonical representative. The count is a finite, decidable number, and a theorem in the framework's machine-checked library of formal theorems proves it equals exactly 4. The four sectors are the empty loop (0000), an adjacent-edge loop (0011), a diagonal loop (0101), and the full loop (1111). This is the concrete realization of the geometric coefficient 4 that appears in the recognition pixel area formula a_pix = 4 · H · ℓ_P².

What the theorem does not claim is as important as what it proves. The count of 4 is pure plaquette combinatorics on the forced 8 = 2³ substrate; no entropy H, no length scale ℓ_P², and no area quantity appears in any definition. The theorem does not link this sector count to the area coefficient in the pixel area formula; that link is a separate argument, not the enumeration. The length scale ℓ_P² is provably unreachable from the current dimensionless theorem data, requiring a new forced action normalization that carries a length. The module supplies the forced integer and nothing more; it does not allow anyone to claim a derived Bekenstein 1/4.

The practical consequence is a clean, verified count that closes one leg of a three-leg split. The framework's holography panel separated the pixel area into three quantities: the integer 4, the per-event entropy H, and the area scale ℓ_P². This theorem establishes the integer leg on the actually forced discrete substrate, rather than by importing continuum isotropy or any Bekenstein-Hawking input. The remaining two legs, the entropy and the length scale, remain open targets for future work.

/-- **The face stabilizer `D₄`**: the 8 symmetries of the square (4 rotations +
4 reflections), as permutations of the 4 vertices arranged in cyclic order 0-1-2-3. -/
def faceStabilizer : List (Fin 4 → Fin 4) :=
  [ ![0, 1, 2, 3], ![1, 2, 3, 0], ![2, 3, 0, 1], ![3, 0, 1, 2],
    ![0, 3, 2, 1], ![2, 1, 0, 3], ![1, 0, 3, 2], ![3, 2, 1, 0] ]

/-- **Ledger closure** on the plaquette: the 4 vertex bits XOR to 0 (even parity).
A closed recognition loop posts a balanced (zero-sum) ledger around the face. -/
def closed (c : FaceCfg) : Bool :=
  ! (vbit c 0 ^^ vbit c 1 ^^ vbit c 2 ^^ vbit c 3)

/-- **THEOREM (axiom-clean, by `decide`). The D=3 forced lattice yields exactly 4
recognition sectors per boundary face.**

`card(AdmissibleBoundarySectors / FaceStabilizer) = 4 = 2^(D-1)`. No `H`, no `ℓ_P`,
no area input enters any definition; the count is pure ledger-closed plaquette
combinatorics on the forced 8 = 2³ substrate. -/
theorem recognition_sector_count : admissibleSectors.card = 4 := by decide

/-- The four sectors are exactly the orbit minima `{0000, 0011, 0101, 1111}`
(empty loop, an adjacent-edge loop, a diagonal loop, the full loop). -/
theorem admissibleSectors_eq :
    admissibleSectors = ({0, 3, 5, 15} : Finset FaceCfg) := by decide

/-- **THEOREM (axiom-clean, by `decide`). The D=3 forced lattice yields exactly 4
recognition sectors per boundary face.**

`card(AdmissibleBoundarySectors / FaceStabilizer) = 4 = 2^(D-1)`. No `H`, no `ℓ_P`,
no area input enters any definition; the count is pure ledger-closed plaquette
combinatorics on the forced 8 = 2³ substrate. -/
theorem recognition_sector_count : admissibleSectors.card = 4 := by decide

What this page does not claim

The theorem does not derive the entropy H or the length scale ℓ_P². The theorem does not link the sector count to the area coefficient in the pixel area formula. The theorem does not derive the Bekenstein-Hawking entropy 1/4.

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/Holography/PixelLocal.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: