IndisputableMonolith.Foundation.DomainBootstrap
Relativizes the Recognition comparison-operator axioms to an arbitrary linearly ordered field and shows that the reals carry a full logic-supporting structure. Anyone citing domain independence of the J-cost or the real bootstrap of SatisfiesLawsOfLogic lands here. The module packages the On-predicates, the LogicSupported interface, and the bootstrap_to_real / bootstrap_closure theorems.
claimOn a linearly ordered field $F$, a comparison operator $C$ yields a derived cost $J_C$. The structure $(F,C)$ is logic-supporting when identity, non-contradiction, scale invariance, and distinguishability hold for $J_C$. The reals admit such a $C$, and the bootstrap closes: any domain meeting the required interface supports the laws of logic.
background
Recognition Science encodes the laws of logic as a functional equation on a comparison operator, with derived cost $J(x)=(x+x^{-1})/2-1$ (T5). In LogicAsFunctionalEquation, SatisfiesLawsOfLogic packages identity, non-contradiction, scale invariance, and a non-triviality clause on positive ratios.
NonTrivialityFromDistinguishability promotes non-triviality from a bare posit to a corollary of distinguishability, so the constant-zero operator is ruled out rather than excluded by hand. This module lifts those axioms off a fixed carrier and states them relative to an arbitrary linearly ordered field $F$ via the *On predicates (IdentityOn, NonContradictionOn, ScaleInvariantOn, DistinguishabilityOn).
ComparisonOperatorOn and derivedCostOn are the domain-relative operator and cost. LogicSupported is the bundled interface; required collects the minimal hypotheses the bootstrap needs.
proof idea
Definition layer first: the *On predicates restate each logic law with explicit quantification over the ordered field $F$ and its positive units. LogicSupported F packages those predicates plus the comparison operator.
bootstrap_to_real instantiates the interface on $\mathbb{R}$ by supplying the standard multiplicative comparison and verifying each law from the ordered-field structure and the upstream non-triviality corollary. real_supports_logic is the resulting instance. bootstrap_closure shows that any carrier meeting required yields LogicSupported, so the real case is the canonical model rather than a one-off.
why it matters in Recognition Science
Without a domain bootstrap, the functional-equation form of logic is pinned to a single carrier and cannot feed the forcing chain (T5 J-uniqueness through T8). This module is the bridge from LogicAsFunctionalEquation and NonTrivialityFromDistinguishability to any later development that needs the laws of logic on $\mathbb{R}$ or on a generic ordered field.
Downstream work that quotes real-supported $J$, scale invariance on positive reals, or closure of the logic interface under the required hypotheses depends on bootstrap_to_real and bootstrap_closure. No used_by edges are recorded yet in the mirror graph; the module is foundational scaffolding for the Foundation domain rather than a leaf lemma.
scope and limits
- Does not prove J-uniqueness (T5) or the Recognition Composition Law on the bootstrapped domain.
- Does not construct comparison operators on carriers other than those meeting required.
- Does not derive dimensional or octave constraints (T7, T8) from LogicSupported.
- Does not discharge physics constants or the mass ladder; Foundation only.
- Does not claim every linearly ordered field supports logic without the required hypotheses.