curvature_pos
The lemma establishes that modal curvature is strictly positive for every valid configuration in the ILG parameter space. Researchers analyzing modal stability or possibility-space geometry in Recognition Science cite this to rule out sign changes in curvature. The proof is a short tactic sequence that unfolds the curvature definition, applies the inverse-positivity rule to the configuration's positivity field, and finishes with the positivity tactic.
claimFor every configuration $c$ in the ILG parameter space, the modal curvature satisfies $0 < 1/c.value$, where $c.value > 0$ by the configuration hypothesis.
background
ModalGeometry builds the geometry of possibility and actualization spaces on top of the ILG Config structure, whose fields (upsilonStar, eps_r, eps_v, eps_t, eps_a) calibrate modal evolution. The curvature function is introduced as the reciprocal of the configuration value, inheriting positivity directly from that value. Upstream results supply the supporting structures: PhiForcingDerived for J-cost calibration, SpectralEmergence for the forced gauge and generation content, LedgerFactorization for the underlying (R+, ×) monoid, and the astrophysics tiers that embed nuclear densities on the phi-ladder.
proof idea
The term proof unfolds possibility_curvature, introduces the auxiliary fact 0 < c.value^{-1} via inv_pos.mpr applied to c.pos, and closes with the positivity tactic.
why it matters in Recognition Science
The result supplies the curvature-positivity hypothesis required by StabilityHypotheses in the DAlembert stability theorem. It sits inside the modal layer of the forcing chain (T5–T7) where the eight-tick period and positive J-cost together guarantee consistent actualization; the lemma closes one local positivity gap before the global stability argument proceeds.
scope and limits
- Does not compute a numerical value for the curvature.
- Does not apply when the configuration value is non-positive.
- Does not address curvature outside the modal geometry setting.
formal statement (Lean)
123lemma curvature_pos (c : Config) : 0 < possibility_curvature c := by
proof body
Term-mode proof.
124 unfold possibility_curvature
125 have h1 : 0 < c.value⁻¹ := inv_pos.mpr c.pos
126 positivity
127
128/-! ## Modal Nyquist Theorem -/
129
130/-- **8-TICK PERIOD**: The fundamental period of modal evolution. -/