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

possibility_curvature

show as:
view Lean formalization →

The possibility curvature assigns to each configuration the real number given by the sum of the squared reciprocal and fourth-power reciprocal of its value. Modal geometers cite this when quantifying the local spread of possibilities around a state. The definition is a direct algebraic expression that matches the second derivative of the J-cost function evaluated at the configuration value.

claimLet $c$ be a configuration with positive real value $v$. The possibility curvature is the function assigning to $c$ the real number $v^{-2} + v^{-4}$.

background

In the ModalGeometry module, a configuration is a point in recognition state space specified by a positive real value that generalizes the bond multiplier, together with a positivity constraint. The identity event from ObserverForcing sits at the J-cost minimum where the state equals 1. This curvature definition draws on the Config structure imported from the Possibility module and supplies the local geometry for possibility space.

proof idea

The definition is given directly by the algebraic expression consisting of the sum of the squared reciprocal and the fourth-power reciprocal of the configuration value. No lemmas are applied.

why it matters in Recognition Science

This definition supplies the curvature function used to construct the modal manifold and invoked by the lemmas curvature_at_identity and curvature_pos. It realizes the second derivative of the J-cost in the modal setting, supporting analysis of possibility spread within the Recognition Science forcing chain. It touches the open question of extending the simplified Config to full LedgerState representations.

scope and limits

formal statement (Lean)

 114noncomputable def possibility_curvature (c : Config) : ℝ :=

proof body

Definition body.

 115  c.value⁻¹^2 + c.value⁻¹^4
 116
 117/-- Curvature at identity. -/

used by (5)

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

depends on (5)

Lean names referenced from this declaration's body.