Papers Gcic Reduced Phase Potential

Reduced phase potential

The reduced phase potential is a cost function that measures how far a phase value sits from being an integer. It is written J̃(λ, δ) = cosh(λ · d_ℤ(δ)) − 1, where d_ℤ(δ) is the distance from δ to the nearest integer and λ = ln b for the base b of a discrete scaling quotient. The function is periodic with period 1, is always nonnegative, and vanishes exactly when δ is an integer, provided λ is nonzero. These properties are established in Lean 4 in the module IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean.

The potential is called reduced because it works on the quotient where phases that differ by an integer are identified. This matches the discrete scaling structure x ~ bⁿx, so the cost depends only on the fractional part of the phase difference. The small-gradient behavior is controlled by a stiffness constant κ = λ²/2: near an integer, the potential grows at least quadratically with the distance to that integer. For the golden ratio base φ, the stiffness is κ = (ln φ)²/2, which is established positive.

The central structural result is phase rigidity. On any finite connected graph, if the reduced phase cost vanishes on every edge, then the phase field is constant modulo integers. That is, the zero set of the potential is so small that a connected network cannot host a nonconstant phase field without paying positive cost somewhere. This follows from the nonnegativity and the unique-zero characterization of J̃. The theorem is tagged THEOREM and is anchored to phase_rigidity in the same module.

In plain terms, the module establishes that a periodic, nonnegative cost with a unique zero at integer values forces global phase alignment on connected structures. This is a rigidity statement: the discrete scaling quotient leaves no room for phase gradients. The stiffness bound quantifies how quickly the cost rises when phases deviate from integers, which is the mechanism behind the rigidity.

THEOREM Jtilde · IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean

THEOREM Jtilde_periodic · Jtilde_nonneg · Jtilde_zero_iff · IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean

THEOREM Jtilde_stiffness_lb · IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean

THEOREM phase_rigidity · IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean

What this page does not claim

This answer does not claim the reduced phase potential is the same as the full J(x) cost function. This answer does not claim phase rigidity holds for disconnected graphs. This answer does not claim the stiffness constant is derived from the forcing chain; it is defined for the golden ratio base.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Papers/GCIC/ReducedPhasePotential.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: