Order Bound

Order Bound: for all A in Set(alpha_n), A <= alpha_n in the internal order on tau-Idx. alpha_n is the maximum of Set(alpha_n). Membership ‘looks downward’ from the representing element.

Order Bound

Summary

Order Bound: for all A in Set(alpha_n), A <= alpha_n in the internal order on tau-Idx. alpha_n is the maximum of Set(alpha_n). Membership ‘looks downward’ from the representing element.

Statement

%
\label{prop:order-bound}
For all $A \in \mathrm{Set}(\alpha_n)$,
\[
    \boxed{A \;\leq\; \alpha_n}
\]
in the internal order on $\tau$-Idx.
In particular, $\alpha_n$ is the \textbf{maximum}
of $\mathrm{Set}(\alpha_n)$.

Proof / Justification

Every element $\alpha_k \in \mathrm{Set}(\alpha_n)$
satisfies $k \mid n$.
For $n \geq 1$,
divisibility implies $k \leq n$
(since $k \mid n$ and $n > 0$
forces $k \leq n$).
Therefore $\alpha_k \leq \alpha_n$
in the natural ordering on $\tau$-Idx.

Source Context

• Registry source: book-01.jsonl line 215
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part08/ch83-orbit-set-correspondence.tex lines 471-481

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Sets.OrbitSets
• Name: Tau.Sets.orbit_set_order_bound

Dependencies

• Canonical: I.D94, I.D31

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.