canonicalTrajectory_net_zero
plain-language theorem explainer
The canonical trajectory for integer n realizes an n-fold ln φ displacement over eight ticks yet carries zero net physical quantity. Researchers closing the discrete gauge gap in the GCIC paper cite this to confirm neutrality follows from T6 and T7. The proof is a one-line application of the net_physical_zero property of ValidTrajectory to the canonicalTrajectory construction.
Claim. For any integer $n$, the net physical quantity of the trajectory realizing an $n$-fold displacement by $n·ln φ$ in eight ticks vanishes: netPhysical(canonicalTrajectory $n$) = 0.
background
The module derives Mechanism A of the GCIC Response paper: the discrete identification $r ~ r + n·ln φ$ ($n ∈ ℤ$) follows from φ-self-similarity (T6: each tick changes log-ratio by integer multiple of ln φ) and 8-tick neutrality (T7: sum of eight consecutive changes is zero). The canonical trajectory is the explicit 8-tick path satisfying ValidTrajectory that achieves exactly this displacement. Upstream results include the tick definition (fundamental time quantum τ₀ = 1) and IntegrationGap.A (active edge count per tick, with φ-power balance at D = 3). The local setting is the Bloch-analog derivation of compact phase Θ ∈ ℝ/ℤ from the φ-lattice and crystal period without imposing periodicity by hand.
proof idea
The proof is a one-line wrapper that applies ValidTrajectory.net_physical_zero directly to the instance (canonicalTrajectory n).
why it matters
This result supplies the neutrality half of the 8-tick compactification theorem stated in the module doc-comment, showing that the orbit {r + n·ln φ} is dynamically equivalent under valid trajectories. It closes the acknowledged Gap A in the GCIC paper by deriving the gauge from T6+T7 rather than as an input. In the Recognition framework it anchors the eight-tick octave (T7) and supports the compact phase construction used in downstream discrete gauge arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.