`bootstrap_closure`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DomainBootstrap
domain: Foundation
line: 155 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.DomainBootstrap on GitHub at line 155.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 152/-- **Bootstrap closure**: the Law of Logic plus Archimedean
 153completeness uniquely picks out `ℝ` as the ambient ordered field, up
 154to canonical isomorphism. -/
 155theorem bootstrap_closure
 156    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
 157    (h : LogicSupported K) :
 158    Nonempty (K ≃+*o ℝ) :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.