Pith. sign in
module module high

IndisputableMonolith.Holography.EdgeSectorBridge

show as:
view Lean formalization →

Isolates the ledger-closed boundary configurations: the four raw edge bits that satisfy the parity (ledger-closure) constraint, before any D₄ quotient. This is the pre-closure edge substrate for the live 4H/3H fork in the RS holography panel. Anyone tracking the integer coefficient in a_pix = κ H ℓ_P² cites it. The module defines the closed set, its card and free bits, and a lossy surjective sector quotient.

claimOn four raw edge bits, the ledger-closed configurations are the assignments obeying the parity (ledger-closure) constraint, prior to any $D_4$ identification. The module defines that closed set, records its cardinality and free-bit count, and exhibits a surjective lossy quotient from closed configs onto the admissible recognition sectors.

background

The RS holography panel splits the recognition-pixel area $a_{\mathrm{pix}} = 4 \cdot H \cdot \ell_P^2$ into three separately forced pieces: the integer coefficient, the per-event entropy $H = (\varphi+2)\log\varphi$, and the area scale $\ell_P^2$. Upstream PixelLocal attacks the integer on the forced discrete substrate (D=3 spatial, eight-tick $2^3$ lattice). $H$ is already a theorem; $\ell_P^2$ is blocked by a scale-invariance no-go.

This module sits one layer below any $D_4$ quotient. A plaquette boundary carries four raw edge bits. Ledger closure is the parity constraint on those bits. Closed configs are exactly the parity-satisfying assignments; sectors are their images under a lossy map that forgets some closed-config data. The live panel fork (4H vs 3H) is about which count multiplies $H$ after this substrate is fixed.

proof idea

Definition-and-lemma module, not a single deep proof. It introduces the closed configuration set (parity-satisfying 4-bit edge assignments), proves cardinality and free-bit count lemmas, defines the sector map from closed configs into admissible sectors, and shows that map is surjective on the closed set and is a lossy quotient. A small certificate packages the bridge facts for downstream import. No heavy tactic automation; the content is finite combinatorics on edge bits plus the quotient statement.

why it matters in Recognition Science

Direct feedstock for CoefficientBridge, where panel GAP 1 is restated: the coefficient $\kappa$ in $a_{\mathrm{pix}} = \kappa \cdot H \cdot \ell_P^2$ is not a number for decide to pick among labelled integers, but a named physical selector (does per-plaquette multiplicity attach to ledger-closure rank, pointing at 4H, or to a reduced count, pointing at 3H?). Also imported by RecordCostAsymmetry, which frames the same rank/nullity selector from the record-cost reading.

Without a clean pre-closure edge substrate, the 4H/3H fork has no combinatorial object to select on. The module therefore anchors the holography integer attack to the T7 eight-tick / T8 D=3 discrete lattice already forced upstream, while leaving the physical selector itself to the downstream bridge modules.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)