Foundation Primitive Recognition Calculus Delta Probability Prob Nonneg

A probability that never goes negative

Probability, in the framework's most primitive setting, is simply a ratio of counts. The space under consideration is a finite set of N+1 distinct alternatives, and an event is a rule that selects some of them. The probability of an event is the number of selected alternatives divided by N+1, a rational number between zero and one. The declaration prob_nonneg establishes the lower half of that bound: for any event on any finite space, the probability is greater than or equal to zero. It is a theorem, machine-checked in the framework's library of formal theorems.

The proof is immediate once the definition is unpacked. A count is a natural number, the cardinality of a finite subset, and a natural number divided by a positive integer is never negative. The declaration does not merely assert this; it supplies a formal proof that the rational division of a nonnegative count by N+1 is nonnegative. The companion theorem prob_le_one establishes the upper bound, and together with prob_empty and prob_univ they form the four cornerstones of the delta_probability_headline, a single theorem bundling the impossible event at zero, the certain event at one, and every event in between.

This is the native probability layer of the Recognition Science framework, where a ledger, a discrete record of distinction events, is the substrate. The framework models recognition as a finite process of distinguishing alternatives, and probability here is not an axiom or a primitive; it is derived as a counting ratio. The declaration proves a property of that derived quantity, not a new physical law. It says nothing about continuous probability spaces, measure theory, or the infinite limit; those lie outside this finite, rational foundation.

What prob_nonneg does not claim is as important as what it proves. It does not assert that probabilities are strictly positive; an event selecting no alternatives has probability exactly zero. It does not assert that the framework's probabilities match empirical frequencies in the physical world; that is a separate empirical question. And it does not claim that the framework's cost function, the famous J(x) = (x + 1/x)/2 - 1, is derived from this probability layer; the probability calculus and the cost forcing chain are distinct parts of the foundation. The declaration is a small, precise, and complete statement: finite distinction probabilities are nonnegative, and that is all.

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

theorem count_eq_card {N : ℕ} (E : Event N) : count E = (eventFinset E).card := by
  rfl

/-- **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

prob_nonneg does not claim that probabilities are strictly positive; an event selecting no alternatives has probability exactly zero. The declaration does not assert that framework probabilities match empirical frequencies in the physical world. The probability calculus and the cost forcing chain are distinct parts of the foundation; prob_nonneg does not derive the cost function.

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: