Pith. sign in
module module high

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge

show as:
view Lean formalization →

The BooleanRatioBridge module defines finite weighted Boolean realities over Fin n and proves their embedding into positive ratios. It supplies the discrete-logic half of the scale-free comparison chain collected in the main theorem package. The module consists of supporting definitions for weights and ratios followed by a single embedding theorem.

claimLet $B$ be a finite weighted Boolean reality over $\mathrm{Fin}\,n$. Then $B$ embeds into the positive ratios such that counted-once composition is preserved and the resulting factors satisfy the Recognition Composition Law.

background

This module belongs to the LogicAsFunctionalEquation package. The upstream MainTheorem module collects the formal chain closest to the paper headline: scale-free comparison factors through positive ratios; no-hidden-state finite comparison gives counted-once composition; counted-once finite logical comparison forces the RCL family. The module introduces FiniteBooleanReality together with the auxiliary notions eventWeight, eventRatio and the embedding statement finite_boolean_logic_embeds_into_positive_ratios.

proof idea

This is a definition module, no proofs. It introduces the Boolean reality object, defines positive weights and ratios on events, and states the embedding theorem that realizes the finite case of the main chain.

why it matters in Recognition Science

The module supplies the finite Boolean case that feeds the main theorem package for logic as functional equation. It realizes the step in which no-hidden-state finite comparison gives counted-once composition, which forces the RCL family as described in the upstream module documentation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)