Foundation Primitive Recognition Calculus Delta Probability Prob Le One

The probability bound

Probability, in its oldest and most concrete form, is a ratio of counts. If a space has N+1 equally likely outcomes and an event selects k of them, the probability of that event is k divided by N+1. The Recognition Science framework, in its ledger (a discrete record of events) models this as a counting ratio over a finite set of alternatives, and its machine-checked library of formal theorems proves the bound that follows immediately from the definition: the probability of any event is at most 1.

The theorem called prob_le_one states this exactly. For any finite space of N+1 alternatives and any event E defined on it, the probability prob E satisfies prob E ≤ 1. The proof is a direct comparison of counts: the number of outcomes satisfying E cannot exceed the total number of outcomes, so the ratio cannot exceed 1. The same library also proves the companion facts that the impossible event has probability 0, the certain event has probability 1, and every probability is nonnegative, together with monotonicity (a larger event has larger probability) and additivity for disjoint events.

These results belong to a foundational layer of the framework, before any of its larger claims about cost functions, the golden ratio, or spatial dimensions. They establish that the native notion of probability is a well-behaved classical one: rational, bounded, monotone, and additive. The headline theorem delta_probability_headline packages all of these properties into a single statement, which the library checks as one unit.

What prob_le_one does not claim is any connection to the framework's deeper theorems. It does not assert that probabilities arise from the cost function J, nor that they constrain the golden ratio or the forcing chain. It is a local, self-contained fact about finite counting. It also does not claim anything about infinite probability spaces, continuous distributions, or measure theory; those lie outside the finite setting of this declaration.

/-- Finite distinction probabilities are bounded by one. -/
theorem prob_le_one {N : ℕ} (E : Event N) : prob E ≤ 1 := by
  classical
  unfold prob count
  have hcard : (Finset.univ.filter fun i : Fin (N + 1) => E i).card ≤ (Finset.univ : Finset (Fin (N + 1))).card :=
    Finset.card_filter_le _ _
  have hcard' : (Finset.univ.filter fun i : Fin (N + 1) => E i).card ≤ N + 1 := by
    simpa using hcard
  have hden : (0 : ℚ) < (N + 1 : ℚ) := by positivity
  have hcast : (((Finset.univ.filter fun i : Fin (N + 1) => E i).card : ℚ) ≤ ((N + 1 : ℕ) : ℚ)) := by
    exact_mod_cast hcard'
  rw [div_le_iff₀ hden]
  simpa using hcast

/-- The impossible event has probability zero. -/
theorem prob_empty (N : ℕ) : prob (N := N) (fun _ => False) = 0 := by
  classical
  simp [prob, count_empty]

/-- The certain event has probability one. -/
theorem prob_univ (N : ℕ) : prob (N := N) (fun _ => True) = 1 := by
  classical
  have h : ((N + 1 : ℚ) ≠ 0) := by positivity
  rw [prob, count_univ]
  rw [show (((N + 1 : ℕ) : ℚ)) = (N + 1 : ℚ) by norm_num]
  exact div_self h

/-- Finite distinction probabilities are nonnegative. -/
theorem prob_nonneg {N : ℕ} (E : Event N) : 0 ≤ prob E := by
  classical
  unfold prob
  positivity

/-- **Delta-native probability headline.** Probability at the native finite layer
is rational counting over finite distinction alternatives: impossible event zero,
certain event one, and every event has probability in `[0,1]`. -/
theorem delta_probability_headline (N : ℕ) :
    prob (N := N) (fun _ => False) = 0
      ∧ prob (N := N) (fun _ => True) = 1
      ∧ (∀ E : Event N, 0 ≤ prob E ∧ prob E ≤ 1)
      ∧ (∀ E F : Event N, (∀ i, E i → F i) → prob E ≤ prob F)
      ∧ (∀ E F : Event N, (∀ i, ¬ (E i ∧ F i)) →
          prob (fun i => E i ∨ F i) = prob E + prob F) :=
  ⟨prob_empty N, prob_univ N, fun E => ⟨prob_nonneg E, prob_le_one E⟩,
    fun _ _ h => prob_mono h, fun _ _ h => prob_disjoint_or h⟩

What this page does not claim

This theorem does not connect probability to the cost function J or to the golden ratio forcing chain. This theorem does not apply to infinite probability spaces, continuous distributions, or measure theory. This theorem does not assert that probabilities are derived from recognition events; it only defines them as counting ratios.

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/Foundation/PrimitiveRecognitionCalculus/DeltaProbability.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: