Cost Ndim Scalar Certificates

Scalar certificates

In differential geometry, proving that a surface is curved or that a direction is not parallel often requires checking a condition at every point. A scalar certificate is a single, explicit formula that settles such a question for all points at once. Instead of testing each location, you compute one expression, show it is always positive or always negative, and the property is established universally.

The Recognition Science framework uses this idea to verify two structural facts about a family of geometries it studies. The family is built from a potential function Φ_λ(t₀,t₁) = cosh t₀ + cosh t₁ + λ(cosh(t₀+t₁) − 1), which defines a metric h_λ and a projector P_λ onto a preferred direction. The module ScalarCertificates provides closed-form expressions for the key tensor components and then proves they never vanish (or are always negative) away from a single exceptional point.

Concretely, the module proves two theorems. First, the projector P_λ is not parallel: its covariant derivative is nonzero for every t ≠ 0, both with respect to the flat connection D and with respect to the Levi-Civita connection ∇^λ of the metric. Second, the metric h_λ is non-flat for λ > 0: the Riemann tensor component R⁰_1,0,1 is strictly negative for every t ≠ 0. The proofs work by writing down explicit formulas such as dP00(t) = −sinh t / (cosh t + 1)² and R0101Closed(t,λ) = −λ sinh²t (λ cosh t + 1) / (4 cosh²t (λ cosh t + λ + 1)²), then showing these expressions are never zero or always negative.

These certificates matter because they turn a pointwise check into a global statement. The closed forms are verified by hand and by symbolic computation against a ground-truth value at one point, and the module proves the nonvanishing and negativity directly from the formulas. This avoids having to construct special points inside the proof system. The identification of these scalar expressions with the actual tensor components is recorded as a hypothesis-level fact, not re-derived in this file, which focuses on the algebraic core.

In Recognition Science, the result supports the broader claim that the golden and metallic λ-family has the geometric structure the framework expects. The scalar certificates establish that the non-parallelism and non-flatness hold universally on the slice, not just at isolated points. This is a necessary step for the framework's account of how recognition costs force geometric structure, though the full physical bridge from these mathematical facts to the three-dimensional world remains an open target.

/-- **Theorem 1a** (non-parallelism of `P_λ` w.r.t. the flat connection `D`):
    the ordinary derivative of the `(0,0)` entry of `P_λ` is nonzero for every `t ≠ 0`.
    Hence `D P_λ ≠ 0`, i.e. `P_λ` is not `D`-parallel. -/
theorem dP00_ne_zero (t : ℝ) (ht : t ≠ 0) : dP00 t ≠ 0 := by
  unfold dP00
  apply div_ne_zero
  · exact neg_ne_zero.mpr (Real.sinh_ne_zero.mpr ht)
  · exact pow_ne_zero 2 (ne_of_gt (by linarith [Real.cosh_pos t]))

/-- **Theorem 1b** (non-parallelism of `P_λ` w.r.t. the Levi-Civita connection `∇^λ`):
    the covariant derivative of the `(0,0)` entry of `P_λ` is nonzero for every `t ≠ 0`.
    Hence `∇^λ P_λ ≠ 0`, i.e. `P_λ` is not `∇^λ`-parallel. -/
theorem nablaP000_ne_zero (t : ℝ) (ht : t ≠ 0) : nablaP000 t ≠ 0 := by
  unfold nablaP000
  have hsinh_ne : Real.sinh t ≠ 0 := Real.sinh_ne_zero.mpr ht
  have hc3_ne : Real.cosh t + 3 ≠ 0 := ne_of_gt (by linarith [Real.cosh_pos t])
  apply div_ne_zero
  · exact mul_ne_zero (neg_ne_zero.mpr hsinh_ne) hc3_ne
  · have h1 : (0:ℝ) < Real.cosh t + 1 := by linarith [Real.cosh_pos t]
    have h2 : (0:ℝ) < Real.cosh t + 2 := by linarith [Real.cosh_pos t]
    positivity

/-- **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 identification of the scalar formulas with the tensor components is not proved in this module; it is a hypothesis-level bridge. The module does not establish the physical significance of the golden ratio or the three-dimensionality of space. The certificates apply only to the 2-dimensional slice α = (1,1), not to the full higher-dimensional geometry.

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: