real_supports_logic
plain-language theorem explainer
The definition equips the reals with a LogicSupported structure for any comparison operator C that satisfies the laws of logic. Researchers closing the logic-to-reals bootstrap cite it to establish that the construction is idempotent on its own domain. The proof is a direct structure construction that copies the four law fields from the hypothesis and discharges the ordering axiom by normalization.
Claim. Let $C$ be a comparison operator on the reals that satisfies the laws of logic. Then the reals carry a logic-supported structure: they admit an identity operator, a non-contradiction operator, a scale-invariant operator, and a distinguishability operator, together with the ordering fact $0<1$.
background
LogicSupported packages a linearly ordered field K with a comparison operator C obeying the four Aristotelian conditions plus scale invariance and distinguishability. The module states the bootstrap theorem: any ordered field supporting the Law of Logic, together with the Archimedean and conditional-completeness hypotheses forced by continuity of C, is canonically isomorphic to the reals. The upstream hypothesis SatisfiesLawsOfLogic encodes the functional-equation form of those laws; the distinguishability field is recovered from non-triviality via the lemma distinguishability_of_nonTrivial.
proof idea
The definition builds the LogicSupported instance on the reals by assigning the supplied C, copying identity, non_contradiction, scale_invariant, and distinguishability directly from the hypothesis h, and obtaining the distinguishability field via distinguishability_of_nonTrivial applied to C and h.non_trivial. The single ordering axiom zero_lt_one_in_K is discharged by norm_num.
why it matters
This definition supplies the backward half of the bootstrap closure, showing that the reals themselves satisfy the logic-support condition. It therefore makes the choice of ambient field canonical up to ordered-field isomorphism once the Law of Logic and Archimedean completeness are assumed. The construction feeds the idempotence argument that any other candidate ordered field supporting the same laws is isomorphic to the reals, closing the chicken-and-egg loop between RealsFromLogic and the present module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.