Stage-Finite Euclidean Geometry

Geometric structure of tau^3 determined by stage spaces Z/P_k Z (finite cyclic groups with positive-definite cyclic metric), stage-k Tarski axioms, and profinite limit preserving Euclidean geometry. Discretely Euclidean at every finite stage, profinitely Euclidean in the limit.

Stage-Finite Euclidean Geometry

Summary

Geometric structure of tau^3 determined by stage spaces Z/P_k Z (finite cyclic groups with positive-definite cyclic metric), stage-k Tarski axioms, and profinite limit preserving Euclidean geometry. Discretely Euclidean at every finite stage, profinitely Euclidean in the limit.

Statement

%
\label{def:stage-finite-euclidean}
\textbf{Stage-finite Euclidean geometry}
is the geometric structure on $\tau^3$
defined by:
\begin{enumerate}
    \item[\textup{(S1)}]
          \textbf{Stage spaces.}
          At each primorial depth~$k$,
          the stage-$k$ space $\tau^3_k$
          is a finite set of points.
    \item[\textup{(S2)}]
          \textbf{Discrete distance.}
          The ultrametric $d = 2^{-\delta}$
          restricts to a discrete metric on $\tau^3_k$.
    \item[\textup{(S3)}]
          \textbf{Stage-$k$ Tarski axioms.}
          All ten Tarski axioms hold
          on each $\tau^3_k$.
    \item[\textup{(S4)}]
          \textbf{Profinite limit.}
          The full geometry on $\tau^3$
          is the profinite limit
          $\tau^3 = \varprojlim_k \tau^3_k$.
\end{enumerate}
The geometry is ``finitely Euclidean at every stage''
and ``profinitely Euclidean in the limit.''

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 178
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part11/ch64-gains.tex lines 212-240

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Mirror.WaveHolomorphy
• Name: StageGeometry

Dependencies

• Canonical: II.D14, II.T15, II.T16, II.T17, II.T18

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.