Holography Recognition Multiplicity Target Recognition Multiplicity Holds

What the multiplicity target proves

The declaration target_recognition_multiplicity_holds is a theorem in the framework's machine-checked library of formal theorems. It bundles together six smaller results about a cell built from unit faces, each face a minimal closed recognition loop. The central fact is a consistency check: the cost of the cell's recognition ledger, which counts posted distinctions, equals the cell's rank, which counts the number of independent parity checks that close. For one face the cost is 1 and the rank is 1; for two faces the cost is 2 and the rank is 2. The theorem also records that this cost diverges from the nullity, the count of free bits, which is 4 for two faces. A further result states that the ratio of one pixel to its admissible sectors is 1/4.

The honest scope is narrow. The ledger construction itself is a modeling choice, not a derivation. The framework's own audit found that the theorem bekenstein_selector_derived, which names a Bekenstein-style selector, never actually uses the ledger; its proof closes directly on the rank. A mirror construction with three generators per face instead of one is equally consistent with the underlying axioms and yields the opposite divergence. So the theorem proves that two readings of the ledger, rank versus nullity, are mutually exclusive, but it does not select between them. The 1/4 coefficient is conditional on the one-generator-per-face choice.

What survives is a rank-consistency check. If one posts one distinction per face, then the ledger multiplicity provably tracks the closure rank and provably diverges from the nullity on the domino. The theorem rules the two readings mutually exclusive; it does not adjudicate. The open route to forcing the rank reading is an extensivity argument, that an area law demands the extensive branch, which lives in a separate quad module and is not part of this declaration.

/-- **Bridge at one face (the selector's target).** The ledger multiplicity of one plaquette
equals the closure rank. Computed by two disjoint routes: `recognitionMultiplicity 1` from
the ledger floor, `CoefficientBridge.closureRank` from the image of `PixelLocal.closed`. -/
theorem multiplicity_eq_rank_one :
    recognitionMultiplicity 1 = (CoefficientBridge.closureRank : ℝ) := by
  rw [recognitionMultiplicity_eq, CoefficientBridge.closureRank_eq_one]

/-- **Bridge at two faces (the divergence witness).** `recognitionMultiplicity 2 = 2 = dominoRank`
— the ledger multiplicity tracks the rank even where rank and nullity have split apart. -/
theorem multiplicity_eq_rank_two :
    recognitionMultiplicity 2 = (dominoRank : ℝ) := by
  rw [recognitionMultiplicity_eq, dominoRank_eq_two]

/-- **The divergence witness — scoped.** `recognitionMultiplicity 2 = 2`, but the nullity is
`4`, so `2 ≠ 4`: UNDER the rank reading encoded in `cellLedger`, multiplicity diverges from
nullity, so the two readings are mutually exclusive. It does NOT rule out the `κ = 4/3`
branch on its own: the mirror `cellLedgerNullity` (three generators per face) yields the
symmetric witness `6 ≠ 2` for the other branch. What it does establish non-trivially: a
dependent gluing would have broken `multiplicity = rank` even under this reading. -/
theorem multiplicity_ne_nullity_two :
    recognitionMultiplicity 2 ≠ (dominoNullity : ℝ) := by
  rw [recognitionMultiplicity_eq, dominoNullity_eq_four]; norm_num

/-- **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

What this page does not claim

The declaration does not prove that the ledger construction is the only one consistent with the axioms. It does not derive the 1/4 coefficient independently of the modeling choice. It does not select between the rank and nullity readings of the ledger.

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: