bootstrap_closure
plain-language theorem explainer
Any conditionally complete linearly ordered field supporting the Law of Logic is canonically isomorphic to the reals as an ordered field. Foundation researchers cite this to close the chicken-and-egg between the abstract comparison-operator domain and the concrete real line recovered from the same law. The proof is a one-line wrapper applying the named-hypothesis bootstrap theorem via the induced order ring isomorphism.
Claim. Let $K$ be a conditionally complete linearly ordered field that admits a comparison operator satisfying the four Aristotelian conditions, scale invariance, and distinguishability. Then there exists an order-preserving ring isomorphism from $K$ to the reals.
background
The module closes the loop between the Law of Logic (stated with a comparison operator on an ambient ordered field) and the recovered real line in RealsFromLogic. LogicSupported K packages a linearly ordered field together with a comparison operator obeying identity, non-contradiction, scale invariance, and distinguishability. The upstream bootstrap_to_real states that any such field which is also Archimedean and conditionally complete is canonically isomorphic to ℝ; its doc-comment notes that the completeness hypotheses supply the analytic content the Law of Logic does not provide on its own.
proof idea
The proof is a one-line wrapper that applies bootstrap_to_real K h, which in turn invokes LinearOrderedField.inducedOrderRingIso to produce the order ring isomorphism.
why it matters
This declaration supplies the uniqueness step that forces the ambient field to be ℝ once the Law of Logic is supported, thereby discharging the residual classical input of Archimedean completeness named in the module doc-comment. It directly supports the sibling real_supports_logic direction and the overall bootstrap argument in DomainBootstrap. The result makes explicit that the Law of Logic plus completeness selects the reals up to canonical isomorphism, consistent with the framework's move from functional equation to concrete domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.