global_phase
plain-language theorem explainer
Global phase on a ledger state is fixed at the real value 0, independent of the underlying eight-tick signal. Anyone assembling the recognition operator or reading phase-sensitive update rules cites this as the gauge choice. The body is a constant definition, not a derived identity.
Claim. For every ledger state $s$ (an eight-tick signal configuration), the associated global phase is the real number $0$: $\mathrm{global\_phase}(s) := 0$.
background
In this module a ledger state is abbreviated to Signal8, the eight-component discrete signal that carries one octave of recognition data. Sibling projections on that state include time, Z-patterns, channels, and active bonds; global phase sits beside them as a real-valued readout.
Elsewhere in the monolith, LedgerState appears with richer structure (configuration plus tick, lists of recognition events, or active bonds with positive multipliers). Those variants track conserved log-ratio charge or total recognition cost. Here the foundation layer collapses the state to the bare eight-tick carrier and treats global phase as an external real label.
Setting that label identically to zero is the standard U(1) gauge fix: only relative phases among channels matter for the projector-then-shift dynamics that the recognition operator will apply.
proof idea
There is no proof. The declaration is a constant function: the ledger-state argument is ignored and the real literal 0 is returned. No lemmas are invoked.
why it matters
The recognition operator structure consumes this readout when it packages the bare one-tick propagation map on eight-tick signals. A fixed zero global phase keeps the operator record free of an unobservable overall U(1) factor, so sector data and bond multipliers determine the update alone.
In the broader forcing chain the eight-tick octave (T7) already fixes the discrete period; pinning global phase to zero is the continuous counterpart of that discreteness choice. It does not itself force dimension, $\varphi$, or the J-cost, but it keeps phase bookkeeping consistent with those later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.