LogicSupported
plain-language theorem explainer
LogicSupported packages the minimal ordered-field data and comparison-operator axioms needed to state the Law of Logic on an arbitrary linearly ordered field K. Researchers deriving the reals from logic axioms cite it to isolate the Aristotelian conditions plus scale invariance and distinguishability from the separate Archimedean and completeness hypotheses. The declaration is a plain structure definition that simply bundles the field instances, the operator, and the four required properties with no further proof steps.
Claim. A linearly ordered field $K$ is Logic-supported when $0<1$ holds in $K$, a comparison operator $C:K→K→K$ exists, and $C$ satisfies: identity ($C(x,x)=0$ for all $x>0$), non-contradiction ($C(x,y)=C(y,x)$ for all $x,y>0$), scale invariance ($C(λx,λy)=C(x,y)$ for all $x,y,λ>0$), and distinguishability (there exist $x,y>0$ with $C(x,y)≠0$).
background
The module DomainBootstrap isolates the comparison-operator domain that carries the Law of Logic. A comparison operator is simply any map $C:K→K→K$ on a linearly ordered field; the four Aristotelian conditions are then expressed as the predicates IdentityOn, NonContradictionOn, ScaleInvariantOn and DistinguishabilityOn (all defined in the same file). These predicates are the generic-field versions of the functional equation studied in LogicAsFunctionalEquation. The module doc states that the Law of Logic on an ambient field plus Archimedean and Dedekind-completeness forces that field to be canonically isomorphic to ℝ; LogicSupported is the packaging that makes the Law-of-Logic hypotheses explicit while leaving the analytic hypotheses named separately.
proof idea
The declaration is a structure definition whose fields are exactly the required instances and predicates; no tactics or lemmas are applied. It is a one-line wrapper that collects zero_lt_one_in_K together with the four named predicates on the comparison operator C.
why it matters
LogicSupported supplies the hypothesis for the bootstrap theorems bootstrap_to_real and bootstrap_closure, which conclude that any such K is order-isomorphic to ℝ. The module doc identifies this as the step that closes the chicken-and-egg loop between the Law of Logic and the recovered real line. It therefore sits at the interface between the functional-equation formulation of logic and the classical characterization of ℝ as the unique Archimedean conditionally complete ordered field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.