Pith. sign in
module module high

IndisputableMonolith.Holography.KeystoneFactorThree

show as:
view Lean formalization →

The holographic factor 3 relating microstate cost to record cost is forced by the ledger of a one-face closure map, not inserted by hand. Kernel-side cost is exactly three times image-side cost, both obtained by deciding the actual map. Holography and Bekenstein-bound workers cite this when selecting the record reading over the microstate reading. The argument is finite enumeration plus saturation of the area bound.

claimFor the one-face closure map, the kernel-side (microstate) recognition cost equals three times the image-side (record) cost: $C_{\mathrm{ker}}=3\,C_{\mathrm{im}}$ with $C_{\mathrm{im}}=1$, so the density ratio is exactly $3$. The factor $3$ in the microstate assignment $3\cdot(A/4)$ is this ledger ratio. The record reading saturates the Bekenstein bound; the microstate reading violates it in a scale-free way.

background

Recognition holography compares two cost readings of the same geometric map: a microstate (kernel) reading and a record (image) reading. The upstream module RecordCostAsymmetry supplies the rank/nullity selector that distinguishes those readings and frames the panel correction away from a pure Landauer story toward record-cost asymmetry.

This module isolates the numerical factor that appears when the one-face closure map is costed on both sides. Both costs are computed by deciding the concrete map; the identity $3=3\cdot 1$ is therefore ledger data, not a free parameter. Sibling material packages a total-entropy Bekenstein bound, saturation for the record chain, and a scale-free violation for the microstate chain.

The local setting is the LEG-B holography chain: area-law entropy bounds, cost asymmetry between kernel and image, and selection of the reading that stays deficit-free under holonomy closure.

proof idea

The module is theorem-bearing, not a pure definition dump. The core ratio is obtained by evaluating kernel and image costs of the one-face closure map (decidable finite data), yielding density ratio three and the forced identity $3=3\cdot 1$.

From there the argument branches: the record reading is shown to saturate the total-entropy Bekenstein bound; the microstate reading is shown to violate it. Violation lemmas establish scale-freeness and survival under unit conversion, so the contradiction is not an artifact of normalization. A keystone certificate packages the comparison and selects the record reading as the only bound-compatible chain.

why it matters in Recognition Science

Without a ledger-forced factor 3, the microstate assignment $3\cdot(A/4)$ would be an external ansatz. This module pins that coefficient to the actual cost ratio of the closure map and certifies that only the record reading saturates the Bekenstein bound.

Downstream, DeficitFreePeriod imports the module as part of the LEG-B core chain that forces the holonomy period $2\pi/\kappa$. That parent is theorem-status on the mathematical spine (with named model premises on the physics bridge). The keystone certificate is the hinge: record-chain saturation versus microstate-chain contradiction, feeding deficit-free period selection.

In the broader Recognition stack this is holography infrastructure for area-law consistency, not a T0–T8 forcing step, but it is required wherever the framework claims the factor 3 is derived rather than typed.

scope and limits

used by (1)

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 (11)