kappa
plain-language theorem explainer
kappa supplies the stiffness constant κ = (log φ)^2 for annular J-cost models and log-spiral parameterizations. Researchers working on flight geometry and lambda derivations cite it when setting per-turn multipliers to φ^κ. The declaration is a direct noncomputable assignment with no proof steps or computational reduction.
Claim. $κ := (log φ)^2$, where φ is the golden ratio and log denotes the natural logarithm.
background
The Annular J-Cost Framework introduces phiCost u := cosh((log φ)·u) − 1, which equals J(φ^u) and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). kappa serves as the stiffness parameter inside SpiralField.Params, controlling exponential growth rates in log-spiral constructions. The module setting centers on φ-weighted costs, annular sampling, Jensen coercivity bounds, and carrier-budget interfaces for topological cost covering.
proof idea
The declaration is a direct definition that assigns (Real.log phi)^2 to kappa with no lemmas or tactics applied.
why it matters
kappa feeds the unique lambda root in balance_determines_lambda and supplies the parameter for kappa_discreteness, perTurn_ratio, and stepRatio_invariant_under_r0. It anchors the logarithmic scaling that links J-cost to the phi-ladder and eight-tick octave, enabling discrete pitch families via integer shifts that multiply per-turn ratios by φ^d. The definition closes the stiffness interface required for annular excess decomposition and trace-based carrier budgets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.