Foundation Primitive Recognition Calculus Delta Probability Count Disjoint Or

Counting without double counting

In ordinary counting, if you have a bag of red marbles and a bag of blue marbles, and no marble is both red and blue, then the total number of marbles in either bag is the red count plus the blue count. The declaration count_disjoint_or states this same principle for finite events in the Recognition Science framework: if two events cannot both occur at the same point, then the count of points where either event occurs equals the sum of the two individual counts. The statement is proved in the framework's machine-checked library of formal theorems, meaning it holds by construction from the definitions, not by assumption.

The framework builds its probability from this counting. A finite event is a property that each point in a finite space either has or lacks. The count of an event is the number of points satisfying it, and the probability is that count divided by the total number of points. Because counts add for disjoint events, probabilities add the same way: the probability that either of two mutually exclusive events occurs is the sum of their separate probabilities. This additivity is the foundation of the framework's ledger, a discrete record of which events happened at which points, and it is what lets the framework treat probability as rational counting rather than as a separate primitive notion.

The theorem also fits into a small family of results that together describe how counting behaves. The impossible event has count zero, the certain event has count equal to the whole space, counts are monotone under event inclusion, and disjoint events add. The declaration count_disjoint_or is the additivity piece: it is what makes the framework's probability behave like ordinary probability, where the chance of one outcome or another is the sum of the chances when the outcomes exclude each other.

What the declaration does not do is equally important. It does not define probability itself; it only states a property that counts satisfy. It does not say anything about events that overlap, where the same point satisfies both events, because the additivity rule fails there without a correction term. It also does not introduce any new physical content: it is a theorem about finite sets and counting, not a claim about the physical world. The framework's larger claims about recognition and cost build on this counting, but this particular declaration is a piece of mathematics, not physics.

/-- Disjoint finite events have additive counts. -/
theorem count_disjoint_or {N : ℕ} {E F : Event N}
    (hdisj : ∀ i, ¬ (E i ∧ F i)) :
    count (fun i => E i ∨ F i) = count E + count F := by
  classical
  have hunion : eventFinset (fun i : Fin (N + 1) => E i ∨ F i) = eventFinset E ∪ eventFinset F := by
    ext i
    simp [eventFinset, and_or_left]
  have hdf : Disjoint (eventFinset E) (eventFinset F) := by
    rw [Finset.disjoint_left]
    intro i hiE hiF
    simp [eventFinset] at hiE hiF
    exact hdisj i ⟨hiE, hiF⟩
  rw [count_eq_card, count_eq_card, count_eq_card, hunion]
  exact Finset.card_union_of_disjoint hdf

/-- Disjoint finite events have additive probability. -/
theorem prob_disjoint_or {N : ℕ} {E F : Event N}
    (hdisj : ∀ i, ¬ (E i ∧ F i)) :
    prob (fun i => E i ∨ F i) = prob E + prob F := by
  unfold prob
  rw [count_disjoint_or hdisj]
  rw [Nat.cast_add]
  ring

/-- **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 declaration defines probability; it only states a property of counts. This declaration covers overlapping events, where additivity requires a correction term. This declaration makes any claim about the physical world; it is a theorem about finite sets.

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: