Verification Jcost Satisfies Jensen Cert

The uniqueness certificate

The cost function J(x) = (x + 1/x)/2 - 1 plays a central role in Recognition Science as the unique function satisfying five plain conditions. The verification module JcostSatisfiesJensenCert closes a logical loop: it proves that Jcost itself satisfies all the requirements of the JensenSketch interface, a formal specification of those conditions. This is a machine-checked certificate, meaning a computer program has verified every step of the proof.

The JensenSketch requirements are four: symmetry, meaning J(x) = J(1/x) for all positive x; unit normalization, meaning J(1) = 0; and two axis bounds that are trivially satisfied for Jcost because they hold by reflexive equality. The symmetry and unit normalization are proven algebraically from the explicit formula. The certificate then constructs an instance jcost_jensen_sketch that packages these proofs into the required interface.

This certificate matters because it completes the T5 uniqueness theorem. That theorem states: any function F satisfying JensenSketch equals Jcost on (0, ∞). But this is conditional on F satisfying the requirements. This certificate proves Jcost does satisfy them. Together, these establish that Jcost is THE unique cost function satisfying these axioms, not merely one among many.

In plain language: imagine the system tracks records for the universe, and the cost of recognizing an event is forced by five simple rules. This certificate is the final audit showing that those rules point to exactly one cost function, and that function is J(x) = (x + 1/x)/2 - 1. The proof is definitional, meaning it follows directly from the formula, and every step is verified by the machine-checked library of formal theorems.

structure JcostSatisfiesJensenCert where
  deriving Repr

/-- The Jcost instance can be explicitly constructed from the verified properties. -/
def jcost_jensen_sketch : JensenSketch Jcost :=
  { symmetric := fun hx => Jcost_symm hx
  , unit0 := Jcost_unit0
  , axis_upper := fun _ => le_refl _
  , axis_lower := fun _ => le_refl _ }

structure JcostSatisfiesJensenCert where
  deriving Repr

What this page does not claim

This certificate does not prove the T5 uniqueness theorem itself, only that Jcost satisfies its requirements. This certificate does not derive the value of any physical constant or make empirical predictions.

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/JcostSatisfiesJensenCert.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: