Pith. sign in
module module moderate

IndisputableMonolith.Holography.PixelLocal

show as:
view Lean formalization →

Local model of one holographic boundary pixel: a cube face carrying four recognition bits, one per vertex. Configurations live in a 16-element space; ledger-closed ones are quotiented by the face dihedral group D4 to yield recognition sectors. Downstream holography modules cite the resulting sector count (exactly four) when testing area-additivity, edge bridges, and discrete period exclusion. The development is definitional plus finite enumeration over Fin 16 and D4 orbits.

claimA face configuration is an assignment of one bit to each of the four vertices of a cube face, equivalently an element of $\{0,1\}^4 \cong \mathrm{Fin}\,16$. Ledger-closed configurations are those satisfying the closed-plaquette condition. The face stabilizer is the dihedral group $D_4$ acting by vertex permutation; recognition sectors are $D_4$-orbits of closed configurations (or chosen representatives). The recognition-sector count of one pixel is the number of such orbits, proved equal to $4 = 2^2$.

background

In the Recognition Science holography layer, a spatial cube face is the elementary boundary pixel. Each of its four vertices carries a single recognition bit. The module packs those four bits into the low nibble of a natural number below 16, so the configuration space is finite and enumerable.

Ledger closure is a local parity (or balance) constraint on the four bits: only closed plaquettes are retained as physically admissible. The geometric symmetry of the square face is the dihedral group $D_4$ of order 8; it acts on configurations by permuting vertices. Recognition sectors are the orbits of closed configurations under this action (equivalently, a set of orbit representatives).

The module sits upstream of the discrete half of the Bekenstein–Hawking coefficient program and of the panel's GAP-1 tests: one needs a precise, machine-checked count of sectors on a single pixel before asking whether that count behaves like an area density or feeds an eight-tick census.

proof idea

This is primarily a definitions-and-enumeration module, not a deep proof development. Face configurations, bit extractors, the closed predicate, the $D_4$ stabilizer, and its action are introduced as finite combinatorial objects over Fin 16 and finite types from Mathlib.

Admissible sectors are defined as closed configurations modulo the face action (or as a filtered set of representatives). The equality admissibleSectors_eq and the theorem that the recognition-sector count equals a power of two are discharged by exhaustive finite checking and orbit counting: with only 16 configurations and a group of order 8, the closed subset and its orbits can be listed completely. No analytic or continuum argument appears here.

why it matters in Recognition Science

PixelLocal is the shared combinatorial substrate for four holography modules. PixelGluedPlaquette (live bet LB1) quotes the single-pixel count of exactly four ledger-closed sectors modulo $D_4$ and shows that gluing two faces does not double the count, so the integer is not an extensive area density. EdgeSectorBridge treats sectors as a deterministic lossy quotient of edge bits and needs the local sector vocabulary. EightTickSubperiodExclusion uses the admissible census in the discrete half of the deficit-free period argument (full 8-tick turn, no proper submultiple). RecordCostAsymmetry builds the rank/nullity selector from the same record-cost and sector language.

Within the framework landmarks, the face is the spatial dual of the eight-tick octave structure (T7) on a 3-dimensional cube (T8): four vertices, dihedral symmetry, and a $2^k$ sector count feed later entropy and area claims without yet asserting the Bekenstein–Hawking coefficient.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (12)