pith. machine review for the scientific record. sign in
def definition def or abbrev high

kappa

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  59noncomputable def kappa : ℝ := (Real.log phi) ^ 2

proof body

Definition body.

  60

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.