Jcost
plain-language theorem explainer
Jcost supplies the explicit formula for the central cost function in Recognition Science. It realizes the T5 J-uniqueness step by setting J(x) to the average of x and its reciprocal minus one. Researchers on the forcing chain or phi-ladder cite this as the algebraic root for all cost properties. The declaration is a direct noncomputable definition with no proof obligations.
Claim. The J-cost function on positive reals is defined by $J(x) = (x + x^{-1})/2 - 1$.
background
The Jcost definition sits in the Cost.JcostCore module and introduces the core cost measure for Recognition Science. It matches the closed form given in the T5 landmark of the forcing chain, where J is the unique function satisfying the Recognition Composition Law. The expression is equivalent to cosh(log x) - 1 and serves as the starting point for symmetry, non-negativity, and quadratic bounds proved in sibling declarations.
proof idea
The declaration is a one-line definition that directly assigns the algebraic expression (x + x inverse)/2 minus 1 to Jcost(x).
why it matters
This definition anchors the entire cost domain and feeds the suite of basic lemmas on J-cost. It fills the T5 slot in the UnifiedForcingChain by supplying the explicit J that satisfies the composition law, enabling later steps toward the phi-ladder, eight-tick octave, and D=3. No open questions attach at this foundational level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Captions, not labels: a vision model you steer with a sentence
"CLIP learns a multi-modal embedding space by jointly training an image encoder and text encoder to maximize the cosine similarity of the image and text embeddings of the N real pairs in the batch while minimizing the cosine similarity of the embeddings of the N²−N incorrect pairings. We optimize a symmetric cross entropy loss over these similarity scores."