gcic_kappa
plain-language theorem explainer
gcic_kappa supplies the explicit stiffness value κ = (ln φ)²/2 for the reduced phase potential in the GCIC framework. Workers on global co-identity constraints and phase rigidity in scale-invariant systems cite this when establishing quadratic lower bounds on the J̃ potential. The definition is a direct one-line expression in terms of the golden-ratio logarithm from the Constants bundle.
Claim. The GCIC stiffness constant is defined by $κ = (ln φ)^2 / 2$, where φ denotes the golden ratio.
background
The module formalizes the reduced phase-mismatch potential J̃_b(δ) = cosh(lam · d_ℤ(δ)) − 1, where lam = ln b and d_ℤ(δ) is the distance to the nearest integer. This κ is identified as the small-gradient stiffness lower bound for J̃. The upstream Constants structure from LawOfExistence bundles the fundamental CPM parameters, including phi.
proof idea
Direct definition as (log Constants.phi)^2 / 2.
why it matters
This definition supplies the explicit value of the stiffness parameter used in gcic_kappa_pos to prove positivity and in gcic_global_phase_independent_of_path to establish path independence of the global phase. It fills the role of the lower bound κ = lam²/2 in the GCIC paper Section IV, supporting the phase rigidity result in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.