Encyclopedia Holography Holography Recognition Event Capacity Prob Mass Eq Inv Pow

ARTICLE 4 claims 4 theorems

Holography Recognition Event Capacity Prob Mass Eq Inv Pow

A single theorem in the Recognition Science library pins down the exact probability of each recognition event as a pure inverse power of the golden ratio.

Verify this page

The forced measure's closed form

In probability theory, a geometric distribution assigns probabilities to the nonnegative integers by a constant ratio: P(n) = (1 - r) r^n. The Recognition Science framework arrives at the same family from its own axioms, and the declaration probMass_eq_inv_pow states the closed form for the specific ratio the framework forces. It proves that the probability of a recognition event at depth n equals (φ^(n+2))⁻¹, where φ is the golden ratio (1 + √5)/2. Since 1 - φ⁻¹ = φ⁻², this is exactly a geometric distribution with ratio φ⁻¹, written in a way that exposes the pure inverse power of φ.

The theorem is a formal result in the framework's machine-checked library of formal theorems, not a numerical approximation. It derives from the definition of probMass and the golden identity, and it is axiom-clean: the proof uses only the standard logical axioms, with no framework-specific assumptions. The closed form matters because it makes the entire recognition-event capacity computable: the per-event entropy (φ+2)·log φ nats, the effective outcome count φ^(φ+2) ≈ 5.70, and the bit rate (φ+2)·log₂ φ ≈ 2.51 bits all follow from this single expression.

What the theorem does not claim is equally important. It does not say that a recognition event can distinguish only about 5.7 states. The framework's own deflation test proved that a forced readout can hard-distinguish infinitely many states; the effective outcome count is a perplexity, an average information measure, not a hard cardinality ceiling. The theorem also does not assert the Born rule or any bridge from this entropy to quantum measurement probabilities; that bridge remains an open target, documented as such in the library. And the additivity of access across multiple events is a definitional linearity, not yet the substantive product-measure additivity theorem.

What the closed form does give is a concrete, checkable anchor for the framework's information theory. Before this theorem, the access bound was a spurious orbit count of 8; now it is a forced geometric measure whose every consequence is proved from the golden ratio alone. A reader can verify the probability of any depth, compute the entropy, and see why the effective outcome count is not 8 but φ^(φ+2). That is the difference between a framework that gestures at structure and one that forces the result.

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 a hard distinguishability ceiling; the framework proved the hard count is infinite. The entropy of the forced measure is literally the entropy of a quantum measurement outcome distribution; the Born bridge remains open. The additivity of eventAccess is the substantive product-measure theorem; it is only definitional linearity.

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