eventRatio_pos
Nonempty finite Boolean events under a weighted reality compare via strictly positive likelihood ratios. Researchers bridging discrete Boolean structures to the positive reals in the LogicAsFunctionalEquation module cite this result. The term proof unfolds the ratio definition and applies division positivity to the two positive event weights.
claimLet $R$ be a finite weighted Boolean reality on $n$ points with strictly positive real weights on each point. Let $A,B : Fin n → Bool$ be nonempty events (each true at least at one index). Then the ratio of the summed weight of $A$ to the summed weight of $B$ is strictly positive.
background
The module supplies a discrete-to-continuous bridge: finite Boolean events with positive weights compare by likelihood ratios that remain positive. A FiniteBooleanReality is a structure consisting of a weight function $Fin n → ℝ$ together with the axiom that every weight is positive. EventNonempty is the proposition that an event function $Fin n → Bool$ evaluates to true at least once. The event weight is the sum of the underlying weights over the support of the event; eventRatio is the quotient of two such weights.
proof idea
The proof is a one-line term that unfolds eventRatio to the quotient of the two event weights and applies div_pos to the two instances of eventWeight_pos R A hA and eventWeight_pos R B hB.
why it matters in Recognition Science
This result is invoked by the downstream theorem finite_boolean_logic_embeds_into_positive_ratios, which exhibits an explicit positive real equal to the ratio. It completes the local step ensuring that nonempty Boolean comparisons remain inside the positive domain, a prerequisite for embedding finite logic into the positive-ratio setting used by the larger functional-equation framework.
scope and limits
- Does not establish positivity when either event is empty.
- Does not extend the result to infinite or continuous event spaces.
- Does not produce numerical values or bounds on the ratio.
- Does not invoke the Recognition Science forcing chain or phi-ladder.
formal statement (Lean)
57theorem eventRatio_pos {n : Nat} (R : FiniteBooleanReality n)
58 (A B : Fin n → Bool)
59 (hA : EventNonempty A) (hB : EventNonempty B) :
60 0 < R.eventRatio A B := by
proof body
Term-mode proof.
61 unfold eventRatio
62 exact div_pos (eventWeight_pos R A hA) (eventWeight_pos R B hB)
63
64/-- Finite Boolean comparison embeds into the positive-ratio domain whenever
65both compared events have positive measure. -/