FiniteBooleanReality
plain-language theorem explainer
A structure that equips Fin n with a strictly positive real weight function on its elements. Workers on the Boolean-to-ratio bridge in Recognition Science cite it to ground likelihood comparisons in positive reals. The declaration is a plain structure definition with no computational body or lemmas.
Claim. A finite weighted Boolean reality over $n$ consists of a map $w : [n] → ℝ$ such that $w(i) > 0$ for every $i$.
background
The module supplies a discrete-to-continuous bridge: finite Boolean events equipped with positive weights compare via likelihood ratios that remain positive. FiniteBooleanReality packages the required data type. Upstream structures supply the surrounding Recognition Science setting: LedgerFactorization calibrates J on the positive reals, PhiForcingDerived encodes J-cost, PhysicsComplexityStructure records that J-cost minimization is convex with unique minimum at 1, and SpectralEmergence derives the gauge and generation content from the same forcing chain.
proof idea
This is a structure definition. It directly records the weight function and the positivity axiom; no tactics or lemmas are invoked.
why it matters
The structure supplies the carrier type for the module's downstream results: eventWeight, eventRatio, eventWeight_pos, eventRatio_pos, and the embedding theorem finite_boolean_logic_embeds_into_positive_ratios. It therefore anchors the finite-Boolean fragment of the LogicAsFunctionalEquation development that feeds positive-ratio comparisons into the J-cost and forcing machinery of the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.