Encyclopedia Holography Holography Recognition Event Capacity

ARTICLE 4 claims 4 theorems

Holography Recognition Event Capacity

A single act of recognition in this framework carries about 2.51 bits of information, a number forced by the golden ratio and not chosen by hand.

Verify this page

Recognition event capacity

In information theory, a channel's capacity is the maximum rate at which it can reliably transmit information. Recognition Science applies this idea to a single act of recognition: one event where reality's ledger, a discrete record of events, registers a distinction. The question is how much information such an event can carry. The framework's answer is not a free choice but a consequence of its forced measure, a probability distribution over recognition depths that the framework proves is the only intrinsic weighting.

The classical result is Shannon entropy, the standard measure of average information content. For a probability distribution P over outcomes, the entropy in natural units is H = -∑ P(n) log P(n). The framework's forced measure assigns to depth n the probability P(n) = (1 - φ⁻¹)·φ⁻ⁿ, where φ is the golden ratio, about 1.618. This is a geometric distribution: deeper recognitions are exponentially less likely. Its mean depth is exactly φ, and its probabilities sum to 1.

Computing the Shannon entropy of this forced measure gives the central number: H = (φ + 2)·log φ nats, approximately 1.741 nats. Converting to bits, this is about 2.51 bits per event. The effective number of distinguishable outcomes, the perplexity exp(H), is φ^(φ+2), approximately 5.70. This replaces an earlier naive count of eight states per site, which the framework's own deflation test showed was a false hard ceiling: the actual readout can distinguish infinitely many states, so the correct quantity is an average, not a hard cardinality bound.

In Recognition Science, a framework that derives physical structure from the cost of recognition events, these numbers are proved in a machine-checked library of formal theorems. The keystone theorem forcedEntropy_eq derives the entropy value from the forced measure's mean and normalization, with no free parameters and no arbitrary alphabet. The access law for k events is simply k times the per-event entropy, additive by definition. This gives a concrete, testable claim: each recognition event in this framework carries 2.51 bits, and this is the framework's answer to how much information a single act of recognition can hold.

THEOREM probMass_eq_inv_pow · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
probMass_eq_inv_pow · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:69 
/-- Closed form: `P(n) = (φ^{n+2})⁻¹`. The forced measure is a pure inverse power of φ. -/
theorem probMass_eq_inv_pow (n : ℕ) : probMass n = (Constants.phi ^ (n + 2))⁻¹ := by
  unfold probMass
  rw [one_sub_rho]
  unfold rho
  rw [div_pow, one_pow, pow_add]
  have hphi : Constants.phi ≠ 0 := ne_of_gt Constants.phi_pos
  field_simp
THEOREM forcedEntropy_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
forcedEntropy_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:85 
/-- **The per-event entropy (keystone).** A single recognition event carries `(φ+2)·log φ`
nats, the Shannon entropy of the forced measure, computed from its mean depth `φ`
(`meanRung_eq_phi`) and normalization (`probMass_tsum_one`).

PROVED (2026-06-26, axiom-clean). Strategy realized below:
rewrite each summand by `neglog_probMass` to `probMass n * (((n:ℝ)+2) * log φ)`, then via
`tsum_congr` to `log φ * ((n:ℝ) * probMass n) + (2 * log φ) * probMass n`; split with the
additive tsum lemma using `Summable (fun n => (n:ℝ) * probMass n)` (from
`summable_pow_mul_geometric_of_norm_lt_one 1` times `(1-ρ)`) and `Summable probMass` (from
`summable_geometric_of_lt_one` times `(1-ρ)`); pull constants with `tsum_mul_left`; close
with `meanRung_eq_phi` (`∑ n·P(n) = φ`) and `probMass_tsum_one` (`∑ P(n) = 1`), then `ring`
gives `(φ+2)·log φ`. -/
theorem forcedEntropy_eq :
    forcedEntropy = (Constants.phi + 2) * Real.log Constants.phi := by
  have hnorm : ‖rho‖ < 1 := by
    rw [Real.norm_eq_abs, abs_of_pos rho_pos]; exact rho_lt_one
  have hsP : Summable probMass := by
    have hg : Summable (fun n : ℕ => rho ^ n) :=
      summable_geometric_of_lt_one rho_nonneg rho_lt_one
    have := hg.mul_left (1 - rho)
    simpa [probMass] using this
  have hsNP : Summable (fun n : ℕ => (n : ℝ) * probMass n) := by
    have h0 : Summable (fun n : ℕ => (n : ℝ) ^ 1 * rho ^ n) :=
      summable_pow_mul_geometric_of_norm_lt_one 1 hnorm
    have h1 := h0.mul_left (1 - rho)
    have heq : (fun n : ℕ => (n : ℝ) * probMass n)
        = fun n : ℕ => (1 - rho) * ((n : ℝ) ^ 1 * rho ^ n) := by
      funext n; unfold probMass; ring
    rw [heq]; exact h1
  have hsum2P : Summable (fun n : ℕ => (2 : ℝ) * probMass n) := hsP.mul_left 2
  have hmean : (∑' n : ℕ, (n : ℝ) * probMass n) = Constants.phi := by
    have h := meanRung_eq_phi; unfold meanRung at h; exact h
  have h2sum : (∑' n : ℕ, (2 : ℝ) * probMass n) = 2 := by
    rw [tsum_mul_left, probMass_tsum_one]; ring
  unfold forcedEntropy
  have hstep : (∑' n : ℕ, probMass n * (-(Real.log (probMass n))))
      = Real.log Constants.phi
          * ((∑' n : ℕ, (n : ℝ) * probMass n) + (∑' n : ℕ, (2 : ℝ) * probMass n)) := by
    rw [← hsNP.tsum_add hsum2P, ← tsum_mul_left]
    exact tsum_congr (fun n => by rw [neglog_probMass]; ring)
  rw [hstep, hmean, h2sum]; ring
THEOREM effectiveOutcomes_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
effectiveOutcomes_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:132 
/-- **The forced effective outcome count is `φ^{φ+2}`** (≈ 5.70), replacing the spurious
`8` of the orbit count. A perplexity / channel-capacity quantity, not a hard ceiling.
Proved modulo the entropy keystone. -/
theorem effectiveOutcomes_eq :
    effectiveOutcomes = Constants.phi ^ (Constants.phi + 2) := by
  unfold effectiveOutcomes
  rw [forcedEntropy_eq,
      show (Constants.phi + 2) * Real.log Constants.phi
        = Real.log Constants.phi * (Constants.phi + 2) from mul_comm _ _,
      ← Real.rpow_def_of_pos Constants.phi_pos]
THEOREM bitsPerEvent_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
bitsPerEvent_eq · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:146 
/-- **The forced per-event bit rate is `(φ+2)·log₂ φ`** (≈ 2.51 bits), the physically
forced access rate replacing the artifact `3 = log₂ 8`. Proved modulo the entropy
keystone. -/
theorem bitsPerEvent_eq :
    bitsPerEvent = (Constants.phi + 2) * Real.logb 2 Constants.phi := by
  unfold bitsPerEvent Real.logb
  rw [forcedEntropy_eq]
  ring

What this page does not claim

The effective outcome count is not a hard cardinality ceiling; a forced readout can distinguish infinitely many states. This entropy is not yet proven to be the entropy of a forced-measurement outcome distribution; the Born bridge remains open. The additivity of eventAccess is definitional linearity, not the substantive product-measure additivity theorem.

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/RecognitionEventCapacity.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND