Foundation Primitive Recognition Calculus Delta Probability Delta Probability He

Probability at the base layer

Probability, in its most basic form, is a ratio of counts. If you have a finite set of equally likely outcomes, the probability of an event is the number of outcomes that satisfy it divided by the total number of outcomes. This is the classical definition, the one that begins every introductory course. The Recognition Science framework starts from the same picture, but it makes the counting explicit and finite: the space of possibilities is a nonempty finite set, and an event is a subset of those possibilities.

The framework's machine-checked library of formal theorems proves a single result, called the delta probability headline, that bundles the essential properties of this counting definition. It states that the impossible event has probability zero, the certain event has probability one, and every event has probability between zero and one. It also proves two structural facts: if one event is contained in another, its probability is no larger, and if two events are disjoint, the probability of their union is the sum of their probabilities. These are the axioms of probability, but here they are derived as theorems from the counting definition, not assumed.

In Recognition Science, this is the base layer of a larger structure. The framework models reality as a discrete record of recognition events, and probability at this native layer is rational counting over finite distinction alternatives. The headline establishes that this counting yields a well-behaved probability theory, one that satisfies the standard laws. It is a foundation stone, not a destination.

What the headline does not claim is just as important. It does not claim that all probability is discrete, or that continuous probability can be reduced to this finite counting without further work. It does not claim that this definition is the only possible one, or that it applies to infinite spaces. It only establishes the properties of this particular finite, rational construction. The theorem is a precise statement about a specific definition, and its scope is exactly that definition.

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

/-- **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 claim that all probability is discrete or that continuous probability is reducible to it. This theorem does not claim that the counting definition is the only possible foundation for probability. This theorem does not claim anything about probability on infinite spaces.

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: