eventWeight
eventWeight sums the positive atom weights of a finite Boolean event by selecting only those atoms that evaluate to true. Researchers building the discrete-to-continuous bridge in Recognition Science cite it when forming likelihood ratios of events. The definition is a direct summation that extracts the total weight for the supplied event vector.
claimFor a finite weighted Boolean reality $R$ on $n$ atoms, each with positive weight $w_i$, the weight of an event $e :$ Fin $n$ $→$ Bool is $W(e) = ∑_i w_i$ if $e(i)$ holds and $0$ otherwise.
background
The module gives a discrete-to-continuous bridge: finite Boolean events with positive weights compare by likelihood ratios that stay positive when both weights are positive. A FiniteBooleanReality n is the structure with weight : Fin n → ℝ and the axiom ∀ i, 0 < weight i. Events are maps Fin n → Bool; their weight sums the atom weights marked true by the map.
proof idea
This is a definition implemented by direct summation over Fin n. For each i it adds R.weight i when event i holds and adds zero otherwise.
why it matters in Recognition Science
eventWeight is the operand for the sibling eventRatio that forms likelihood ratios and for the theorem eventWeight_pos that shows nonempty events have positive weight. It fills the finite Boolean bridge in the LogicAsFunctionalEquation module, supporting the Recognition Composition Law and the T5–T8 forcing chain that derives three spatial dimensions.
scope and limits
- Does not apply to infinite collections of atoms.
- Does not require the weights to sum to one.
- Does not itself form ratios between events.
- Does not invoke the self-reference axioms from UniversalForcingSelfReference.
Lean usage
noncomputable def sampleRatio {n : Nat} (R : FiniteBooleanReality n) (A B : Fin n → Bool) : ℝ := R.eventWeight A / R.eventWeight Bformal statement (Lean)
24noncomputable def eventWeight {n : Nat} (R : FiniteBooleanReality n)
25 (event : Fin n → Bool) : ℝ :=
proof body
Definition body.
26 ∑ i, if event i then R.weight i else 0
27
28/-- A positive witness for an event. -/