required
plain-language theorem explainer
The required structure bundles the minimal ordered-field axioms plus support for a comparison operator obeying the Law of Logic, together with explicit Archimedean and Dedekind-completeness hypotheses. Researchers closing the bootstrap from logic to the reals, or invoking the domain in action functionals and complexity bounds, cite this definition. It is introduced as a direct structure declaration carrying no proof obligations.
Claim. Let $K$ be a linearly ordered field. The structure required on $K$ consists of a comparison operator $C:K→K→K$ satisfying the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, together with the Archimedean property and Dedekind completeness.
background
The DomainBootstrap module resolves the circularity between stating the Law of Logic on the reals and recovering an isomorphic copy of the reals from that law. It relies on the classical uniqueness of the reals as the unique Archimedean Dedekind-complete ordered field, available in Mathlib through order isomorphisms between any such field and ℝ. The required structure supplies the explicit interface for these hypotheses so that the Law of Logic can be stated without presupposing the target field.
proof idea
The declaration is a bare structure definition. It records the ordered-field carrier, the comparison operator, and the two completeness hypotheses as fields of the record with no tactics, lemmas, or computational content attached.
why it matters
This structure supplies the domain hypothesis for the module's bootstrap theorem that any field supporting the Law of Logic is canonically isomorphic to ℝ. It is referenced by forty downstream results, including uniqueness of action minima, heat-kernel bounds in two-dimensional fluid models, and the unconditional P-versus-NP resolution. It makes explicit the residual analytic input (Archimedean completeness) that the Law of Logic alone does not force, thereby closing the loop in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.