Approximation Sequence

Approximation Sequence

Approximation Sequence

Summary

Approximation Sequence

Statement

%
\label{def:approximation-sequence}
Let $x \in \tau^3$ be a $\tau$-admissible point.
The \textbf{approximation sequence} of~$x$
is the sequence of normalized stage-$k$ coordinate vectors
\[
    \boxed{%
    \mathrm{app}_k(x)
    \;:=\;
    \left(
        \frac{D_k(x)}{P_k},\;
        \frac{A_k(x)}{P_k},\;
        \frac{B_k(x)}{P_k},\;
        \frac{C_k(x)}{P_k}
    \right)
    \;\in\; [0, 1)^4
    \;\subset\; \mathbb{R}^4,}
\]
where $P_k = p_1 \cdots p_k$ is the $k$th primorial
and the coordinates $D_k, A_k, B_k, C_k$
are the ABCD values of the CRT reduction~$\pi_k(x)$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 59
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part04/ch22-orthodox-bridge.tex lines 134-156

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Geometry.OrthodoxBridge
• Name: approx_seq

Dependencies

• Canonical: II.D13, II.D14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.