eight_tick_span
plain-language theorem explainer
The theorem verifies that the eight discrete phases from the 8-tick ledger structure start at zero and reach 7π/4, establishing uniform spacing of π/4 over [0, 2π). Researchers deriving gauge symmetries from ledger redundancy in Recognition Science cite this to ground the discrete U(1) phase shifts before the continuous limit. The proof is a direct unfolding of the phase map followed by constructor and simplification.
Claim. Let the phase map be defined by $kmapsto kπ/4$ for integers $k=0$ to $7$. Then the value at the first tick is $0$ and the value at the seventh tick is $7π/4$.
background
The module derives gauge invariance from ledger redundancy, where distinct ledger representations encode identical physics and the choice among them constitutes the symmetry. The 8-tick structure supplies the discrete phases $φ_k = kπ/4$ for $k=0,…,7$, which serve as the fundamental discrete level whose continuous limit yields U(1). This rests on the phase map definition together with upstream results on collision-free empirical programs, simplicial edge lengths, circle phase lifts, and mock theta structures that guarantee the phases remain well-defined and neutral.
proof idea
The proof is a one-line wrapper that unfolds the discrete phase map definition, splits the conjunction with constructor, and applies simplification to confirm the two endpoint identities.
why it matters
The declaration anchors the discrete phase structure inside the gauge-invariance derivation, directly supporting the claim that U(1) emerges as the continuous limit of 8-tick shifts. It instantiates the eight-tick octave (T7) from the forcing chain and supplies the concrete phase values needed for the ledger-redundancy account of gauge symmetry. No downstream theorems yet consume it, leaving the non-Abelian extension and continuous-limit construction as open follow-on work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.