bootstrap_closure
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the Law of Logic from more primitive axioms.
- Does not apply to non-Archimedean ordered fields.
- Does not produce explicit numerical values for physical constants.
- Does not address quantum or relativistic extensions of the field.
formal statement (Lean)
155theorem bootstrap_closure
156 (K : Type*) [ConditionallyCompleteLinearOrderedField K]
157 (h : LogicSupported K) :
158 Nonempty (K ≃+*o ℝ) :=
proof body
Term-mode proof.
159 bootstrap_to_real K h
160
161/-! ## 4. Summary
162
163The Law of Logic, on its own, does not literally name the ambient
164field as `ℝ`; it requires a domain that is at least a linearly
165ordered field. Adding the analytic content (Archimedean + Dedekind
166completeness) forces the domain to be `ℝ`. The recovered real line
167from `Foundation.RealsFromLogic` then matches the ambient `ℝ`, and
168the chicken-and-egg is closed up to canonical isomorphism.
169
170The single residual classical input is the Archimedean
171completeness of the ambient field. This is named, not hidden. -/
172
173end DomainBootstrap
174end Foundation
175end IndisputableMonolith