phi_coupling_stiffness
plain-language theorem explainer
GCIC stiffness for base φ supplies a quadratic lower bound on the phase-adjusted J-cost Jtilde at logarithmic scale for arbitrary real deviation δ. Derivations of the Global Co-Identity Constraint from the forcing chain cite this bound when establishing collective cost subadditivity. The argument is a one-line term application of the general Jtilde stiffness lower bound lemma.
Claim. For any real number $δ$, $((ln φ) · dist_Z(δ))^2 / 2 ≤ J̃((ln φ), δ)$, where φ is the golden-ratio constant from the CPM bundle, dist_Z is distance to the nearest integer, and J̃ is the phase-adjusted J-cost function.
background
The module derives the Global Co-Identity Constraint from the J-cost forcing chain with zero empirical axioms. Key upstream results include the Constants structure bundling CPM parameters with non-negativity, the cost function on multiplicative recognizers, and the J-cost of recognition events. The local setting is the chain T5 (J-uniqueness) to ratio rigidity to compact phase Θ ∈ ℝ/ℤ, yielding uniform Θ at J-stationarity.
proof idea
The proof is a one-line term wrapper that applies the lemma Jtilde_stiffness_lb at the logarithmic phi scale and the supplied deviation δ.
why it matters
This supplies the base-case stiffness bound for the phi scale inside the GCIC derivation, feeding directly into phase_alignment_minimizes_Jtilde and aligned_collective_cost_zero. It closes the link from T5 J-uniqueness through ratio rigidity to the uniform phase constraint of the forcing chain. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.