Holography Recognition Multiplicity Coefficient Is One Quarter Derived

The one-quarter coefficient

The ledger, a discrete record of performed distinctions, assigns a cost to each configuration of a physical cell. In the Recognition Science framework, this cost is the recognition multiplicity. The declaration coefficient_is_one_quarter_derived is a theorem in the machine-checked library of formal theorems. It states that, for a single cell, the ratio of one unit of recognition multiplicity to the number of admissible sectors is exactly 1/4. The proof is a direct computation: it unfolds definitions and applies a previously established selector theorem.

The theorem's scope is narrower than its name suggests. The proof of the underlying selector theorem, bekenstein_selector_derived, closes the goal 1 = closureRank directly. It does not use the ledger construction at all. The ledger's shape, specifically the choice to post one distinction per face, is a modeling choice encoded in the definition of cellLedger. A mirror construction, cellLedgerNullity, posts three distinctions per face and is equally consistent with the underlying axioms. Both lead to different values for the coefficient. The theorem therefore establishes a conditional consistency check: if one accepts the one-distinction-per-face reading, then the ratio is 1/4. It does not establish that this reading is the only possible one.

This distinction matters for the framework's ambitions. The coefficient 1/4 is a famous number in physics, appearing in the Bekenstein-Hawking formula for black hole entropy. The framework aims to derive such constants from first principles. Here, the derivation is conditional on a choice that the axioms do not force. The open question is whether a non-circular argument can force the rank reading. The candidate argument, based on gluing invariance and extensivity, lives in a separate module and remains open.

/-- **CONDITIONAL (modeling choice): the Bekenstein-Hawking coefficient `1/4`.** The
pixel-to-sector ratio is exactly `1/4` GIVEN the rank reading of the selector. Conditional
on the `cellLedger` one-generator-per-face choice, NOT forced by T-1 alone (audit
`holo_mult_fable_20260702`). The name `_derived` is kept for downstream stability. -/
theorem coefficient_is_one_quarter_derived :
    (1 : ℚ) / (PixelLocal.admissibleSectors.card : ℚ) = 1 / 4 :=
  CoefficientBridge.bekenstein_of_selector 1 bekenstein_selector_derived

/-- **CONDITIONAL (modeling choice): the Bekenstein-Hawking coefficient `1/4`.** The
pixel-to-sector ratio is exactly `1/4` GIVEN the rank reading of the selector. Conditional
on the `cellLedger` one-generator-per-face choice, NOT forced by T-1 alone (audit
`holo_mult_fable_20260702`). The name `_derived` is kept for downstream stability. -/
theorem coefficient_is_one_quarter_derived :
    (1 : ℚ) / (PixelLocal.admissibleSectors.card : ℚ) = 1 / 4 :=
  CoefficientBridge.bekenstein_of_selector 1 bekenstein_selector_derived

/-- **CONDITIONAL (modeling choice): the Bekenstein selector.**
`selector_multiplicity_is_closure_rank 1` holds. AUDIT NOTE (`holo_mult_fable_20260702`):
the proof term below closes `1 = closureRank` directly and never consumes
`recognitionMultiplicity` or `cellLedger` — the ledger construction is not load-bearing
here, so this theorem does not DERIVE the selector from T-1; it instantiates the rank
reading. The name `_derived` is kept only for downstream stability
(`RecordCostAsymmetry` re-exports it). GAP 1's selector remains open pending the
extensivity/gluing-invariance forcing in the quad module. -/
theorem bekenstein_selector_derived :
    CoefficientBridge.selector_multiplicity_is_closure_rank 1 := by
  unfold CoefficientBridge.selector_multiplicity_is_closure_rank
  rw [CoefficientBridge.closureRank_eq_one]

/-- The **defect ledger of a `k`-face cell**: `k` distinct primitive posted distinctions,
one per D=3-forced unit face, each of multiplicity one. This is a MODELING CHOICE, not a
T-1 consequence (audit `holo_mult_fable_20260702`): T-1 says a closed recognition loop
posts distinctions but does not fix HOW MANY per face. One-per-face encodes the rank
reading; a mirror three-per-face ledger (one per free bit) would encode the nullity
reading and is equally T-1-consistent. The choice made here is what downstream theorems
are conditional on. It knows only the face count — nothing about the closure map. -/
noncomputable def cellLedger : ℕ → Foundation.RecognitionLedgerFloor.DefectLedger ℕ
  | 0 => 0
  | (k+1) => cellLedger k + Finsupp.single k 1

What this page does not claim

The theorem does not prove that the one-distinction-per-face ledger is the only possible one. The theorem does not derive the 1/4 coefficient from the axioms alone, only from a specific modeling choice. The theorem does not establish that the rank reading is physically correct over the nullity reading.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/RecognitionMultiplicity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: