agrees_on_exp_of_bounds
plain-language theorem explainer
Any function F satisfying the averaging bounds condition must agree exactly with the J-cost on the image of the exponential map. Researchers deriving cost equalities in the Recognition Science framework cite this to convert bounding inequalities into pointwise identity. The proof is a short tactic sequence that retrieves the upper and lower bounds, invokes antisymmetry of the order relation, and simplifies.
Claim. Let $F : ℝ → ℝ$ satisfy the averaging bounds condition. Then $F(e^t) = J(e^t)$ for all real $t$, where $J$ denotes the J-cost function.
background
In the Cost module the J-cost supplies the canonical cost measure obtained from the Recognition Composition Law. AveragingBounds is the typeclass that extends SymmUnit F with the two inequalities $F(e^t) ≤ J(e^t)$ and $J(e^t) ≤ F(e^t)$ for every real $t$. AgreesOnExp is the proposition asserting exact equality $F(e^t) = J(e^t)$ on the same domain. The theorem therefore converts the bounding class into the equality proposition. It rests on the antisymmetry lemma for the order relation supplied by the arithmetic foundations.
proof idea
The tactic proof introduces an arbitrary real $t$, obtains the upper bound from AveragingBounds.upper and the lower bound from AveragingBounds.lower, applies the antisymmetry theorem le_antisymm to those two inequalities, and finishes with simpa to obtain the required equality.
why it matters
The result supplies the missing step that turns verified bounds into exact agreement, directly feeding the downstream theorem F_eq_J_on_pos_alt that extends the identity to all positive reals. It therefore supports uniqueness arguments for the J-cost inside the Recognition Science cost derivations and the broader forcing-chain development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.