phase_rigidity
plain-language theorem explainer
Phase rigidity shows that on a connected graph, vanishing reduced phase potential J̃(λ, Θ_v − Θ_w) on every edge forces the phase field Θ to differ by an integer between any pair of vertices. Researchers deriving global co-identity constraints from scale-invariant energies cite this to obtain compact phase structure. The argument first converts edge conditions to integer differences via the zero characterization of J̃, then propagates them by induction along paths in the reflexive-transitive closure of adjacency.
Claim. Let $(V, adj)$ be a graph such that the reflexive-transitive closure of $adj$ relates every pair of vertices. For real parameter $λ ≠ 0$ and phase function $Θ : V → ℝ$, if the reduced phase potential satisfies $J̃(λ, Θ(v) − Θ(w)) = 0$ whenever $adj(v, w)$, then for all $v, w ∈ V$ there exists an integer $n$ with $Θ(v) − Θ(w) = n$.
background
The reduced phase potential is defined by $J̃(λ, δ) = cosh(λ · distZ(δ)) − 1$, where distZ(δ) denotes distance to the nearest integer and λ = ln b for the discrete scaling base b. This construction encodes phase mismatch under the quotient x ∼ b^n x in the GCIC paper, Section IV. The module supplies the auxiliary facts J̃ ≥ 0, periodicity, and the key zero characterization: J̃(λ, δ) = 0 if and only if δ is integer when λ ≠ 0.
proof idea
The proof first invokes Jtilde_zero_iff (with the hypothesis λ ≠ 0) to obtain an integer difference on every adjacent pair. It then performs induction on the reflexive-transitive closure of adjacency supplied by the connectedness hypothesis. The reflexive base case yields difference zero; each tail step adds the integer offset from the new edge via integer arithmetic and linarith.
why it matters
This theorem supplies the phase-rigidity step required by gcic_global_phase_unique in GlobalCoIdentityConstraint, which derives the global co-identity constraint under the GCIC edge condition. It corresponds to RESULT 3 of Thapa–Washburn (2026), Section IV, on rigidity and compact phase emergence in scale-invariant ratio-based energies. In the Recognition Science setting it closes a link between the J-cost functional and the emergence of discrete phase structure, supporting later steps toward the eight-tick octave and three-dimensional spatial emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.