kappa_pos
plain-language theorem explainer
kappa_pos asserts that the annular stiffness constant κ = (log φ)² is strictly positive. Researchers certifying the continuum limit of the simplicial ledger cite it to confirm the Einstein coupling remains positive. The proof is a term-mode reduction that unfolds the definition of kappa, invokes Real.log_pos on the upstream fact 1 < φ, and closes with nlinarith.
Claim. Let φ > 1 denote the golden ratio. Define the stiffness constant by κ := (log φ)². Then κ > 0.
background
The Annular J-Cost Framework introduces phiCost u := cosh((log φ)·u) − 1, which equals J(φ^u) under the Recognition Composition Law. The stiffness constant kappa is defined locally as (Real.log phi)² to furnish the quadratic lower bound phiCost u ≥ κ u²/2. This lemma depends on the upstream result one_lt_phi, which establishes 1 < φ from the quadratic irrationality of the golden ratio, together with the positivity of the real logarithm.
proof idea
The term-mode proof unfolds kappa to (log phi)². It applies Real.log_pos to the lemma one_lt_phi to obtain 0 < log phi. nlinarith then concludes that the square is positive.
why it matters
kappa_pos supplies the positivity hypothesis required by ContinuumBridgeCert and ContinuumFieldCurvatureCert, which certify that J-cost stationarity on the simplicial ledger yields the Einstein field equations with coupling 8 φ⁵. It thereby closes the positivity step in the annular cost layer that supports the T5–T8 forcing chain and the transition from discrete ledger to continuum curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.