derivedCostL
plain-language theorem explainer
From any two-argument comparison operator on recovered reals, form the one-argument cost by fixing the second slot at the unit. Anyone stating non-triviality or transporting Law-of-Logic axioms to Mathlib reals cites this. The body is a one-line partial application via the real-embedding of 1.
Claim. Given a comparison operator $C$ on recovered reals (a map $\mathrm{LogicReal}\times\mathrm{LogicReal}\to\mathrm{LogicReal}$), the derived cost is the unary map $r\mapsto C(r,1)$, where $1$ is the image of the Mathlib unit under the embedding into recovered reals.
background
This module is the recovered-real mirror of LogicAsFunctionalEquation. Comparison operators are stated natively on LogicReal (the Cauchy completion of recovered rationals, wrapped to avoid polluting Mathlib's completed reals), while analytic regularity is transported through toReal.
A comparison operator here is simply a binary map $C:\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$. The classical RS cost surface uses a unary $J$ obtained by comparing a scale to the unit; this definition is that same specialization on the recovered line. The embedding fromReal sends Mathlib $\mathbb{R}$ into LogicReal via the comparison equivalence, so fromReal 1 is the recovered unit.
Upstream, LogicReal and fromReal supply the carrier and the unit; the sibling abbrev ComparisonOperatorL names the binary type.
proof idea
Pure definition, not a proof. The body is the lambda $r \mapsto C, r, (\mathrm{fromReal}, 1)$: fix the second argument of the binary comparison at the embedded unit. Marked @[simp] so downstream rewrites unfold it automatically.
why it matters
Unary cost is the native object in the Recognition Composition Law and in T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). Non-triviality on recovered reals is defined exactly as existence of positive $x$ with derived cost not equal to the embedded zero; the transport theorem nonTrivialL_to_real pushes that witness to Mathlib reals via transportComparison. Without this partial application, the structural Law-of-Logic package (SatisfiesLawsOfLogicL and its identity, non-contradiction, scale-invariance, non-triviality fields) cannot state the cost-side non-degeneracy axiom on LogicReal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.