FiniteBooleanReality
FiniteBooleanReality n equips a finite collection of n Boolean atoms with strictly positive real weights. It is cited by the eventRatio and eventWeight definitions to embed finite Boolean logic into positive-ratio comparisons. The declaration is a bare structure record whose two fields directly encode the map and the positivity condition with no further obligations.
claimLet $n$ be a natural number. A finite weighted Boolean reality is a function $w : [n] → ℝ$ such that $w(i) > 0$ for every index $i$.
background
The module supplies a modest discrete-to-continuous bridge: finite Boolean events equipped with positive weights compare by likelihood ratios, and those ratios remain positive. FiniteBooleanReality n records a weight map on the finite set Fin n together with the universal positivity hypothesis. Upstream structures supply the surrounding context: J-cost minimization is convex with unique minimum at unity (PhysicsComplexityStructure), ledger factorization calibrates the positive-ratio domain (DAlembert), and spectral emergence fixes the gauge and generation content that the ratios ultimately serve.
proof idea
The declaration is a direct structure definition. It packages the weight function and the positivity predicate with no computational content or proof obligations.
why it matters in Recognition Science
It provides the interface that lets finite Boolean logic embed into the positive-ratio domain required by the Recognition Composition Law. The structure is used directly by eventRatio, eventWeight, and the embedding theorem finite_boolean_logic_embeds_into_positive_ratios. This step closes the discrete-to-continuous passage between Boolean atoms and the J-functional equation in the T0–T8 forcing chain.
scope and limits
- Does not prescribe how the weights are chosen or normalized.
- Does not link the weights to Recognition Science constants such as phi or alpha.
- Does not guarantee that the induced ratios obey the Recognition Composition Law.
- Does not extend to infinite or continuous Boolean algebras.
formal statement (Lean)
17structure FiniteBooleanReality (n : Nat) where
18 weight : Fin n → ℝ
19 positive_weight : ∀ i, 0 < weight i
20
21namespace FiniteBooleanReality
22
23/-- The weight of an event. -/