IndisputableMonolith.Holography.RecognitionEventCapacity

   1import IndisputableMonolith.Foundation.MeasureForcing
   2
   3/-!
   4# RecognitionEventCapacity: the access bound as forced-measure entropy per event
   5
   6The deflation test (`ThetaAccessDeflation`) killed the naive "eight states per site"
   7quotient: the physical per-carrier content is a continuum, so the orbit count is not the
   8physical access bound. The hypothesis this module executes (Jon, 2026-06-26): the right
   9PHYSICAL access bound is FORCED-MEASUREMENT OUTCOME QUANTIZATION. A single recognition
  10event resolves into discrete `φ^{-n}`-weighted outcomes (the T9 forced measure, proved in
  11`Foundation.MeasureForcing`: `probMass n = (1-φ^{-1})·φ^{-n}`, normalized, mean depth `φ`,
  12partition `φ^2`). The access law is then NOT an orbit count but the INFORMATION CONTENT of
  13one recognition event, the Shannon entropy of the forced measure, additive over events.
  14
  15The central number is forced, with no free parameter and no arbitrary alphabet:
  16
  17* `forcedEntropy = (φ + 2)·log φ` nats (≈ 1.741): information per recognition event.
  18* `effectiveOutcomes = exp(forcedEntropy) = φ^{φ+2}` (≈ 5.70): the EFFECTIVE outcome count
  19  (perplexity) per event. Replaces the spurious `8`, and is genuinely different from 8.
  20* `bitsPerEvent = (φ+2)·log₂ φ` (≈ 2.51 bits) (`bitsPerEvent_eq`).
  21* `eventAccess k = k·forcedEntropy`: the rebuilt access rate, scaled over `k` events. The
  22  old `|R|·log₂|α|` bound is the special case where each event is a uniform `α`-symbol.
  23
  24CRITICAL FRAMING (panel, 2026-06-26), do not overclaim: entropy bounds AVERAGE INFORMATION
  25/ CHANNEL CAPACITY, NOT zero-error distinguishability. `ThetaAccessDeflation.sumSig_surjective`
  26proves a forced readout can hard-distinguish INFINITELY many states, so `effectiveOutcomes`
  27is an EFFECTIVE (perplexity) count, NOT a hard cardinality ceiling, and the rebuilt access
  28law is a mutual-information / channel-capacity statement, not an injection bound. That is
  29why it supersedes the deflated orbit count: the orbit count was a false hard ceiling; this
  30is the true average rate.
  31
  32Status. THEOREM (axiom-clean), grounded in proved `MeasureForcing` decls: the per-term
  33log-weight law (`neglog_probMass`), the closed form `probMass n = (φ^{n+2})⁻¹`, the
  34effective outcome count `φ^{φ+2}`, the bit-rate identity, and additivity. The keystone
  35`forcedEntropy_eq` (the Shannon-tsum value) is now PROVED (closed 2026-06-26, axiom-clean:
  36`[propext, Classical.choice, Quot.sound]`): the standard entropy-of-geometric computation,
  37done from `meanRung_eq_phi` and `probMass_tsum_one` via the additive-tsum split. MODEL: identifying
  38"information per recognition event" with the entropy of the forced instance-weighting
  39(cost-sufficiency: the forced measure is the only intrinsic weighting). OPEN, documented
  40(NOT a faked Prop): the Born bridge, that this entropy is literally the entropy of a
  41forced-MEASUREMENT outcome distribution (the bridge from the sub-Gaussian L² seed in
  42`MeasureForcing` to recognition Hilbert space). The elliptic `U(1)` phase sector
  43(`Recognition_Cost_As_Symplectic_Action`) is where the residual outcome phase lives. Do
  44NOT assert the Born rule as an identity (a prior panel killed "phase projection = Born").
  45
  46Anti-vacuity: `forcedEntropy` is the genuine Shannon tsum `-∑ P(n) log P(n)` of the proved
  47forced measure, not a chosen constant; its value `(φ+2)log φ` is to be computed from
  48`meanRung_eq_phi` and normalization, never posited. Every consequence below is proved
  49modulo that one keystone.
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Holography
  54namespace RecognitionEventCapacity
  55
  56open IndisputableMonolith.Foundation.MeasureForcing
  57open scoped BigOperators
  58
  59noncomputable section
  60
  61/-- The Shannon entropy (nats) of the forced measure `P(n) = (1-ρ)ρⁿ`: information per
  62recognition event. -/
  63noncomputable def forcedEntropy : ℝ := ∑' n : ℕ, probMass n * (-(Real.log (probMass n)))
  64
  65/-- `1 - ρ = ρ²` (the golden identity `1 - φ⁻¹ = φ⁻²`). -/
  66theorem one_sub_rho_eq_sq : 1 - rho = rho ^ 2 := by
  67  rw [one_sub_rho]; unfold rho; rw [div_pow, one_pow]
  68
  69/-- Closed form: `P(n) = (φ^{n+2})⁻¹`. The forced measure is a pure inverse power of φ. -/
  70theorem probMass_eq_inv_pow (n : ℕ) : probMass n = (Constants.phi ^ (n + 2))⁻¹ := by
  71  unfold probMass
  72  rw [one_sub_rho]
  73  unfold rho
  74  rw [div_pow, one_pow, pow_add]
  75  have hphi : Constants.phi ≠ 0 := ne_of_gt Constants.phi_pos
  76  field_simp
  77
  78/-- Per-term log-weight law: `-log P(n) = (n+2)·log φ`, linear in recognition depth. -/
  79theorem neglog_probMass (n : ℕ) :
  80    -(Real.log (probMass n)) = ((n : ℝ) + 2) * Real.log Constants.phi := by
  81  rw [probMass_eq_inv_pow, Real.log_inv, Real.log_pow]
  82  push_cast
  83  ring
  84
  85/-- **The per-event entropy (keystone).** A single recognition event carries `(φ+2)·log φ`
  86nats, the Shannon entropy of the forced measure, computed from its mean depth `φ`
  87(`meanRung_eq_phi`) and normalization (`probMass_tsum_one`).
  88
  89PROVED (2026-06-26, axiom-clean). Strategy realized below:
  90rewrite each summand by `neglog_probMass` to `probMass n * (((n:ℝ)+2) * log φ)`, then via
  91`tsum_congr` to `log φ * ((n:ℝ) * probMass n) + (2 * log φ) * probMass n`; split with the
  92additive tsum lemma using `Summable (fun n => (n:ℝ) * probMass n)` (from
  93`summable_pow_mul_geometric_of_norm_lt_one 1` times `(1-ρ)`) and `Summable probMass` (from
  94`summable_geometric_of_lt_one` times `(1-ρ)`); pull constants with `tsum_mul_left`; close
  95with `meanRung_eq_phi` (`∑ n·P(n) = φ`) and `probMass_tsum_one` (`∑ P(n) = 1`), then `ring`
  96gives `(φ+2)·log φ`. -/
  97theorem forcedEntropy_eq :
  98    forcedEntropy = (Constants.phi + 2) * Real.log Constants.phi := by
  99  have hnorm : ‖rho‖ < 1 := by
 100    rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one
 101  have hsP : Summable probMass := by
 102    have hg : Summable (fun n : ℕ => rho ^ n) :=
 103      summable_geometric_of_lt_one rho_nonneg rho_lt_one
 104    have := hg.mul_left (1 - rho)
 105    simpa [probMass] using this
 106  have hsNP : Summable (fun n : ℕ => (n : ℝ) * probMass n) := by
 107    have h0 : Summable (fun n : ℕ => (n : ℝ) ^ 1 * rho ^ n) :=
 108      summable_pow_mul_geometric_of_norm_lt_one 1 hnorm
 109    have h1 := h0.mul_left (1 - rho)
 110    have heq : (fun n : ℕ => (n : ℝ) * probMass n)
 111        = fun n : ℕ => (1 - rho) * ((n : ℝ) ^ 1 * rho ^ n) := by
 112      funext n; unfold probMass; ring
 113    rw [heq]; exact h1
 114  have hsum2P : Summable (fun n : ℕ => (2 : ℝ) * probMass n) := hsP.mul_left 2
 115  have hmean : (∑' n : ℕ, (n : ℝ) * probMass n) = Constants.phi := by
 116    have h := meanRung_eq_phi; unfold meanRung at h; exact h
 117  have h2sum : (∑' n : ℕ, (2 : ℝ) * probMass n) = 2 := by
 118    rw [tsum_mul_left, probMass_tsum_one]; ring
 119  unfold forcedEntropy
 120  have hstep : (∑' n : ℕ, probMass n * (-(Real.log (probMass n))))
 121      = Real.log Constants.phi
 122          * ((∑' n : ℕ, (n : ℝ) * probMass n) + (∑' n : ℕ, (2 : ℝ) * probMass n)) := by
 123    rw [← hsNP.tsum_add hsum2P, ← tsum_mul_left]
 124    exact tsum_congr (fun n => by rw [neglog_probMass]; ring)
 125  rw [hstep, hmean, h2sum]; ring
 126
 127/-- The effective outcome count per recognition event: the perplexity `exp H` of the
 128forced measure. EFFECTIVE (average), not a hard distinguishability ceiling (the hard count
 129is infinite, `ThetaAccessDeflation.sumSig_surjective`). -/
 130noncomputable def effectiveOutcomes : ℝ := Real.exp forcedEntropy
 131
 132/-- **The forced effective outcome count is `φ^{φ+2}`** (≈ 5.70), replacing the spurious
 133`8` of the orbit count. A perplexity / channel-capacity quantity, not a hard ceiling.
 134Proved modulo the entropy keystone. -/
 135theorem effectiveOutcomes_eq :
 136    effectiveOutcomes = Constants.phi ^ (Constants.phi + 2) := by
 137  unfold effectiveOutcomes
 138  rw [forcedEntropy_eq,
 139      show (Constants.phi + 2) * Real.log Constants.phi
 140        = Real.log Constants.phi * (Constants.phi + 2) from mul_comm _ _,
 141      ← Real.rpow_def_of_pos Constants.phi_pos]
 142
 143/-- Bits of information per recognition event. -/
 144noncomputable def bitsPerEvent : ℝ := forcedEntropy / Real.log 2
 145
 146/-- **The forced per-event bit rate is `(φ+2)·log₂ φ`** (≈ 2.51 bits), the physically
 147forced access rate replacing the artifact `3 = log₂ 8`. Proved modulo the entropy
 148keystone. -/
 149theorem bitsPerEvent_eq :
 150    bitsPerEvent = (Constants.phi + 2) * Real.logb 2 Constants.phi := by
 151  unfold bitsPerEvent Real.logb
 152  rw [forcedEntropy_eq]
 153  ring
 154
 155/-- The information accessible across `k` recognition events, at the forced per-event
 156rate. MODEL definition: this is `k·H` by construction. The SUBSTANTIVE additivity (that
 157the entropy of `k` INDEPENDENT events equals `k·H`, via the product measure and the
 158forced-measure factorization `Factorizes`) is the open next target, NOT this definitional
 159linearity. -/
 160noncomputable def eventAccess (k : ℕ) : ℝ := (k : ℝ) * forcedEntropy
 161
 162/-- Definitional linearity of `eventAccess` (MODEL). This is true by the definition
 163`eventAccess k = k·H`; it is NOT the substantive product-measure additivity theorem (which
 164is open). Kept only to record the scaling shape. -/
 165theorem eventAccess_additive (j k : ℕ) :
 166    eventAccess (j + k) = eventAccess j + eventAccess k := by
 167  unfold eventAccess; push_cast; ring
 168
 169/-- **Recognition-event capacity certificate.** The per-event information is the forced
 170measure's entropy `(φ+2)log φ`; the effective outcome count is `φ^{φ+2}`; the bit rate is
 171`(φ+2)log₂φ`; access is additive over events. -/
 172structure EventCapacityCert : Prop where
 173  entropy_value : forcedEntropy = (Constants.phi + 2) * Real.log Constants.phi
 174  outcomes_value : effectiveOutcomes = Constants.phi ^ (Constants.phi + 2)
 175  bits_value : bitsPerEvent = (Constants.phi + 2) * Real.logb 2 Constants.phi
 176  additive : ∀ j k : ℕ, eventAccess (j + k) = eventAccess j + eventAccess k
 177
 178theorem eventCapacityCert : EventCapacityCert where
 179  entropy_value := forcedEntropy_eq
 180  outcomes_value := effectiveOutcomes_eq
 181  bits_value := bitsPerEvent_eq
 182  additive := eventAccess_additive
 183
 184end
 185
 186end RecognitionEventCapacity
 187end Holography
 188end IndisputableMonolith
 189