AXM0006canonicalv1No-Jump / Cover (K4)
rho is a successor within each orbit (no skipping); covers are primitive.
Payload
No-Jump / Cover (K4)
rho is a successor within each orbit (no skipping); covers are primitive.
No-Jump / Cover (K4)
Summary
rho is a successor within each orbit (no skipping); covers are primitive.
Statement
%
\label{ax:no-jump}
For each generator $g \in \{\alpha, \pi, \gamma, \eta\}$ and
each $n \geq 0$:
\[
\boxed{%
\rho\bigl(\rho^n(g)\bigr) = \rho^{n+1}(g).
}
\]
The element $\rho^{n+1}(g)$ is the \emph{immediate successor}
of $\rho^n(g)$ in $O_g$, and there is no other element
between them.
Proof / Justification
This item is an axiom. No manuscript proof is required.
Source Context
- Registry source:
book-01.jsonlline 9 - Manuscript source:
2nd-edition/book-i-categorical-foundations/02_mainmatter/part01/ch03-generation-cover.texlines 162-175
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookI.Kernel.Axioms - Name:
Tau.Kernel.K4_no_jump
Dependencies
- Canonical: I.D02
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
I.K4no-jump-cover-k4ax:no-jumpRelease lines
corpus_v3_workingcorpus_v2Relations
Formalized by (1)
Appears in (1)
Downstream uses (computed) (2)
Items in the corpus that reference this one via load-bearing relations. Computed from the full corpus-v3 graph at build time.
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.