Holography Pixel Local

The pixel count

Holography pixel local is a result in Recognition Science about counting boundary states on a cube. The framework models reality as a discrete ledger, a record of recognition events that must balance. Starting from a forced eight-tick cell in three dimensions, the cube, the subject examines one square face, a boundary pixel, and asks how many distinct recognition sectors that face can hold.

The setup is concrete. Each of the four vertices of a cube face carries one recognition bit, a single on or off value. The ledger closure condition requires that a closed recognition loop posts a balanced, zero-sum ledger around the face, so the four bits must XOR to zero, meaning they have even parity. This is the only admissibility condition, and it comes from the recognition ledger, not from geometry.

The second ingredient is symmetry. Two boundary configurations that differ only by a symmetry of the square, a rotation or a reflection, are the same physical sector. The subject quotients by the square's symmetry group, the eight elements that fix the plaquette. The admissible sectors are the ledger-closed configurations modulo this face stabilizer.

The result is a finite, decidable count: exactly four. The four sectors are the empty loop, an adjacent-edge loop, a diagonal loop, and the full loop. This is the substrate-native realization of the geometric coefficient that appears in the recognition-pixel area formula, where the area splits into an integer, an entropy term, and a length scale. The result is axiom-clean, proved by computation, with no entropy, no length scale, and no area quantity appearing in any definition.

In Recognition Science, this closes the integer leg of a three-leg split. The per-event entropy is already a theorem, and the length scale is provably unreachable from the current dimensionless data. What this subject establishes is the forced integer and nothing more. It does not claim a derived Bekenstein quarter; it supplies the sector count and points the autonomous loop at the two remaining legs.

/-- **The admissible boundary sectors of one cube face**: ledger-closed plaquette
configurations modulo the face stabilizer `D₄`, counted by canonical representative. -/
def admissibleSectors : Finset FaceCfg :=
  Finset.univ.filter (fun c => closed c = true ∧ isSectorRep c = true)

/-- **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

This subject does not derive the area coefficient in the recognition-pixel area formula. This subject does not derive the length scale, which is provably unreachable from the current dimensionless data. This subject does not claim a derived Bekenstein quarter.

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: