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