The Intelligence Bound

Definitions and units

These quantities come from the formal artifact. Habitat quality, acreage, spending and ecological scores are not substitutes for them.

Assumptions remain explicit

• formal hypothesis: μ is a probability measure; Ω and State are measurable spaces.
• formal hypothesis: observationBandwidth μ O ≠ ⊤.
• formal hypothesis: predictiveRichness μ X O τ ≤ 1; it is not established from ecosystem descriptions.
• formal hypothesis: 0 < kB and 0 < T, with nonnegative P and τ.
• scientific regime hypothesis: SatisfiesLandauerLimit μ X O τ P T kB, defined as P ≥ intelligenceCreationRate μ X O τ × ofReal(kB × T × ln 2). This physical applicability is assumed, not derived from microphysics in P0.
• empirical/modeling dependency: Justify actual X/O/μ/τ, physical regime, observation-channel quantities and mapping from available measurements; missing for generic conservation choices.
• scientific regime hypothesis when using the dissipation bridge: landauer_dissipation_bound additionally assumes an erasure rate at least the creation rate and a Landauer erasure floor. Bounded memory alone is not that bridge.

Standard foundational axioms (propext, Classical.choice, Quot.sound) are distinct from the scientific assumptions. The formal proof does not establish that the probability model or Landauer regime describes a particular ecosystem.

Exact statement and formal definitions

The statement below is quoted from the pinned public source, not reconstructed from product language.

theorem intelligence_bound {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (X : Process Ω State) (O : Process Ω State) (τ : NNReal)
    (P T kB : NNReal) (h_kB_pos : 0 < kB) (h_T_pos : 0 < T)
    (h_landauer : SatisfiesLandauerLimit μ X O τ P T kB)
    (hB : observationBandwidth μ O ≠ ⊤)
    (hRho_le_one : predictiveRichness μ X O τ ≤ 1) :
    intelligenceCreationRate μ X O τ ≤
      min (predictiveRichness μ X O τ * observationBandwidth μ O)
        (ENNReal.ofReal ((P : ℝ) / ((kB : ℝ) * (T : ℝ) * Real.log 2))) := by
  refine' le_min _ _
  · apply_rules [data_bound_lemma_conditional]
    exact ne_of_lt (lt_of_le_of_lt hRho_le_one ENNReal.one_lt_top)
  · exact thermodynamic_bound_lemma μ X O τ P T kB h_kB_pos h_T_pos h_landauer

def mutualInformation {Ω A B : Type*} [MeasurableSpace Ω] [MeasurableSpace A]
    [MeasurableSpace B] (μ : Measure Ω) (X : Ω → A) (Y : Ω → B) : ENNReal :=
  klDiv (μ.map (fun ω => (X ω, Y ω))) ((μ.map X).prod (μ.map Y))

def shannonEntropy {Ω A : Type*} [MeasurableSpace Ω] [MeasurableSpace A]
    (μ : Measure Ω) (X : Ω → A) : ENNReal :=
  mutualInformation μ X X

def Process (Ω State : Type) : Type := Ω → NNReal → State

def trajectory {Ω State : Type} (X : Process Ω State) (t : NNReal) :
    Ω → (Set.Icc (0 : NNReal) t → State) :=
  fun ω => (fun (s : Set.Icc (0 : NNReal) t) => X ω s)

def cumulativePredictiveInformation {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (X : Process Ω State)
    (O : Process Ω State) (t τ : NNReal) : ENNReal :=
  mutualInformation μ (trajectory X (t + τ)) (trajectory O t)

def intelligenceCreationRate {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (X : Process Ω State)
    (O : Process Ω State) (τ : NNReal) : ENNReal :=
  Filter.limsup (fun t : NNReal =>
    cumulativePredictiveInformation μ X O t τ / t) Filter.atTop

def observationEntropy {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (O : Process Ω State)
    (t : NNReal) : ENNReal :=
  shannonEntropy μ (trajectory O t)

def observationBandwidth {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (O : Process Ω State) : ENNReal :=
  Filter.limsup (fun t : NNReal => observationEntropy μ O t / t) Filter.atTop

def predictiveRichness {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (X : Process Ω State)
    (O : Process Ω State) (τ : NNReal) : ENNReal :=
  Filter.limsup (fun t : NNReal =>
    cumulativePredictiveInformation μ X O t τ /
    observationEntropy μ O t) Filter.atTop

def SatisfiesLandauerLimit {Ω State : Type} [MeasurableSpace Ω]
    [MeasurableSpace State] (μ : Measure Ω) (X : Process Ω State)
    (O : Process Ω State) (τ : NNReal) (P T kB : NNReal) : Prop :=
  (P : ENNReal) ≥ intelligenceCreationRate μ X O τ *
    ENNReal.ofReal ((kB : ℝ) * (T : ℝ) * Real.log 2)

Reproduction, provenance and limits

The inspected public P0 build uses leanprover/lean4:v4.24.0 and Mathlib f897ebcf72cd16f89ab4577d0c826cd14afaafc7. Its compiled dependency audit recursively checks the allowed foundational axioms. This website update inspected the source and public build receipts; it did not run a new Lean or Comparator verification.

Current Git P0 proof bodies were repaired July 27 after July 19 Zenodo spine publication. The theorem/public version DOI and current code commit are separate provenance fields; no claim of byte identity with the Zenodo archive is made.

• Exact repaired P0 formal source · Apache-2.0

  SHA-256 3f192275ee326f0fb2cf2dca3b4d97146044b3b12fca28ff18e07914fb4d9130

• Intelligence Bound Canon v10.2.0 archive · CC-BY-4.0
• Transitive P0 axiom audit · Apache-2.0

  SHA-256 1845ca3c6eb788ef0baf33226efdd769f9053d4e1ed8cac8d90e9b9f5915fdff

• Exact-source P0 public CI · Public build receipt
• Implementation and release boundary · Proprietary application documentation

Physical constraints alone do not select human values, conservation objectives or an aligned intervention policy. Those choices stay explicit in the decision workspace.