Pith. sign in
module module moderate

IndisputableMonolith.Holography.CoefficientBridge

show as:
view Lean formalization →

Defines the ledger-closure rank, free-bit count, and raw-bit count on face configurations, then proves they evaluate to 1, 3, and 4. The ratio rank/rawBits supplies the holographic coefficient 1/4 without assuming it. Downstream multiplicity and record-cost modules import this bridge. The argument reads rank off the image cardinality of the closure map and checks the rank-nullity identity.

claimFor the landed ledger-closure map $\mathrm{closed}:\mathrm{FaceCfg}\to\{\mathrm{true},\mathrm{false}\}$, set $\mathrm{closureRank}=\log_2|\mathrm{im}(\mathrm{closed})|$, $\mathrm{rawBits}=4$, $\mathrm{freeBits}=3$. Then $\mathrm{closureRank}=1$, the rank-nullity identity $\mathrm{closureRank}+\mathrm{freeBits}=\mathrm{rawBits}$ holds, and the target coefficient bridge identifies $\mathrm{closureRank}/\mathrm{rawBits}=1/4$ with the holographic selector coefficient.

background

Holography in Recognition Science tracks how discrete ledger data on faces and edges compress under recognition events. Upstream, EdgeSectorBridge treats sectors as a deterministic lossy quotient of edge bits and records the panel verdict that a naive sector reading of the factor $4H$ is not physical. RecognitionEventCapacity replaces orbit-count access bounds by forced-measure outcome quantization: a single recognition event resolves into $\varphi^{-n}$-weighted outcomes (T9 measure forcing).

This module works on the landed closure map $\mathrm{closed}:\mathrm{FaceCfg}\to\mathrm{Bool}$. Rank is $\mathrm{Nat.log2}$ of the image cardinality, read from the actual map rather than defined as a difference of bit counts. The parity functional hits both Boolean values, so $|\mathrm{image}|=2=2^1$ and rank equals 1. Raw bits count the full face configuration space dimension (four); free bits count the kernel/null directions (three).

The coefficient bridge packages the identity rank + freeBits = rawBits together with the numerical evaluations into a single target statement that the holographic coefficient is rank/rawBits = 1/4.

proof idea

Definitions first: closureRank from image cardinality of closed, freeBits and rawBits as fixed natural numbers. Three evaluation lemmas prove closureRank = 1 (parity hits both values), freeBits = 3, rawBits = 4. rank_nullity_add and closure_image_times_kernel establish the additive decomposition of configuration space into image and kernel factors. target_coefficient_bridge packages the ratio claim; target_coefficient_bridge_holds discharges it from the evaluations. coefficient_of_multiplicity and bekenstein_branch expose the 1/4 selector for downstream use. No deep analytic machinery: finite-set cardinality, log2 of a two-element image, and arithmetic on small naturals.

why it matters in Recognition Science

Supplies the numerical rank/rawBits = 1/4 bridge that later holography modules treat as the ledger-side origin of the Bekenstein coefficient. RecognitionMultiplicity imports it when encoding the selector as a T-1 ledger (panel-retagged conditional on modeling choice, not an unconditional derivation). RecordCostAsymmetry imports it for the rank/nullity selector under the record-cost reading, after the naming correction away from Landauer framing.

In the broader RS chain the module sits downstream of edge-sector and recognition-event capacity work, and upstream of multiplicity and cost-asymmetry arguments. It does not itself invoke T5 J-uniqueness, phi forcing, or the eight-tick octave; it only fixes the discrete coefficient that those layers later interpret thermodynamically.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)