possibility_curvature
plain-language theorem explainer
possibility_curvature assigns to each configuration c the real number 1 over c.value squared plus 1 over c.value to the fourth, which equals the second derivative of the J-cost at that point. Modal geometers cite it when they quantify local spreading of possibilities around a recognition state. The definition is supplied as a direct algebraic expression with no lemmas or reductions required.
Claim. For a configuration $c$ with positive real value $v$, the possibility curvature is the real number $v^{-2} + v^{-4}$.
background
In ModalGeometry, a Config is a point in recognition state space carrying a positive real value (generalizing the bond multiplier) together with a positivity witness. The J-cost is the recognition cost function minimized at the identity event (state equal to 1) whose second derivative supplies the curvature. The module imports Possibility and Actualization to equip these points with modal structure on top of recognition events from ObserverForcing.
proof idea
The definition is a direct algebraic encoding of the second derivative expression; no lemmas are applied and the body is the explicit formula in the configuration value.
why it matters
This supplies the curvature function that equips the ModalManifold structure and appears in standard_modal_manifold, curvature_at_identity, and curvature_pos. It fills the local-geometry step that links the J-uniqueness property (T5) to modal extensions of the forcing chain. Downstream lemmas use it to establish positivity and to define the metric on possibility space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.