Cost Ndim Scalar Certificates Has Deriv At P00 Gen

A derivative certificate

In calculus, the derivative of a function measures how its output changes as its input moves. The declaration hasDerivAt_P00Gen is a machine-checked proof that a specific function, written P00Gen, has a derivative at every real number t, provided a parameter a is nonzero. The function itself is a rational expression involving hyperbolic cosine: P00Gen(a, b, t) = a² / (a² + b²·cosh t). The theorem states that its derivative is dP00Gen(a, b, t) = −a²b²·sinh t / (a² + b²·cosh t)², and the proof verifies this using the standard derivative rules for hyperbolic functions and the quotient rule.

Why care about one derivative? This is a certificate inside a larger argument. The function P00Gen appears as a component of a projector, a geometric object that picks out a direction in a curved space. The framework's goal is to show that this projector is not parallel: it changes as you move, rather than staying constant. A key step is to show its derivative is not zero. The theorem hasDerivAt_P00Gen provides the derivative formula; a companion theorem, dP00Gen_ne_zero, then shows that this derivative is nonzero for all nonzero t, given both a and b are nonzero. Together they prove that the projector genuinely varies, a fact that supports the non-parallelism claim.

This declaration is a formal result inside the machine-checked library of the Recognition Science framework. It is a theorem: it is proved from the axioms of real analysis, with no additional assumptions. But it is a narrow result. It does not, by itself, establish the geometric meaning of the function, nor does it prove that the projector is not parallel in a physical sense. Those conclusions rely on additional identifications, recorded elsewhere as hypotheses. The declaration is a self-contained algebraic fact, a small but necessary gear in a larger machine.

What this means for a reader: a single derivative computation, when checked by a computer, can serve as a reliable building block. The framework can point to this certificate and say, here is a fact that is not assumed but derived. The larger claims about geometry and physics rest on many such certificates, each one individually modest, together forming a chain. This declaration is one link in that chain, and its value is in its certainty, not in its size.

/-- `P00Gen a b` is differentiable with derivative `dP00Gen a b`. -/
theorem hasDerivAt_P00Gen (a b t : ℝ) (ha : a ≠ 0) :
    HasDerivAt (P00Gen a b) (dP00Gen a b t) t := by
  have hc : HasDerivAt (fun x => a ^ 2 + b ^ 2 * Real.cosh x) (b ^ 2 * Real.sinh t) t := by
    have := (Real.hasDerivAt_cosh t).const_mul (b ^ 2)
    simpa using this.const_add (a ^ 2)
  have ha2 : (0:ℝ) < a ^ 2 := by positivity
  have hne : a ^ 2 + b ^ 2 * Real.cosh t ≠ 0 := by
    have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
    linarith
  have hnum : HasDerivAt (fun _ : ℝ => a ^ 2) 0 t := hasDerivAt_const t (a ^ 2)
  have := (hnum.div hc hne)
  simpa [P00Gen, dP00Gen, div_eq_mul_inv] using this |>.congr_deriv (by ring)

/-- `P00Gen a b` is differentiable with derivative `dP00Gen a b`. -/
theorem hasDerivAt_P00Gen (a b t : ℝ) (ha : a ≠ 0) :
    HasDerivAt (P00Gen a b) (dP00Gen a b t) t := by
  have hc : HasDerivAt (fun x => a ^ 2 + b ^ 2 * Real.cosh x) (b ^ 2 * Real.sinh t) t := by
    have := (Real.hasDerivAt_cosh t).const_mul (b ^ 2)
    simpa using this.const_add (a ^ 2)
  have ha2 : (0:ℝ) < a ^ 2 := by positivity
  have hne : a ^ 2 + b ^ 2 * Real.cosh t ≠ 0 := by
    have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
    linarith
  have hnum : HasDerivAt (fun _ : ℝ => a ^ 2) 0 t := hasDerivAt_const t (a ^ 2)
  have := (hnum.div hc hne)
  simpa [P00Gen, dP00Gen, div_eq_mul_inv] using this |>.congr_deriv (by ring)

/-- **Theorem 1a, general `α`**: the ordinary derivative of the `(0,0)` entry of `P_λ`
    is nonzero for every `t ≠ 0`, `a ≠ 0`, `b ≠ 0`. Hence `D P_λ ≠ 0` for the whole
    `α = (a, b)` family, not just `α = (1,1)`. -/
theorem dP00Gen_ne_zero (a b t : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (ht : t ≠ 0) :
    dP00Gen a b t ≠ 0 := by
  unfold dP00Gen
  have ha2 : (0:ℝ) < a ^ 2 := by positivity
  have hb2 : (0:ℝ) < b ^ 2 := by positivity
  apply div_ne_zero
  · exact neg_ne_zero.mpr
      (mul_ne_zero (mul_ne_zero (ne_of_gt ha2) (ne_of_gt hb2)) (Real.sinh_ne_zero.mpr ht))
  · have hpos : (0:ℝ) < a ^ 2 + b ^ 2 * Real.cosh t := by
      have : (0:ℝ) ≤ b ^ 2 * Real.cosh t := by positivity
      linarith
    exact pow_ne_zero 2 (ne_of_gt hpos)

What this page does not claim

This declaration does not establish the geometric meaning of P00Gen as a projector component. This declaration does not prove that the projector is not parallel in a physical sense; that relies on additional identifications. This declaration does not apply when the parameter a is zero.

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: