IndisputableMonolith.Holography.RecognitionMultiplicity

   1import IndisputableMonolith.Holography.CoefficientBridge
   2import IndisputableMonolith.Holography.PixelGluedPlaquette
   3import IndisputableMonolith.Foundation.RecognitionLedgerFloor
   4
   5/-!
   6# RecognitionMultiplicity: the selector ENCODED as a T-1 ledger (rank-consistency check)
   7
   8**RETAGGED (adversarial panel `holo_mult_fable_20260702`, judge Fable 5 over 6 directors
   9+ one debate round): CONDITIONAL on a modeling choice, NOT a derivation.** The earlier
  10headline ("the Bekenstein 1/4 selector, DERIVED from the ledger floor, FORCED conditional
  11on T-1") is retracted on proof-term evidence:
  12
  13* `bekenstein_selector_derived` never references `recognitionMultiplicity` or `cellLedger`;
  14  its proof term closes `1 = closureRank` directly. The ledger construction is not
  15  load-bearing in the payoff theorem.
  16* `cellLedger` types ONE generator per face **by fiat**. A mirror `cellLedgerNullity`
  17  (three generators per face, one per free bit) is equally T-1-consistent, equally
  18  axiom-clean, equally additive, and yields its own "divergence witness" for the opposite
  19  branch. Bare T-1 underdetermines the ledger's shape, so the shape IS the selector,
  20  encoded rather than derived.
  21
  22What survives (the theorems are all true and stay): this module is a **rank-consistency
  23check** — IF one posts one distinction per face (the rank reading of T-1), THEN the ledger
  24multiplicity provably tracks the closure rank and provably diverges from the nullity on
  25the domino. It rules the two readings mutually exclusive; it does not select between them.
  26The candidate non-circular selector argument is gluing-invariance/extensivity (rank stays
  271 per face under gluing; nullity does not: 3 → 4 ≠ 6 on the domino), formalized in the
  28quad module `PixelQuadPlaquette` — see there for the live forcing argument.
  29
  30Prior history: `T9CarrierBridge` proved the selector EQUIVALENT to an abstract
  31`T9CarrierUniversality` (a step-map surjectivity postulate) and showed T9 multiplicativity
  32alone does not force it. This module then re-encoded the selector at the T-1 ledger floor;
  33the `holo_mult_fable_20260702` audit found that encoding to be a modeling choice, not a
  34forcing. The tag chain is: postulate (`T9CarrierBridge`) → modeling choice (here) →
  35candidate consistency-forcing (quad extensivity, OPEN until landed).
  36
  37## The three independent quantities (each computed by different machinery)
  38
  39For a cell built of `k` D=3-forced unit faces (each a minimal closed recognition loop):
  40
  411. **`recognitionMultiplicity k`** — the recognition ledger cost
  42   (`Foundation.RecognitionLedgerFloor.ledgerCost`, unit weight) of the cell's defect
  43   ledger, one primitive posted double-entry distinction per face. This is grounded
  44   OUTSIDE holography in the T-1/T0 free ledger floor; it never mentions the closure map.
  45   `recognitionMultiplicity_eq : recognitionMultiplicity k = k`.
  46
  472. **rank** — `Nat.log2` of the cardinality of the *image* of the cell's local closure map
  48   (`k` independent GF(2) parity functionals). `k = 1`: `CoefficientBridge.closureRank = 1`
  49   (image `PixelLocal.closed`). `k = 2`: `dominoRank = 2` (image of the two-face map).
  50
  513. **nullity** — `Nat.log2` of the *kernel* cardinality (the free/undistinguished bits).
  52   `k = 1`: `CoefficientBridge.freeBits = 3`. `k = 2`: `dominoNullity = 4`.
  53
  54## The result (theorems axiom-clean and true; their SCOPE is conditional)
  55
  56* `multiplicity_eq_rank_one` / `multiplicity_eq_rank_two`: multiplicity = rank at `k ∈ {1,2}`.
  57  True, but the multiplicity side inherits `cellLedger`'s one-generator-per-face choice, so
  58  this is a consistency check of the rank reading, not an independent derivation of it.
  59* `multiplicity_ne_nullity_two`: `recognitionMultiplicity 2 = 2 ≠ 4 = dominoNullity`. Under
  60  the rank reading, multiplicity diverges from nullity: the two readings are mutually
  61  exclusive. (The mirror `cellLedgerNullity` construction produces the symmetric witness for
  62  the other branch, so this witness does not adjudicate between them.)
  63* `bekenstein_selector_derived`: `selector_multiplicity_is_closure_rank 1` holds. NOTE: the
  64  proof term closes `1 = closureRank` directly and does not consume the ledger construction;
  65  see the retag header. The name is kept for downstream stability
  66  (`RecordCostAsymmetry.bekenstein_selector_from_asymmetry` re-exports it).
  67* `coefficient_is_one_quarter_derived`: the pixel/sector ratio is `1/4` GIVEN the rank
  68  reading. CONDITIONAL on the `cellLedger` modeling choice.
  69
  70## Honest scope (post-audit)
  71
  72This is a **non-standard entropy assignment**, and we state it as such. Standard black-hole
  73microstate counting (Strominger-Vafa, LQG) sets `S = log(microstates)`, and here the
  74microstates ARE the nullity (3 free bits at one face), which would give `κ = 4/3`, NOT `1/4`.
  75RS reads entropy as attaching to the posted DISTINCTION (rank) because `ledgerCost` counts
  76performed distinctions. But the audit established that T-1 alone does not fix how many
  77distinctions a closed plaquette posts: `cellLedger`'s one-per-face is a CHOICE (the mirror
  78three-per-face ledger is equally consistent). So the `1/4` here is CONDITIONAL on that
  79choice. The open, non-circular route to forcing rank is the extensivity/gluing-invariance
  80argument (demanding an area law exist forces the extensive branch, and only rank is
  81extensive), which lives in the quad module — not here.
  82-/
  83
  84namespace IndisputableMonolith
  85namespace Holography
  86namespace RecognitionMultiplicity
  87
  88open PixelGluedPlaquette
  89
  90/-! ## 1. Recognition multiplicity from the ledger floor (independent of any closure map) -/
  91
  92/-- The **defect ledger of a `k`-face cell**: `k` distinct primitive posted distinctions,
  93one per D=3-forced unit face, each of multiplicity one. This is a MODELING CHOICE, not a
  94T-1 consequence (audit `holo_mult_fable_20260702`): T-1 says a closed recognition loop
  95posts distinctions but does not fix HOW MANY per face. One-per-face encodes the rank
  96reading; a mirror three-per-face ledger (one per free bit) would encode the nullity
  97reading and is equally T-1-consistent. The choice made here is what downstream theorems
  98are conditional on. It knows only the face count — nothing about the closure map. -/
  99noncomputable def cellLedger : ℕ → Foundation.RecognitionLedgerFloor.DefectLedger ℕ
 100  | 0 => 0
 101  | (k+1) => cellLedger k + Finsupp.single k 1
 102
 103/-- The **recognition multiplicity** of a `k`-face cell: its recognition ledger cost under
 104unit weight (`Foundation.RecognitionLedgerFloor.ledgerCost`). By construction this is the
 105count of posted distinctions, grounded in the T-1/T0 floor, NOT the closure map's rank. -/
 106noncomputable def recognitionMultiplicity (k : ℕ) : ℝ :=
 107  Foundation.RecognitionLedgerFloor.ledgerCost (fun _ => (1 : ℝ)) (cellLedger k)
 108
 109/-- **The ledger multiplicity is the face count `k`.** Proved from the free ledger floor
 110(`ledgerCost_add` + `ledgerCost_single`, i.e. `two_independent_same_defects` generalized),
 111with no reference whatsoever to the closure map. -/
 112theorem recognitionMultiplicity_eq (k : ℕ) : recognitionMultiplicity k = (k : ℝ) := by
 113  induction k with
 114  | zero => simp [recognitionMultiplicity, cellLedger]
 115  | succ n ih =>
 116      simp only [recognitionMultiplicity, cellLedger] at *
 117      rw [Foundation.RecognitionLedgerFloor.ledgerCost_add,
 118          Foundation.RecognitionLedgerFloor.ledgerCost_single, ih]
 119      push_cast
 120      ring
 121
 122/-! ## 2. The two-face divergence witness: rank 2 ≠ nullity 4 (from the enumerated map) -/
 123
 124/-- Left-face closure of the two-face domino (`0-1-4-3` even parity). -/
 125def dominoLeftClosed (c : DominoCfg) : Bool :=
 126  ! (vbit c 0 ^^ vbit c 1 ^^ vbit c 4 ^^ vbit c 3)
 127
 128/-- Right-face closure of the two-face domino (`1-2-5-4` even parity). -/
 129def dominoRightClosed (c : DominoCfg) : Bool :=
 130  ! (vbit c 1 ^^ vbit c 2 ^^ vbit c 5 ^^ vbit c 4)
 131
 132/-- The **local closure map** of the two-face domino: the pair of the two face parities.
 133Its image is all of `Bool × Bool` (the two constraints are independent), so its rank is 2. -/
 134def dominoLocalMap (c : DominoCfg) : Bool × Bool := (dominoLeftClosed c, dominoRightClosed c)
 135
 136/-- **Rank of the two-face domino** = `Nat.log2` of the image cardinality of `dominoLocalMap`
 137(`|image| = 4 = 2²`, both parities independently achievable). Read off the actual map. -/
 138def dominoRank : ℕ := Nat.log2 (Finset.univ.image dominoLocalMap).card
 139
 140/-- **Nullity of the two-face domino** = `Nat.log2` of the kernel cardinality (both faces
 141closed: `16 = 2⁴` configs), the free/undistinguished bits. -/
 142def dominoNullity : ℕ :=
 143  Nat.log2 (Finset.univ.filter (fun c => dominoLocalMap c = (true, true))).card
 144
 145theorem dominoRank_eq_two : dominoRank = 2 := by decide
 146
 147theorem dominoNullity_eq_four : dominoNullity = 4 := by decide
 148
 149/-- **First-isomorphism check of the actual two-face map.** `|image| · |kernel| = |domain|`
 150(`4 · 16 = 64`), pinning rank 2 and nullity 4 without any hand-typed subtraction. -/
 151theorem domino_image_times_kernel :
 152    (Finset.univ.image dominoLocalMap).card
 153      * (Finset.univ.filter (fun c => dominoLocalMap c = (true, true))).card
 154      = (Finset.univ : Finset DominoCfg).card := by decide
 155
 156/-! ## 3. The bridge: multiplicity = rank ≠ nullity -/
 157
 158/-- **Bridge at one face (the selector's target).** The ledger multiplicity of one plaquette
 159equals the closure rank. Computed by two disjoint routes: `recognitionMultiplicity 1` from
 160the ledger floor, `CoefficientBridge.closureRank` from the image of `PixelLocal.closed`. -/
 161theorem multiplicity_eq_rank_one :
 162    recognitionMultiplicity 1 = (CoefficientBridge.closureRank : ℝ) := by
 163  rw [recognitionMultiplicity_eq, CoefficientBridge.closureRank_eq_one]
 164
 165/-- **Bridge at two faces (the divergence witness).** `recognitionMultiplicity 2 = 2 = dominoRank`
 166— the ledger multiplicity tracks the rank even where rank and nullity have split apart. -/
 167theorem multiplicity_eq_rank_two :
 168    recognitionMultiplicity 2 = (dominoRank : ℝ) := by
 169  rw [recognitionMultiplicity_eq, dominoRank_eq_two]
 170
 171/-- **The divergence witness — scoped.** `recognitionMultiplicity 2 = 2`, but the nullity is
 172`4`, so `2 ≠ 4`: UNDER the rank reading encoded in `cellLedger`, multiplicity diverges from
 173nullity, so the two readings are mutually exclusive. It does NOT rule out the `κ = 4/3`
 174branch on its own: the mirror `cellLedgerNullity` (three generators per face) yields the
 175symmetric witness `6 ≠ 2` for the other branch. What it does establish non-trivially: a
 176dependent gluing would have broken `multiplicity = rank` even under this reading. -/
 177theorem multiplicity_ne_nullity_two :
 178    recognitionMultiplicity 2 ≠ (dominoNullity : ℝ) := by
 179  rw [recognitionMultiplicity_eq, dominoNullity_eq_four]; norm_num
 180
 181/-! ## 4. The payoff, retagged: the Bekenstein 1/4 selector, CONDITIONAL on the rank reading -/
 182
 183/-- **CONDITIONAL (modeling choice): the Bekenstein selector.**
 184`selector_multiplicity_is_closure_rank 1` holds. AUDIT NOTE (`holo_mult_fable_20260702`):
 185the proof term below closes `1 = closureRank` directly and never consumes
 186`recognitionMultiplicity` or `cellLedger` — the ledger construction is not load-bearing
 187here, so this theorem does not DERIVE the selector from T-1; it instantiates the rank
 188reading. The name `_derived` is kept only for downstream stability
 189(`RecordCostAsymmetry` re-exports it). GAP 1's selector remains open pending the
 190extensivity/gluing-invariance forcing in the quad module. -/
 191theorem bekenstein_selector_derived :
 192    CoefficientBridge.selector_multiplicity_is_closure_rank 1 := by
 193  unfold CoefficientBridge.selector_multiplicity_is_closure_rank
 194  rw [CoefficientBridge.closureRank_eq_one]
 195
 196/-- **CONDITIONAL (modeling choice): the Bekenstein-Hawking coefficient `1/4`.** The
 197pixel-to-sector ratio is exactly `1/4` GIVEN the rank reading of the selector. Conditional
 198on the `cellLedger` one-generator-per-face choice, NOT forced by T-1 alone (audit
 199`holo_mult_fable_20260702`). The name `_derived` is kept for downstream stability. -/
 200theorem coefficient_is_one_quarter_derived :
 201    (1 : ℚ) / (PixelLocal.admissibleSectors.card : ℚ) = 1 / 4 :=
 202  CoefficientBridge.bekenstein_of_selector 1 bekenstein_selector_derived
 203
 204/-! ## 5. Bundled target + certificate handle for the holography loop -/
 205
 206/-- **The consistency-check bundle** (retagged; see header). Multiplicity = rank at one and
 207two faces, multiplicity ≠ nullity at two faces (the scoped divergence witness), the selector
 208instantiated under the rank reading, and the conditional coefficient `1/4`. -/
 209def target_recognition_multiplicity : Prop :=
 210  recognitionMultiplicity 1 = (CoefficientBridge.closureRank : ℝ)
 211  ∧ recognitionMultiplicity 2 = (dominoRank : ℝ)
 212  ∧ recognitionMultiplicity 2 ≠ (dominoNullity : ℝ)
 213  ∧ (Finset.univ.image dominoLocalMap).card
 214      * (Finset.univ.filter (fun c => dominoLocalMap c = (true, true))).card
 215      = (Finset.univ : Finset DominoCfg).card
 216  ∧ CoefficientBridge.selector_multiplicity_is_closure_rank 1
 217  ∧ (1 : ℚ) / (PixelLocal.admissibleSectors.card : ℚ) = 1 / 4
 218
 219theorem target_recognition_multiplicity_holds : target_recognition_multiplicity :=
 220  ⟨multiplicity_eq_rank_one, multiplicity_eq_rank_two, multiplicity_ne_nullity_two,
 221   domino_image_times_kernel, bekenstein_selector_derived, coefficient_is_one_quarter_derived⟩
 222
 223/-- Verify-target certificate handle for the holography loop (`#print axioms`-gated). -/
 224theorem recognitionMultiplicityCert : target_recognition_multiplicity :=
 225  target_recognition_multiplicity_holds
 226
 227end RecognitionMultiplicity
 228end Holography
 229end IndisputableMonolith
 230