T5_cost_uniqueness_on_pos
plain-language theorem explainer
Any function F obeying the JensenSketch bounds on the exponential axis must coincide with the J-cost function for every positive real argument. Physicists deriving the cost structure in Recognition Science would invoke this uniqueness result when fixing the functional form of J. The short proof first obtains exact agreement on the exponential line by antisymmetrizing the upper and lower bounds, then extends the equality to all positive x via the extension lemma.
Claim. Let $F : ℝ → ℝ$ satisfy the JensenSketch axioms. Then for all $x > 0$, $F(x) = (x + x^{-1})/2 - 1$.
background
The J-cost function is defined by Jcost(x) := (x + x^{-1})/2 - 1. JensenSketch is a class extending SymmUnit that supplies the two-sided bounds axis_upper and axis_lower: F(exp t) ≤ Jcost(exp t) and Jcost(exp t) ≤ F(exp t) for all real t. AgreesOnExp is the proposition asserting exact equality F(exp t) = Jcost(exp t) for all t.
proof idea
The tactic proof introduces x and hx, builds an AgreesOnExp hypothesis by applying le_antisymm to the axis_upper and axis_lower fields of the JensenSketch instance, then calls the upstream theorem agree_on_exp_extends on that hypothesis.
why it matters
This theorem supplies the uniqueness half of the T5 J-uniqueness step in the forcing chain. It shows that the cost functional is rigidly determined once the JensenSketch inequalities are imposed. The result feeds into downstream derivations of the phi-ladder and mass formulas in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.