identityL_to_real
plain-language theorem explainer
If a comparison operator on recovered reals obeys identity (self-comparison costs zero), its transport to ordinary reals obeys the real identity law. Anyone wiring the recovered-real Law of Logic package cites this bridge lemma. The proof lifts positivity across fromReal/toReal and applies congruence of toReal to the native identity hypothesis.
Claim. Let $C$ be a comparison operator on recovered reals. If $C$ satisfies identity—for every recovered real $x>0$, $C(x,x)$ equals the zero recovered real—then the transported operator $C_{\mathbb{R}}(x,y):=\mathrm{toReal}(C(\mathrm{fromReal}\,x,\mathrm{fromReal}\,y))$ satisfies the real identity law: for every real $x>0$, $C_{\mathbb{R}}(x,x)=0$.
background
This module is the recovered-real mirror of Foundation.LogicAsFunctionalEquation. Comparison operators here are maps $C:\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$. Structural laws (identity, non-contradiction, scale invariance, non-triviality) are stated natively on LogicReal; analytic regularity is pushed through toReal.
Identity on recovered reals says self-comparison costs the zero element: $C(x,x)=\mathrm{fromReal},0$ whenever $x>0$. The real counterpart (Aristotelian A = A) requires $C(x,x)=0$ on positive reals. Transport is defined by $C_{\mathbb{R}}(x,y)=\mathrm{toReal}(C(\mathrm{fromReal},x,\mathrm{fromReal},y))$, where toReal evaluates $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ by $\langle a,b\rangle\mapsto a+b\varphi$.
Upstream, the real Identity predicate is already the verified surface this lemma targets; toReal_zero and the fromReal/toReal round-trip supply the arithmetic glue.
proof idea
Short tactic proof. Fix a positive real $x$ and unfold transport. Lift positivity: $0<\mathrm{fromReal},x$ follows by rewriting with lt_iff_toReal_lt, toReal_zero, and toReal_fromReal. Apply the native IdentityL hypothesis at $\mathrm{fromReal},x$, then take toReal of both sides via congrArg. Finish by simplifying with toReal_fromReal to obtain $C_{\mathbb{R}}(x,x)=0$.
why it matters
One of the structural transport lemmas that connect native LogicReal laws to the already-verified real Law of Logic surface. It discharges the identity half of the bridge needed for the transported_real_laws field of SatisfiesLawsOfLogicL (the recovered-real package bundling identity, non-contradiction, scale invariance, and non-triviality). Sibling lemmas handle the other three structural fields the same way.
In the Recognition framework this sits under the functional-equation foundation that forces J-uniqueness (T5) and the Recognition Composition Law: identity is the zero-cost self-comparison that anchors any admissible cost. No recorded downstream uses yet; the lemma exists so the recovered-real package can inherit the real analytic surface without re-proving it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.