AgreesOnExp
plain-language theorem explainer
AgreesOnExp states that a function F matches Jcost at every exponential argument exp(t). Researchers extending cost agreement properties cite this predicate when moving from the exponential line to the full positive reals. It is realized as a direct definition of a Prop via universal quantification over t.
Claim. A map $F : ℝ → ℝ$ satisfies the condition if $F(ℝ.exp t) = Jcost(ℝ.exp t)$ for all real $t$, where $Jcost(x) = (x + x^{-1})/2 - 1$.
background
Jcost is defined by Jcost(x) := (x + x^{-1})/2 - 1. This expression is the unique cost satisfying the Recognition Composition Law after the T5 J-uniqueness step in the forcing chain. The Cost.JcostCore module collects core properties that candidate cost functions must obey to match this canonical form. Upstream results supply auxiliary F definitions from physics anchors and lepton derivations, yet the present predicate isolates agreement on the exponential image.
proof idea
The declaration is a pure definition. It introduces the Prop by direct quantification over the real parameter t without invoking any lemmas or tactics.
why it matters
This predicate acts as the central interface for agreement results in the cost layer. Downstream theorems such as agree_on_exp_extends and agrees_on_exp_of_bounds rely on it to extend equality from the exponential to all positive reals. It supports the AveragingAgree and AveragingDerivation classes and ties directly to the J-uniqueness step (T5) in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.