13 Operational continuum and number spectrum (exploratory)
13.1 Position
This chapter is exploratory and not a published work (no DOI): a hand-built operational continuum (Path 1, after Brouwer) and an operational number spectrum \(\mathbb {Z} \to \mathbb {Q} \to \mathbb {C} \to \mathbb {R} \to \Omega \), every node constructed from \(\mathbb {Z}\) and kept below the Classical.choice floor. Nothing here passes through mathlib’s \(\mathbb {Q}\) or \(\mathbb {R}\), which are entirely Tier-3 (Finding CONT-7: even \((2:\mathbb {Q})+3\) pulls Classical.choice); the construction stays in pure \(\mathbb {Z}\) arithmetic, so every object below is Axiom profile: [propext, Quot.sound].
The deliverable is not new mathematics — these are textbook rationals and Gaussian rationals — but the precise location of two boundaries, each machine-checked, and a single thesis they share: the Classical.choice floor is a property of construction, not of the object.
13.2 The number spectrum
|
node |
DecidableEq |
order |
inverse |
|
\(\mathbb {Q}_{\mathrm{op}}\) (Qop) |
yes |
yes, trichotomy |
total |
|
\(\mathbb {C}_{\mathrm{op}}\) (GaussQ) |
yes |
none (\(\mathbb {C}\) unorderable) |
total |
|
\(\mathbb {R}_{\mathrm{op}}\) (Real) |
no (Markov) |
apartness only |
witnessed (Pre.invPos) |
Every row is Axiom profile: [propext, Quot.sound]. \(\mathbb {Q}_{\mathrm{op}}\) is the decidable pole: equality, order and a total reciprocal are all decidable and choice-free.
Qop (cross-multiplication quotient of \(\mathbb {Z} \times \mathbb {Z}_{{\gt}0}\)) is a CommRing with DecidableEq, full trichotomy (lt_trichotomy), and a total reciprocal with \(a \ne 0 \to a \cdot a^{-1} = 1\) (mul_inv_cancel). All Axiom profile: [propext, Quot.sound].
GaussQ \(= \texttt{Qop}[i]\) (\(\{ re, im : \texttt{Qop}\} \)) is a CommRing with DecidableEq and a total reciprocal \(z^{-1} = \bar z/|z|^2\) for \(z \ne 0\). Axiom profile: [propext, Quot.sound]. A completeness node: it inherits its base \(\texttt{Qop}\)’s operational character and opens no new operational boundary (its lack of order is classical algebra — \(\mathbb {C}\) is unorderable — not operationality).
13.3 Boundary I: the Markov line (decidability of zero)
\(\mathbb {Q}_{\mathrm{op}}\) and \(\mathbb {C}_{\mathrm{op}}\) carry a total reciprocal because zero is decidable there. Operational \(\mathbb {R}\) cannot: \(\lnot (x \approx 0)\) gives no lower-bound modulus on \(|x|\) (that step is Markov’s principle, non-constructive), so the operational real reciprocal Pre.invPos must take an explicit positivity/apartness witness rather than being total. The \(\texttt{Field}/\texttt{CommRing}\) line across the spectrum is exactly the decidability of zero.
13.4 Boundary II: content versus packaging (machine-checked)
The field content (mul_inv_cancel) is choice-free, but registering Qop as a mathlib Field is blocked below the floor: Field extends DivisionRing extends RatCast, forcing a map \(\texttt{ratCast} : \mathbb {Q} \to \texttt{Qop}\). Any such map reads mathlib \(\mathbb {Q}\) (Tier-3), so it pulls Classical.choice.
Qop.ofRat (the forced ratCast) is Axiom profile: [propext, Classical.choice, Quot.sound], while Qop.mul_inv_cancel is Axiom profile: [propext, Quot.sound]. The field’s doing (its operations) is operational; the Field label (its packaging) is not. This is the doing/being asymmetry at the typeclass level.
The boundary is a build invariant. The exhibit VRClassical/Continuum/Spectrum.lean certifies it at build time over the generic checker Meta/DependsOn.lean:
|
declaration |
Classical.choice |
|
Qop.mul_inv_cancel (field content) |
free |
|
GaussQ.mul_inv_cancel (field content) |
free |
|
Qop.lt_trichotomy (decidable order) |
free |
|
Qop.ofRat (ratCast packaging) |
depends |
13.5 Two rationals, by necessity
The repository now contains two constructions of the rationals, and this is not redundancy — they are the two horns of the floor:
\(\mathbb {Q}_{\mathrm{VR}}\) (Chapter 3, published): built to prove an isomorphism to mathlib \(\mathbb {Q}\); the isomorphism forces the path through mathlib and is Tier-3 by necessity.
Qop (this chapter): built to be choice-free below the floor; it makes no isomorphism claim, which choice-freeness forbids.
A single \(\mathbb {Q}\) that is both choice-free and proven isomorphic to mathlib \(\mathbb {Q}\) is impossible: the isomorphism is a ratCast, which pulls Classical.choice (Finding 338). The same object, two constructions, one above and one below the floor — the construction-relativity of the floor, exhibited concretely.
13.6 Doing, not being (meta)
The same asymmetry appears at the predicate level. Across the published algebra cycle the element predicate IsOperational is fun _ => True in every instance, and Forms.operational_total is a theorem that operationality is total: as a property of being (the object), operationality does not discriminate. What discriminates is the axiom tier of a construction, decidable and universal via Meta/DependsOn.
On one domain \(\mathbb {Z}\): being_total_int (\(\forall a,\ \texttt{IsOperational}\, a\)) is total and choice-free (being does not discriminate), while one \(\le \)-transitivity statement has two proofs — trans_doing (omega) Axiom profile: [propext, Quot.sound] and trans_being_via_choice (le_trans) Axiom profile: [propext, Classical.choice, Quot.sound] — so doing discriminates. The operational boundary lives on the act, not the object: “nothing is, all is doing” at the meta level.
The becoming/Brouwerian core (Spread … Model) realises a non-enumerable operational continuum via choice sequences (branches_not_enumerable, an unconditional Cantor diagonal, Axiom profile: [propext]), with Brouwerian continuity tracked as a hypothesis or earned in a finite-information model — never adopted over classical mathlib, where it is inconsistent.
13.7 The three classical pillars, operationally
The done/becoming cut gives Cantor’s diagonal, the Continuum Hypothesis and the Axiom of Choice a single operational reading. The machine-checked core is collected here; the philosophical reading, and the meta-boundaries it cannot cross, are essay-level and marked as such. VR does not solve these; it reformulates them — operationally they dissolve or are reinterpreted, formally they remain meaningful.
operational_cantor Axiom profile: [propext, Quot.sound]: the performed (node) register is countable (operational_register_countable, witness decodeNode), the becoming register is non-enumerable (branches_not_enumerable), and the countable performed cannot exhaust the becoming (no_node_surjection). The \(\wp (\mathbb {N})\) bridge powerset_diagonal Axiom profile: [propext]: the full powerset (characteristic functions \(\mathbb {N}\to \mathrm{Bool}\)) is non-enumerable, and every enumerable (describable) family of subsets misses its own diagonal. So the diagonal works, but it cuts done/becoming — it does not select an element from a completed uncountable totality (there is none operationally). Reinterpreted, not removed.
CH — dissolved operationally, retained formally (essay). The machine fact under CH is exactly the \(\aleph _0\)/non-enumerable gap of powerset_diagonal. Beyond it CH adds no machine content: “no intermediate cardinal” is a non-existence claim (classically an independence result), not provable inside; and the operational layer is not even uniformly countable (Real is not a countable type — only describable reals would be). CH is therefore a formal-register label, read philosophically; its honest machine anchor is powerset_diagonal.
operational_dependent_choice Axiom profile: [propext]: a history-dependent rule \(f:\mathrm{List\ Bool}\to \mathrm{Bool}\) determines a branch \(\alpha \, n = f(\alpha .\mathrm{take}\, n)\) by recursion — DC is operationally available, choice-free, because there is a rule. Bundled with operational continuity as operational_choice_available Axiom profile: [propext, Quot.sound]. Full AC (selection over an uncountable family with no rule) has no operational correlate — a formal-register label; and \(\mathrm{AC}+\mathrm{AD}\to \bot \) is a \(T\! \to \! T\) phenomenon that never returns through the operational floor. Only DC and WC-N (the Continuity two-register, not_continuity / continuity_of_nbhd) are machine objects; full AC and AC+AD are essay.
The register asymmetry: \(O\to T\) holds, \(T\to O\) does not. A single machine-checked asymmetry underlies all three pillars. In VR-Forms, translate_implies_realisable gives \(O\to T\) (an operational fact yields the formal term’s realisability); its converse fails — from \(\exists s,\dots \) one cannot recover the specific operational object (no Skolemisation across the existential). One passes from operational to formal, but never extracts the operational from the formal: crossing \(T\to O\) requires explicit construction, never derivation. This is the logical core of register inheritance, and of why the three pillars dissolve operationally while remaining formally meaningful.
13.8 Honest scope
No new mathematics. Qop and GaussQ are textbook constructions; the value is the choice-free axiom tracking and the two boundaries it makes precise. \(\mathbb {C}\) inherits. The Gaussian rationals add a completeness node, not an operational insight. Choice did not vanish from VR. The published works (Numbers, Sets, Audit, Algebra’s \(\mathbb {Q}\)-field) remain Tier-3, unchanged; this chapter adds a parallel choice-free \(\mathbb {Q}/\mathbb {C}\) alongside the classical one, not a replacement. The witness is meta-trusted — the dependency checker certifies the relation but is not itself kernel-verified, the same tier as #print axioms.
The Lean 4 formalisation lives under VR/Continuum/ (Rational, GaussianRational, Real, UnitInterval, the becoming core Spread … Model, and the consolidated exhibit Spectrum), with the meta-thesis in VRClassical/Meta/DoingNotBeing.lean.