phase_alignment_minimizes_Jtilde
plain-language theorem explainer
The result establishes that the reduced phase potential J̃(λ, δ) attains its global minimum value of zero precisely when the phase difference δ is an integer. Researchers deriving the Global Co-Identity Constraint from the J-cost forcing chain cite this inequality to replace an empirical assumption with a derived property of aligned configurations. The short tactic proof evaluates J̃ at δ = 0 to obtain zero and then invokes the non-negativity lemma Jtilde_nonneg.
Claim. For all real numbers λ and δ, the reduced phase potential satisfies $J̃(λ, 0) ≤ J̃(λ, δ)$.
background
The GCIC derivation module obtains the Global Co-Identity Constraint as a theorem of the RS forcing chain with zero empirical axioms. The reduced phase potential J̃ is built from the distance function distZ on the circle; it encodes the collective cost of phase mismatches under the eight-tick discrete gauge. Upstream results supply the phase definition (kπ/4 for k = 0..7) and the unimodular complex representation e^{i w} used to close the gauge.
proof idea
The tactic proof first unfolds Jtilde and distZ, then simplifies with Int.fract_zero and Real.cosh_zero to obtain the identity Jtilde lam 0 = 0. It concludes by applying the lemma Jtilde_nonneg lam δ.
why it matters
The theorem supplies the first conjunct of gcic_derivation_cert, which certifies collective subadditivity (Jcost 1 < sum of positive costs) and replaces an empirical axiom. It fills the module step “aligned phases minimize J̃” that connects T5 J-uniqueness through ratio rigidity and compact phase to the GCIC. The parent gcic_derivation_cert packages the result with aligned_beats_perturbed to obtain the full certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.