pith. sign in
module module moderate

IndisputableMonolith.Foundation.DomainBootstrap

show as:
view Lean formalization →

DomainBootstrap bootstraps the domain for the logic-as-functional-equation framework by introducing a comparison operator on linearly ordered fields together with derived cost and invariance structures. It depends on the non-triviality corollary that rules out the zero operator via distinguishability. The module consists entirely of definitions and type classes.

claimA comparison operator $C$ on a linearly ordered field $F$ such that the derived cost function is not identically zero on positive ratios.

background

The module belongs to the Foundation layer and imports LogicAsFunctionalEquation together with NonTrivialityFromDistinguishability. The latter states: 'Move 1: promote NonTrivial from a posit to a corollary. In Foundation.LogicAsFunctionalEquation, SatisfiesLawsOfLogic carries a non_trivial field stating that the derived cost function is not identically zero on the positive ratios. The reason it was posited at all is that the constant-zero comparison operator'. Definitions introduced include ComparisonOperatorOn, derivedCostOn, IdentityOn, NonContradictionOn, ScaleInvariantOn, DistinguishabilityOn, and the bootstrap maps bootstrap_to_real and bootstrap_closure.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the domain objects required by the unified forcing chain (T0-T8) and the Recognition Composition Law. Its bootstrap_closure and real_supports_logic constructions connect the abstract logic structures to concrete models used downstream in J-uniqueness and phi-ladder derivations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)