pith. sign in
module module moderate

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge

show as:
view Lean formalization →

BooleanRatioBridge defines finite weighted Boolean realities over Fin n to bridge Boolean logic structures with positive ratio comparisons in the Recognition Science formalization. Researchers citing the logic-as-functional-equation chain would reference this module for its supporting objects. It supplies definitions and basic properties that connect finite Boolean structures to the RCL family via the imported MainTheorem package.

claimA finite weighted Boolean reality over the finite set $Fin n$ consists of a positive weight function on $Fin n$ together with Boolean operations that embed into positive ratios.

background

The module sits in the Foundation.LogicAsFunctionalEquation domain and imports the MainTheorem package. That upstream module collects the formal chain closest to the paper's 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. BooleanRatioBridge introduces the central object of a finite weighted Boolean reality over Fin n along with sibling definitions for event weights, event ratios and their positivity properties.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the main theorem package for logic as functional equation by supplying the Boolean-to-ratio bridge. It contributes the finite structures needed for the scale-free comparison and counted-once composition steps that force the RCL family in the Recognition Science framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)