Pith. sign in
module module high

IndisputableMonolith.Holography.EdgeSectorBridge

show as:
view Lean formalization →

Defines the ledger-closed edge configurations: the four raw boundary bits that satisfy the parity (ledger-closure) constraint, before any D₄ quotient. Supplies the pre-closure edge substrate for the live 4H/3H fork in RS holography. Downstream coefficient and record-cost modules import this bridge to choose whether the pixel multiplicity attaches to rank or to a lossy sector quotient. The argument is mostly finite enumeration plus an explicit sector map.

claimOn the discrete edge of a recognition pixel, let the raw configurations be bit-strings $e \in \{0,1\}^4$. The ledger-closed set $C$ is the subset of those strings whose parity (ledger-closure) constraint holds. A sector map $s: C \to \mathcal{S}$ sends each closed edge to an admissible recognition sector; $s$ is surjective onto the closed image and realizes a lossy quotient of $C$. The free-bit count and $|C|$ are recorded as finite combinatorial facts feeding the $4H$ vs $3H$ selector.

background

Recognition Science holography splits the 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 Planck area scale. Upstream PixelLocal attacks the integer on the forced $D=3$, eight-tick ($2^3$) lattice substrate rather than by continuum area counting. $H$ is already forced elsewhere; $\ell_P^2$ is blocked by a scale-invariance no-go, so the remaining discrete work is the edge combinatorics.

This module isolates the pre-quotient edge data. Raw edges are four bits. Ledger closure is a parity constraint on those bits; the surviving configurations are the closed set. Only after that set is fixed does one ask how (or whether) a $D_4$ or sector identification collapses it. The siblings name that closed set, its cardinality, its free-bit count, and an explicit sector map with surjectivity and lossy-quotient lemmas.

The local setting is therefore finite Boolean edge space with a linear constraint, not continuum holography. The $4H$/$3H$ fork is precisely whether physical multiplicity tracks the closed rank before quotient or the coarser sector count after a lossy map.

proof idea

Definition-heavy bridge module, not a single deep theorem. Closed configurations are introduced as the parity-satisfying subset of the four edge bits; cardinality and free-bit counts are discharged by finite decide/enumeration on Finset and Fintype infrastructure imported from Mathlib.

The sector map is defined explicitly from closed edges into the admissible sector type inherited from PixelLocal. Membership in admissible sectors, surjectivity onto the closed image, and the lossy-quotient statement are short lemmas: image reasoning plus the combinatorial gap between $|C|$ and the sector count. A certificate bundle packages the bridge facts for downstream import. No analytic estimates; pure finite combinatorics on the edge substrate.

why it matters in Recognition Science

Feeds the panel-critical coefficient choice in RS holography. CoefficientBridge imports this module because the count-to-area factor $\kappa$ in $a_{\mathrm{pix}} = \kappa \cdot H \cdot \ell_P^2$ is not a number for decide to pick among labelled integers; it is a physical selector between ledger-closure rank and coarser entropy labels. Without a named pre-quotient closed edge set, that selector has no substrate.

RecordCostAsymmetry likewise imports the bridge to frame the rank/nullity reading of the same fork (the record-cost, formerly Landauer-asymmetry, course correction). The live $4H$/$3H$ dispute is exactly whether multiplicity attaches to the closed four-bit parity locus defined here or to a lossy sector quotient of it.

In the broader chain this sits under the holography attack on the integer in $a_{\mathrm{pix}}$, complementary to forced $H$ and the blocked $\ell_P^2$ scale, on the $D=3$ eight-tick lattice forced by T7–T8.

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)