Encyclopedia Holography Holography Recognition Event Capacity Forced Entropy Eq

ARTICLE 4 claims 4 theorems

Holography Recognition Event Capacity Forced Entropy Eq

A single recognition event carries a fixed amount of information, about 2.51 bits, and the framework proves this number is forced by its own structure.

Verify this page

The forced entropy

In information theory, entropy measures the average amount of surprise, or information, in a random outcome. The forcedEntropy_eq declaration in the Recognition Science framework's machine-checked library of formal theorems computes this quantity for a specific probability distribution. The distribution, called the forced measure, assigns decreasing weights to deeper levels of a recognition event. The theorem states that the Shannon entropy of this distribution is exactly (φ + 2) · log φ, where φ is the golden ratio, approximately 1.618. This evaluates to about 1.741 nats, or about 2.51 bits, per event.

The number is not chosen or fitted. The framework derives it from the structure of the forced measure itself. The measure assigns probability φ⁻² to the shallowest level, φ⁻³ to the next, and so on. The theorem forcedEntropy_eq computes the entropy of this geometric distribution using its mean depth and normalization. The result is a closed form in terms of φ, with no free parameters. The related theorem effectiveOutcomes_eq shows that the effective number of outcomes per event, the perplexity, is φ^(φ+2), about 5.70. This replaces an earlier estimate of eight, which came from counting discrete states.

Within the framework, this per-event entropy acts as a capacity certificate. The structure EventCapacityCert packages the entropy value, the effective outcome count, the bit rate, and additivity over events into one theorem. This means the information accessible across multiple recognition events scales linearly with the number of events, at the forced per-event rate. The framework describes this as the physical access bound for a recognition event, the average information content rather than a hard ceiling on distinguishable states.

The theorem does not claim that a recognition event can only produce about 5.70 distinct outcomes. The framework explicitly states that a forced readout can distinguish infinitely many states. The effective outcome count is an average, a perplexity measure, not a cardinality limit. The theorem also does not claim that this entropy is the entropy of a quantum measurement outcome distribution. That bridge, called the Born bridge, remains open. The framework models the entropy as the information content of the forced instance-weighting, but it does not assert the Born rule as an identity.

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
THEOREM eventAccess_additive · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
eventAccess_additive · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:162 
/-- Definitional linearity of `eventAccess` (MODEL). This is true by the definition
`eventAccess k = k·H`; it is NOT the substantive product-measure additivity theorem (which
is open). Kept only to record the scaling shape. -/
theorem eventAccess_additive (j k : ℕ) :
    eventAccess (j + k) = eventAccess j + eventAccess k := by
  unfold eventAccess; push_cast; ring

What this page does not claim

A recognition event can only produce about 5.70 distinct outcomes; the hard distinguishability count is infinite. The forced entropy is the entropy of a forced-measurement outcome distribution; the Born bridge is open. The additivity of eventAccess is a substantive product-measure theorem; it is true by definition.

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