EventNonempty
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assign a numerical value to the weight of the event.
- Does not extend the predicate to events indexed by infinite sets.
- Does not assert uniqueness of the witnessing index.
- Does not invoke the J-cost function or the phi-ladder.
formal statement (Lean)
29def EventNonempty {n : Nat} (event : Fin n → Bool) : Prop :=
proof body
Definition body.
30 ∃ i, event i = true
31
32/-- Nonempty finite Boolean events have positive weight. -/