CurvatureType
plain-language theorem explainer
CurvatureType enumerates the three constant-curvature classes for the log-coordinate cost function G(t). Researchers deriving geometry from the Recognition Composition Law cite the classification when ruling out flat and spherical solutions under non-negativity. The inductive definition directly encodes the second-derivative conditions G'' = 1, G'' = G + 1, and G'' = -(G + 1) with no further computation.
Claim. An inductive type with three constructors: flat (zero curvature, second derivative of cost function equals 1), hyperbolic (curvature -1, second derivative equals cost function plus 1), spherical (curvature +1, second derivative equals negative of cost function plus 1).
background
The module sets the Curvature Gate: the cost metric must have constant nonzero curvature. Log-coordinate reparametrization defines G(t) = F(e^t) so that the metric is ds² = G''(t) dt². Flat space gives independent comparisons with G(t) = t²/2; hyperbolic space gives entangled comparisons with G(t) = cosh(t) - 1; spherical space is periodic and violates non-negativity of F.
proof idea
This is an inductive definition with three constructors, each carrying an inline comment on the associated curvature and second-derivative condition. It derives DecidableEq and Repr. No lemmas from upstream results are applied; the definition stands alone as a type for later case analysis.
why it matters
The definition supplies the classification that forces the hyperbolic case G(t) = cosh(t) - 1 under non-negativity and interaction, thereby realizing the Recognition Composition Law. It aligns with J-uniqueness (T5) and supplies the geometric step toward D = 3. No downstream theorems are recorded, leaving open its use in theorems on the phi-ladder and mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.