compactPhase_gauge_invariant
plain-language theorem explainer
The compact phase Θ(r) is unchanged under addition of any integer multiple of ln φ to the log-ratio r. Researchers deriving discrete gauge symmetries from the Recognition forcing chain cite this to treat Θ as a function on the quotient ℝ/(ln φ)ℤ. The proof is a direct algebraic reduction that rewrites the normalized argument and applies the integer-shift rule for the fractional part.
Claim. Let Θ(r) := {r / ln φ} denote the fractional part. Then Θ(r + n ln φ) = Θ(r) for every real r and integer n.
background
The DiscreteGauge module derives the discrete gauge r ~ r + n ln φ from T6 (φ-self-similarity) and T7 (8-tick neutrality) in the GCIC response. The compact phase is defined by Θ(r) = fract(r / ln φ), which folds the log-ratio onto the unit interval. The upstream result log_phi_ne_zero supplies ln φ ≠ 0 so that division is valid; the module_doc states that this construction converts the φ-lattice periodicity into a compact Brillouin zone without manual imposition of periodicity.
proof idea
Unfold the definition of compactPhase. Rewrite the scaled argument via add_div and mul_div_cancel_of_imp using log_phi_ne_zero to obtain r/ln φ + n. Apply Int.fract_add_intCast to absorb the integer n into the fractional part.
why it matters
The result confirms that the compact phase descends to the quotient forced by T6+T7, closing the explicit-input gap noted in the GCIC paper. It supplies the invariance step required for the 8-tick compactification theorem and the Bloch analogy in the module_doc. Within the Recognition framework it anchors the discrete gauge as a derived consequence of the eight-tick octave rather than an added assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.