eventWeight_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.