Verification Cosh Properties Cert

Verification cosh properties cert

The hyperbolic cosine function, written cosh, is the average of the exponential function and its reciprocal: cosh t = (e^t + e^-t)/2. It describes the shape of a hanging cable under gravity, known as a catenary. The verification cosh properties cert is a machine-checked certificate inside the Recognition Science framework's library of formal theorems. It establishes three specific facts about cosh: its value at zero is 1, its derivative at zero is 0, and its second derivative equals the function itself for every real input.

The reason these three facts matter is the uniqueness theorem for second-order differential equations. That theorem states: if a function H satisfies H'' = H with H(0) = 1 and H'(0) = 0, then H must be cosh. But the theorem is only useful if such a function actually exists. If no function met those conditions, the uniqueness claim would be empty. The certificate closes that gap by verifying that cosh itself satisfies the equation and both initial conditions, so the uniqueness theorem applies to a real, concrete function.

The certificate's proof follows directly from the definitions. Since cosh(0) = (1 + 1)/2 = 1 and sinh(0) = (1 - 1)/2 = 0, the initial conditions hold. The derivative of cosh is sinh, and the derivative of sinh is cosh, so the second derivative of cosh is cosh itself. These steps are encoded in the framework's library as a formal structure named CoshPropertiesCert, with a theorem that the certificate's verification predicate holds for any instance. The library checks each step against its foundational axioms, so the result is not an informal argument but a kernel-verified proof.

Within the Recognition Science framework, this certificate is a small but necessary link in a longer chain. The framework derives physical structure from a ledger of recognition events, and its forcing chain leads to constants and dimensional results. Before that chain can rely on the uniqueness theorem for the differential equation, it must know the equation has a solution. This certificate supplies that knowledge. It is a piece of infrastructure: unglamorous, but without it the later derivations would rest on a theorem with no verified instance.

structure CoshPropertiesCert where
  deriving Repr

What this page does not claim

The certificate does not prove the uniqueness theorem itself, only that cosh satisfies its conditions. The certificate does not derive the hyperbolic functions from Recognition Science principles; it uses the standard real analysis definitions. The certificate does not establish any physical result about the framework's constants or dimensions.

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/Verification/CoshPropertiesCert.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: