J
plain-language theorem explainer
The canonical recognition cost is introduced as the function J mapping each real number x to (x plus its reciprocal) divided by two, minus one. Researchers building domain certificates or the master cert chain cite this definition to avoid repeating the cost expression. It is supplied as a direct algebraic abbreviation with no auxiliary lemmas.
Claim. The canonical recognition cost function is given by $J(x) = (x + x^{-1})/2 - 1$ for $x$ real.
background
The Canonical J-Cost Band module supplies a reusable six-clause template applied to any ratio in the master certification chain. The clauses cover J(1) equals zero, non-negativity for positive arguments, equality under reciprocal, strict positivity away from unity, positivity at the golden ratio, and the narrow band containing J at the golden ratio. This definition of J supplies the common cost expression so that each domain-specific certificate can define its own ratio and then invoke the shared properties.
proof idea
The declaration consists of a single-line definition that directly equates J(x) to the stated algebraic combination of x and its reciprocal. No tactics or lemmas are invoked because the body is the primitive expression itself.
why it matters
This definition provides the base for all six-clause J-cost proofs that appear in B-tier whole-science openings and the domain certificates. It realizes the J-uniqueness landmark in the unified forcing chain, where J is required to take the form (x + 1/x)/2 - 1. The module thereby closes the reusable identities that keep the entire certification tree free of sorry statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.