bootstrap_closure
plain-language theorem explainer
Any conditionally complete linearly ordered field that carries a comparison operator satisfying the Law of Logic conditions is canonically isomorphic to the reals as an ordered field. Foundation researchers cite the result to close the identification between the ambient field used to state the Law and the LogicReal recovered from it. The argument is a direct one-line application of the induced order-ring isomorphism supplied by the completeness axioms.
Claim. Let $K$ be a conditionally complete linearly ordered field that admits a comparison operator satisfying the identity, non-contradiction, scale-invariance and distinguishability axioms of the Law of Logic. Then there exists at least one order-preserving ring isomorphism from $K$ to the reals.
background
The module treats the bootstrap problem for the comparison-operator domain. A field $K$ is LogicSupported when it is equipped with a comparison operator obeying the four Aristotelian conditions plus scale invariance and distinguishability. The module document states that the Law of Logic is formulated inside an ambient ordered field while the recovered LogicReal must match that field up to isomorphism, creating an explicit chicken-and-egg that the completeness hypotheses resolve.
proof idea
The proof is a one-line wrapper that applies the upstream bootstrap_to_real theorem to the given hypotheses. That result invokes the Mathlib construction LinearOrderedField.inducedOrderRingIso to obtain the required order-preserving ring isomorphism.
why it matters
The declaration supplies the final identification step inside DomainBootstrap, confirming that the Law of Logic together with named Archimedean and conditional completeness selects the reals uniquely up to canonical isomorphism. It thereby closes the loop required before any downstream physics derivations that rely on the concrete real line can proceed inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.