EventNonempty
plain-language theorem explainer
EventNonempty supplies the predicate that a finite Boolean event over Fin n is nonempty precisely when at least one coordinate is true. Researchers embedding discrete logic into continuous ratio spaces cite it to guarantee positive weights and ratios. The declaration is a direct existential quantification with no auxiliary lemmas.
Claim. Let $n$ be a natural number and let $event : Fin n → Bool$ assign a truth value to each of the $n$ positions. The predicate holds if and only if there exists an index $i$ such that $event(i) = true$.
background
The module Finite Boolean bridge to positive ratios constructs a discrete-to-continuous link: finite Boolean events equipped with positive weights are compared by likelihood ratios that stay positive whenever both weights are positive. FiniteBooleanReality n is the structure that assigns a real weight to each position in Fin n; eventWeight sums the weights over the positions where the event is true.
proof idea
The definition is an abbreviation whose body is the existential statement ∃ i, event i = true. No lemmas or tactics are invoked; the predicate is introduced exactly as the witness that the event is nonempty.
why it matters
EventNonempty is the hypothesis that feeds eventWeight_pos, which proves the weight is positive, and thereby eventRatio_pos and finite_boolean_logic_embeds_into_positive_ratios. It completes the discrete-to-continuous step that lets finite Boolean comparisons inherit positivity from the ratio domain in the Recognition Science foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.