Encyclopedia Holography Holography Recognition Event Capacity Effective Outcomes Eq

ARTICLE 3 claims 3 theorems

Holography Recognition Event Capacity Effective Outcomes Eq

A single recognition event carries about 5.70 effective outcomes, a number forced by the golden ratio, not chosen to fit data.

Verify this page

The effective outcome count

In information theory, the perplexity of a probability distribution is the exponential of its entropy. It answers the question: how many equally likely choices would carry the same uncertainty as this distribution? A fair coin has perplexity 2, a fair die has perplexity 6. The declaration effectiveOutcomes_eq establishes that a single recognition event, a discrete act of the universe storing a record, has perplexity φ^(φ+2), approximately 5.70. This is not a fitted constant; it follows from the framework's proved measure of how recognition instances are weighted.

The number comes from the golden ratio φ, about 1.618, which the framework derives as the unique self-similar scaling. The framework models a recognition event as resolving into outcomes whose probabilities form a geometric sequence: P(n) = (1-φ⁻¹)·φ⁻ⁿ. The Shannon entropy of this distribution, the average information per event, is (φ+2)·log φ nats, about 1.741 nats. Taking the exponential gives the effective outcome count. The declaration effectiveOutcomes_eq proves this count equals φ^(φ+2), a theorem checked in the framework's machine-checked library of formal theorems.

The number replaces an earlier guess of 8, which came from counting eight states per site. That count failed because the physical content per carrier is continuous, not discrete. The new count is an average rate, not a hard ceiling. The framework's library also proves that a forced readout can distinguish infinitely many states, so 5.70 is a measure of typical information, not a limit on distinguishability. The bit rate per event is (φ+2)·log₂ φ, about 2.51 bits.

In Recognition Science, this result is the access bound: the information a single recognition event can carry. It is additive over events by definition, though the substantive theorem that independent events combine this way remains open. The framework models this entropy as the information per event, but the bridge from this measure to quantum measurement outcomes, the Born rule, is explicitly not established. The declaration proves the arithmetic of the effective count; it does not claim that this count is a physical law.

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 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 eventAccess · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
eventAccess · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:155 
/-- The information accessible across `k` recognition events, at the forced per-event
rate. MODEL definition: this is `k·H` by construction. The SUBSTANTIVE additivity (that
the entropy of `k` INDEPENDENT events equals `k·H`, via the product measure and the
forced-measure factorization `Factorizes`) is the open next target, NOT this definitional
linearity. -/
noncomputable def eventAccess (k : ℕ) : ℝ := (k : ℝ) * forcedEntropy

What this page does not claim

The effective outcome count is not a hard cardinality ceiling on distinguishable states. The result does not establish the Born rule or any identity between entropy and quantum measurement probabilities. The additivity of eventAccess is definitional, not a proof that independent events combine this way.

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