Holography Recognition Event Capacity Neglog Prob Mass

The per-event information law

The declaration neglog_probMass establishes a precise, machine-checked relationship between the probability of a recognition outcome and its information content. In plain terms, it states that the negative logarithm of the probability of the n-th outcome equals (n+2) times the natural logarithm of the golden ratio φ. Since the golden ratio is approximately 1.618, this means the information carried by an outcome grows linearly with its depth n in the recognition sequence. The first outcome (n=0) carries about 0.96 nats, the second about 1.57 nats, and so on.

This law is not an isolated formula. It is the per-term building block of a larger result: the total information per recognition event, computed as the Shannon entropy of the forced probability distribution, equals (φ+2)·log φ nats, approximately 1.741 nats. Converting to bits, this is about 2.51 bits per event. The framework's machine-checked library of formal theorems proves this value follows from the golden ratio itself, with no free parameter and no arbitrary alphabet size. The effective number of distinguishable outcomes per event, the perplexity exp(1.741), is about 5.70, a number that replaces an earlier, spurious count of eight states per site.

What the declaration does not claim is as important as what it proves. The 2.51 bits is an average information rate, a channel-capacity quantity, not a hard limit on how many states a recognition system can distinguish. A separate theorem in the same library shows a forced readout can hard-distinguish infinitely many states. The effective outcome count of 5.70 is therefore a measure of typical information content, not a cardinality ceiling. The framework also does not claim that this entropy is literally the entropy of a quantum measurement outcome distribution; that bridge, the Born bridge, remains an open target. The declaration only establishes the information content of the abstract recognition event itself.

The practical consequence is that the framework now has a principled, forced answer to the question of how much information a single recognition event can carry. Earlier attempts based on counting discrete states failed because the physical content is a continuum. The entropy-based approach sidesteps that failure by measuring average information rather than counting states. This number, 2.51 bits per event, now serves as the foundation for the framework's account of access rates and information capacity across recognition sequences.

/-- Per-term log-weight law: `-log P(n) = (n+2)·log φ`, linear in recognition depth. -/
theorem neglog_probMass (n : ℕ) :
    -(Real.log (probMass n)) = ((n : ℝ) + 2) * Real.log Constants.phi := by
  rw [probMass_eq_inv_pow, Real.log_inv, Real.log_pow]
  push_cast
  ring

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

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

/-- **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 2.51 bits per event is not a hard ceiling on distinguishability; a forced readout can distinguish infinitely many states. The framework does not claim this entropy is the entropy of a quantum measurement outcome distribution. The declaration does not prove that the entropy of multiple independent events is additive; that remains an open target.

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: