Anchor Numbers: Completing Dynamic Number with the Anchor Primitive (Constructive Mathematics Series; E-system completion case No.1; Lean formalization, three heterogeneous anchored families, collapse of Cauchy dynamics)
Abstract
Anchor numbers: the completion of the dynamic ontology of number. The companion paper [statics-as-manifestation, DOI 10.5281/zenodo.22785052] axiomatizes number as spontaneous dynamics (D0-D2) but leaves a diagnostic gap: the dynamic axioms are silent about fate — two legitimate models satisfy D0 while one drifts forever and the other stabilizes (machine-verified). Anchor numbers add the missing variable: an anchor, given by a de-constrained dynamic axiom (Anchor-0: motion is the ontology of number, no presupposed direction or manner) and a locality axiom (Anchor-1: where the anchor is, there the limit is; the anchor is defined retroactively by its consequence, presupposing no dynamic structure). The dynamic axioms are absorbed (compatibility of the full axiom set machine-verified; free filling provably fails to carry the observational completeness axiom). Three mechanically heterogeneous anchored families — potential-type (wall and well), metric-type (Banach contraction families), lattice-type (Tarski-Knaster monotone operators on complete lattices, least fixed point intrinsically determined by order structure) — each with an unanchored control theorem, support the claim that anchor numbers are the completion of dynamic number. On the static side, Cauchy dynamics collapse to unique static points under the completeness anchor, and the complete space itself is constructed by the completion functor: the anchor is not an axiom but a construction. Crown: the real numbers of standard mathematics are anchor-collapse products; the two-century rigorization of calculus (Newton's fluxions, Berkeley's ghosts of departed quantities, Cauchy-Weierstrass limits, Dedekind-Cantor completeness) is the first historical actualization of this collapse. Academic comparison: Brouwer (same topic, opposite direction), Cantor-Dedekind (operationally isomorphic, semantically heterogeneous), Bishop (constructive completion holds while the completion reading is refused), Tarski-Davis (completeness equivalent to anchoredness, in lattice terms) — the 'anchor' semantics is blank in all four layers. This construction is also the first live case of the completion standard (E-system) of the constructive-mathematics certification standard. All core theorems formalized in Lean 4 with zero sorry. Record includes the bilingual main document (CN/EN) and two Lean formalization files. v1.1 adds an end-of-paper version note (readout-surface-constant interface): the 2026-10-16 minimal real-line point-sampling experiment supplies a minimal mathematical instance of the anchor definition - the boundary {1,2} of the open interval (1,2) is necessarily given by the interval's definition (Lean general form frontier(Ioo a b) = {a,b}, zero sorry) while interior single-point sampling hits it with measure zero: a minimal model of the anchor's retroactive definition and local unreachability.
Related
- The Generative Mechanism of Dimension: An Axiomatic Construction of Dimensional Conventions (Constructive Mathematics Series, Paper 6; Lean formalization, model-pair independence, numerical evidence)
- Inequalities and equalities of means in Constructive Mathematics
- The strength of the minimum principle in constructive reverse mathematics
- Completing the classification of Hopf superalgebras of dimension up to 10
- Sophus Lie's problem on two-dimensional metrics with projective symmetries: completing the local classification
BibTeX
@article{qin2026anchor,
title = {{Anchor Numbers: Completing Dynamic Number with the Anchor Primitive (Constructive Mathematics Series; E-system completion case No.1; Lean formalization, three heterogeneous anchored families, collapse of Cauchy dynamics)}},
author = {Qin Qin},
journal = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = sep,
doi = {10.5281/zenodo.22866458},
url = {https://doi.org/10.5281/zenodo.22866458},
note = {CC BY},
}
RIS
TY - JOUR
TI - Anchor Numbers: Completing Dynamic Number with the Anchor Primitive (Constructive Mathematics Series; E-system completion case No.1; Lean formalization, three heterogeneous anchored families, collapse of Cauchy dynamics)
AU - Qin Qin
PY - 2026
DA - 2026/09/21
JO - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.22866458
UR - https://doi.org/10.5281/zenodo.22866458
AB - Anchor numbers: the completion of the dynamic ontology of number. The companion paper [statics-as-manifestation, DOI 10.5281/zenodo.22785052] axiomatizes number as spontaneous dynamics (D0-D2) but leaves a diagnostic gap: the dynamic axioms are silent about fate — two legitimate models satisfy D0 while one drifts forever and the other stabilizes (machine-verified). Anchor numbers add the missing variable: an anchor, given by a de-constrained dynamic axiom (Anchor-0: motion is the ontology of number, no presupposed direction or manner) and a locality axiom (Anchor-1: where the anchor is, there the limit is; the anchor is defined retroactively by its consequence, presupposing no dynamic structure). The dynamic axioms are absorbed (compatibility of the full axiom set machine-verified; free filling provably fails to carry the observational completeness axiom). Three mechanically heterogeneous anchored families — potential-type (wall and well), metric-type (Banach contraction families), lattice-type (Tarski-Knaster monotone operators on complete lattices, least fixed point intrinsically determined by order structure) — each with an unanchored control theorem, support the claim that anchor numbers are the completion of dynamic number. On the static side, Cauchy dynamics collapse to unique static points under the completeness anchor, and the complete space itself is constructed by the completion functor: the anchor is not an axiom but a construction. Crown: the real numbers of standard mathematics are anchor-collapse products; the two-century rigorization of calculus (Newton's fluxions, Berkeley's ghosts of departed quantities, Cauchy-Weierstrass limits, Dedekind-Cantor completeness) is the first historical actualization of this collapse. Academic comparison: Brouwer (same topic, opposite direction), Cantor-Dedekind (operationally isomorphic, semantically heterogeneous), Bishop (constructive completion holds while the completion reading is refused), Tarski-Davis (completeness equivalent to anchoredness, in lattice terms) — the 'anchor' semantics is blank in all four layers. This construction is also the first live case of the completion standard (E-system) of the constructive-mathematics certification standard. All core theorems formalized in Lean 4 with zero sorry. Record includes the bilingual main document (CN/EN) and two Lean formalization files. v1.1 adds an end-of-paper version note (readout-surface-constant interface): the 2026-10-16 minimal real-line point-sampling experiment supplies a minimal mathematical instance of the anchor definition - the boundary {1,2} of the open interval (1,2) is necessarily given by the interval's definition (Lean general form frontier(Ioo a b) = {a,b}, zero sorry) while interior single-point sampling hits it with measure zero: a minimal model of the anchor's retroactive definition and local unreachability.
ER -