Encyclopedia Holography Holography Recognition Event Capacity Event Capacity Cert

ARTICLE 5 claims 5 theorems

Holography Recognition Event Capacity Event Capacity Cert

A single recognition event carries about 2.51 bits of information, a number the framework forces rather than chooses.

Verify this page

The capacity certificate

In information theory, the capacity of a channel is the maximum rate at which information can be transmitted reliably. The Recognition Science declaration eventCapacityCert (a certificate, a machine-checked bundle of theorems) states the analogous capacity for one recognition event, a discrete act of distinguishing one outcome from another. The certificate assembles four proved facts: the entropy per event, the effective number of outcomes, the bit rate, and additivity over events.

The central number is the Shannon entropy of a probability distribution that the framework forces, not assumes. That distribution assigns probability P(n) = (φ^(n+2))⁻¹ to depth n, a pure inverse power of the golden ratio φ. Its entropy, computed as −Σ P(n) log P(n), is (φ+2)·log φ nats, about 1.741 nats. Converting to bits gives (φ+2)·log₂ φ, about 2.51 bits per event. The effective number of outcomes, the perplexity exp(H), is φ^(φ+2), about 5.70. These are not arbitrary choices; the framework proves them from its forced measure, with no free parameter and no chosen alphabet.

The certificate also states that access is additive: the information across k events is k times the per-event rate. This is true by definition of the access function, not by a deeper theorem about independent events. The substantive claim, that the entropy of k independent events equals k times the single-event entropy, remains an open target.

What the certificate does not claim is just as important. The effective outcome count is an average, not a hard ceiling. A forced readout can distinguish infinitely many states with zero error; the number 5.70 is a perplexity, a measure of average uncertainty, not a maximum number of distinguishable states. The certificate also does not claim that this entropy is the entropy of a quantum measurement outcome distribution. That bridge, from the framework's measure to a Born-rule probability, is open and explicitly not asserted.

In plain terms, the certificate pins down how much information a single recognition event can carry, and it replaces an earlier, spurious count of eight states per site with a forced, non-integer effective count. The reader can now see the exact value, its status as an average, and the precise limits of what the framework has proved.

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
THEOREM eventCapacityCert · IndisputableMonolith/Holography/RecognitionEventCapacity.lean
eventCapacityCert · IndisputableMonolith/Holography/RecognitionEventCapacity.lean:178 
theorem eventCapacityCert : EventCapacityCert where
  entropy_value := forcedEntropy_eq
  outcomes_value := effectiveOutcomes_eq
  bits_value := bitsPerEvent_eq
  additive := eventAccess_additive

What this page does not claim

The effective outcome count is not a hard ceiling; a forced readout can distinguish infinitely many states. The certificate does not assert the Born rule as an identity. The additivity of access is definitional, not the substantive product-measure additivity.

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