curvature_at_identity
plain-language theorem explainer
The lemma establishes that possibility curvature evaluates to exactly 2 at the identity configuration. Modal geometry work in Recognition Science cites this when anchoring local geometry near minimal-cost points. The proof reduces by direct unfolding of the curvature definition at value 1 followed by algebraic simplification.
Claim. Let $κ(c) = c^{-2} + c^{-4}$ denote curvature of possibility space at configuration $c$. Then $κ$ at the identity configuration (value 1) equals 2.
background
In ModalGeometry, possibility_curvature is the noncomputable function $κ(c) = c.value^{-2} + c.value^{-4}$, interpreted as the second derivative of the J-cost at the configuration value. identity_config constructs the minimal-cost point with value 1 and zero log term. The module imports Possibility and Actualization; the lemma depends on the algebraic definitions of both curvature and the identity point.
proof idea
Term-mode proof: simp unfolds possibility_curvature and identity_config (with inv_one and one_pow), then ring normalizes the resulting expression in one step.
why it matters
The result supplies the concrete numerical value 2 at the identity, matching the explicit statement in the curvature definition. It anchors modal geometry calculations within the Recognition framework's J-cost structure and supports downstream positivity claims for curvature. No used_by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.