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