Cost Ndim Scalar Certificates R0101 Closed Neg

A curvature certificate

In differential geometry, a surface is flat when it can be unfolded into a plane without stretching or tearing. The Recognition Science library contains a machine-checked theorem, R0101Closed_neg, that proves a specific family of surfaces is never flat. The family is built from a potential function Φ_λ(t₀, t₁) = cosh t₀ + cosh t₁ + λ(cosh(t₀+t₁) − 1), where λ is a positive parameter. The theorem states that a particular component of the Riemann tensor, the object that measures curvature, is strictly negative for every nonzero point on the slice t₁ = 0.

The proof works by deriving a closed-form scalar expression for that curvature component: R⁰₁₀₁(t, 0, λ) = −λ sinh²t (λ cosh t + 1) / (4 cosh²t (λ cosh t + λ + 1)²). Because the numerator is always negative and the denominator always positive for λ > 0 and t ≠ 0, the whole expression is always negative. This is a certificate: one formula that establishes non-flatness for every parameter value at once, rather than checking isolated points one by one. The theorem is tagged THEOREM in the framework's library, meaning it is a proved result with no unverified assumptions.

The declaration does not claim that the geometric identification between this scalar formula and the actual tensor component is proved in this file. That bridge, connecting the closed form to the Hessian/Shima curvature formula, is recorded as a hypothesis-level fact elsewhere. The theorem also does not say anything about the physical meaning of non-flatness for recognition cost; it is a pure mathematical statement about a defined family of metrics. It applies only on the specified 2-dimensional slice with t₁ = 0, not to the full space.

What this certificate buys is efficiency and certainty. A single scalar inequality, verified by the machine-checked library, replaces an infinite family of pointwise checks. The result is a building block: future work can rely on this non-flatness fact without re-deriving it, and the framework's account of why recognition cost cannot be trivial gains a solid geometric foundation.

/-- **Theorem 2** (non-flatness of `h_λ`, 2D case): the Riemann tensor component
    `R^0_{1,0,1}` is strictly negative for every `λ > 0` and `t ≠ 0`. Hence `h_λ` is
    not flat. This matches the SymPy-verified value `R^0_101(5/4,3/4,1) = -81/4225`
    (i.e. `R0101Closed t 1 = -81/4225` at `cosh t = 5/4`, `sinh t = 3/4`). -/
theorem R0101Closed_neg (t lam : ℝ) (hlam : 0 < lam) (ht : t ≠ 0) :
    R0101Closed t lam < 0 := by
  unfold R0101Closed
  have hc : 0 < Real.cosh t := Real.cosh_pos t
  have hs_ne : Real.sinh t ≠ 0 := Real.sinh_ne_zero.mpr ht
  have hs2_pos : 0 < (Real.sinh t) ^ 2 := sq_pos_of_ne_zero hs_ne
  have h_lc1 : 0 < lam * Real.cosh t + 1 := by nlinarith
  have h_lc2 : 0 < lam * Real.cosh t + lam + 1 := by nlinarith
  have h_den : 0 < 4 * (Real.cosh t) ^ 2 * (lam * Real.cosh t + lam + 1) ^ 2 := by
    positivity
  have hpos : 0 < lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1) :=
    mul_pos (mul_pos hlam hs2_pos) h_lc1
  have h_num : -(lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1)) < 0 := by linarith
  exact div_neg_of_neg_of_pos h_num h_den

/-- `R^0_{1,0,1}` at the slice point `(t, 0)`, `α = (1,1)`, general `λ`. -/
def R0101Closed (t lam : ℝ) : ℝ :=
  -(lam * (Real.sinh t) ^ 2 * (lam * Real.cosh t + 1)) /
    (4 * (Real.cosh t) ^ 2 * (lam * Real.cosh t + lam + 1) ^ 2)

What this page does not claim

The geometric bridge identifying the scalar formula with the actual tensor component is not proved in this file. The theorem says nothing about the physical meaning of non-flatness for recognition cost. The result applies only on the specified 2-dimensional slice, not to the full space.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/ScalarCertificates.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: