eventWeight_pos
Nonempty finite Boolean events carry strictly positive weight under any FiniteBooleanReality. Researchers establishing the discrete-to-continuous bridge in Recognition Science cite this result when proving positivity of likelihood ratios. The proof extracts a witness index from the nonempty assumption, verifies nonnegativity of all summands via the structure axiom, isolates the positive contribution at that index, and applies single_le_sum followed by lt_of_lt_of_le.
claimLet $R$ be a finite weighted Boolean reality over $Fin n$ with strictly positive weights $w_i > 0$ for all $i$, and let $E : Fin n → Bool$ be a nonempty event. Then the event weight satisfies $0 < ∑_i 1_{E(i)} · w_i$.
background
FiniteBooleanReality n is the structure consisting of a weight function Fin n → ℝ together with the axiom that every weight is strictly positive. EventNonempty event is the proposition asserting existence of at least one index i where event i equals true. The eventWeight of an event under R is the sum over i of (if event i then weight i else 0).
proof idea
The tactic proof rcases the nonempty hypothesis to obtain witness index i₀. It unfolds eventWeight to the explicit sum, proves nonnegativity of every summand by case analysis on event i (invoking positive_weight when true), shows the i₀ term is positive by direct substitution, applies Finset.single_le_sum to bound that term below the total sum, and concludes with lt_of_lt_of_le.
why it matters in Recognition Science
This supplies the positivity step for the downstream theorem eventRatio_pos, which asserts that likelihood ratios of nonempty events remain positive. It completes the finite-Boolean side of the bridge described in the module doc-comment, ensuring weights stay positive before ratios are formed. The result aligns with the positive-weight conventions used throughout the J-cost and phi-forcing developments.
scope and limits
- Does not apply to empty events, which receive zero weight by definition.
- Does not supply an explicit numerical lower bound on the weight.
- Does not extend the statement to infinite index sets.
- Does not address continuous limits or measure-theoretic versions of the events.
Lean usage
exact eventWeight_pos R A hAformal statement (Lean)
33theorem eventWeight_pos {n : Nat} (R : FiniteBooleanReality n)
34 (event : Fin n → Bool) (hNonempty : EventNonempty event) :
35 0 < R.eventWeight event := by
proof body
Tactic-mode proof.
36 rcases hNonempty with ⟨i₀, hi₀⟩
37 unfold eventWeight
38 have h_nonneg : ∀ i : Fin n, 0 ≤ (if event i then R.weight i else 0) := by
39 intro i
40 by_cases h : event i
41 · simp [h, le_of_lt (R.positive_weight i)]
42 · simp [h]
43 have h_i0_pos : 0 < (if event i₀ then R.weight i₀ else 0) := by
44 simp [hi₀, R.positive_weight i₀]
45 have h_le_sum :
46 (if event i₀ then R.weight i₀ else 0) ≤
47 ∑ i, if event i then R.weight i else 0 := by
48 exact Finset.single_le_sum (fun i _ => h_nonneg i) (Finset.mem_univ i₀)
49 exact lt_of_lt_of_le h_i0_pos h_le_sum
50
51/-- Likelihood ratio of two events. -/