constant_field_constant_phase
plain-language theorem explainer
If a real-valued field on vertices is constant, the compact phase of its logarithm is identical at every vertex. This lemma supports the GCIC main result by showing constancy of the field propagates directly to the phase. The proof is a one-line rewrite that substitutes the constant value into both phase expressions.
Claim. Suppose the function $x : V → ℝ$ satisfies $x(v) = x(w)$ for all vertices $v, w$. Then the compact phase of $log(x(v))$ equals the compact phase of $log(x(w))$.
background
The GCIC derivation module extracts the Global Co-Identity Constraint from the RS forcing chain without empirical axioms. It proceeds from T5 J-uniqueness (ratio rigidity at J=0) through T6+T7 compact phase in ℝ/ℤ to uniform Θ at J-stationarity. The compact phase projects the logarithm of the field value onto the discrete gauge, inheriting periodicity from the eight-tick structure.
proof idea
This is a one-line wrapper that applies the rewrite tactic to the constancy hypothesis, equating the two arguments of compactPhase.
why it matters
The lemma is invoked inside gcic_from_forcing_chain, the module's main theorem that at J-cost minimum all vertices share the same compact phase Θ₀. It completes the step from constant field (T5) to constant phase (T6+T7) and thereby closes the GCIC derivation. The result sits inside the eight-tick octave and discrete-gauge portion of the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.