Holography Recognition Multiplicity Domino Image Times Kernel

The domino identity

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition event is the posting of a distinction. The declaration domino_image_times_kernel concerns a domino: two adjacent square faces, each face carrying four binary bits. The local rule asks whether each face is closed, meaning its four bits satisfy a parity condition. The theorem states that the number of distinct closure outcomes for the two faces, multiplied by the number of configurations where both faces are closed, equals the total number of configurations of the domino. In symbols, if the image size is 4 and the kernel size is 4, then 4 times 4 equals 16, the total number of bit configurations.

This identity is a rank-consistency check, not a physical derivation. The image size counts the distinct outcomes of the closure map, which is the rank reading: how many different pairs of closure verdicts the two faces can produce. The kernel size counts the configurations that map to the fully closed outcome, which is the nullity reading: how many free bits remain undistinguished. The theorem proves these two counts multiply to the total, a fact that holds by direct computation. But the multiplicity side of the ledger, the number of distinctions posted per face, is fixed by a modeling choice, not by the framework's axioms. A mirror construction with three distinctions per face is equally consistent and yields a different identity.

What the identity does establish is that the rank reading and the nullity reading are mutually exclusive. Under the rank reading, the ledger multiplicity equals the rank, which is 2 for the domino. Under the nullity reading, the multiplicity would equal the nullity, which is 4. Since 2 does not equal 4, the two readings cannot both describe the same ledger. The identity itself does not adjudicate between them; it only shows they diverge. The choice between them remains open, with a candidate argument based on extensivity, the requirement that an area law exist, living in a separate module.

In plain terms, the declaration is a counting fact about a small combinatorial object. It proves that two ways of counting the local rule's freedom are incompatible, and it leaves the physical interpretation of that freedom to a further argument. The theorem is true and axiom-clean, but its scope is conditional on the modeling choice that fixes how many distinctions a closed face posts. That condition is the honest scope of the result.

/-- **First-isomorphism check of the actual two-face map.** `|image| · |kernel| = |domain|`
(`4 · 16 = 64`), pinning rank 2 and nullity 4 without any hand-typed subtraction. -/
theorem domino_image_times_kernel :
    (Finset.univ.image dominoLocalMap).card
      * (Finset.univ.filter (fun c => dominoLocalMap c = (true, true))).card
      = (Finset.univ : Finset DominoCfg).card := by decide

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

theorem dominoNullity_eq_four : dominoNullity = 4 := by decide

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

/-- 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 identity does not select between the rank and nullity readings. The identity does not derive the Bekenstein 1/4 coefficient; that result is conditional on a modeling choice. The identity does not prove that the ledger multiplicity is forced by the framework's axioms.

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: