HolographicFalsifier
plain-language theorem explainer
HolographicFalsifier records candidate ways the holographic bound could fail, such as entropy exceeding the area limit or AdS/CFT breakdown. Researchers assessing ledger-derived quantum gravity would cite it when checking empirical status against observations. The declaration is a plain structure with two string fields, instantiated directly in the experimentalStatus list.
Claim. A record type with fields falsifier : String (description of a potential violation) and status : String (empirical assessment), used to catalog tests of the bound $S ≤ A/(4ℓ_P²)$ arising from ledger projection.
background
The module derives the holographic bound from Recognition Science ledger projection, where entries are fundamentally two-dimensional surfaces and three-dimensional volume is reconstructed from boundary data. Upstream results supply supporting structures: RSNativeUnits.status defines native units with $c=1$, $ħ=φ^{-5}$, and the φ-ladder; PhiForcingDerived.of and LedgerFactorization.of calibrate the J-cost and factorization underlying the projection; NucleosynthesisTiers.of and SimplicialLedger.EdgeLengthFromPsi.is supply discrete tier and edge-length context.
proof idea
This is a structure definition with no computational content or lemmas applied. It functions as a data container whose fields are populated by direct construction in the downstream experimentalStatus list.
why it matters
The structure supplies the type for experimentalStatus, which lists concrete statuses and thereby supports the module's claim that holography is well-supported. It fills the QG-006 target of deriving the bound from ledger structure, consistent with the forcing chain's T8 (D=3) and the Recognition Composition Law. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.