SatisfiesLawsOfLogicL
plain-language theorem explainer
Packages the recovered-real Law of Logic for a two-argument comparison on LogicReal: identity, reciprocal symmetry, scale invariance, non-triviality, and an explicit transport of analytic regularity onto the already-verified real laws. Anyone forcing the Recognition Composition Law over recovered reals cites this bundle. Pure structure definition; no proof obligation beyond assembling the five fields.
Claim. A comparison operator $C$ on recovered reals satisfies the laws of logic when: (i) $C(x,x)=0$ for every positive recovered real $x$; (ii) $C(x,y)=C(y,x)$ for positive $x,y$; (iii) $C(\lambda x,\lambda y)=C(x,y)$ for positive $\lambda,x,y$; (iv) the derived one-argument cost is not identically zero; and (v) the real transport of $C$ satisfies the corresponding real laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence, and analytic regularity).
background
This module is the recovered-real mirror of Foundation.LogicAsFunctionalEquation. Comparison operators are maps $C:\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$. Structural constraints (identity, reciprocal symmetry, scale invariance, non-triviality) are stated natively on LogicReal; continuity and the polynomial-combiner surface are not re-proved here but pushed through LogicReal.toReal via a transport map.
On the real side, satisfying the laws of logic means the four Aristotelian constraints plus scale invariance (the bridge from two-argument to one-argument form) and non-triviality, so the derived cost is not vacuously zero. The recovered-real package keeps the same intent: identity forces $C(x,x)=0$ on positives; non-contradiction is $C(x,y)=C(y,x)$; scale invariance is homogeneity under positive rescaling; non-triviality asserts some positive $x$ with nonzero derived cost.
The fifth field is the bridge: the transported real operator must already satisfy the verified real structure. That is how analytic regularity is inherited rather than rebuilt over LogicReal.
proof idea
No proof body: this is a structure (Prop-valued record). Inhabitants are five-field packages. The first four fields are the native LogicReal predicates IdentityL, NonContradictionL, ScaleInvariantL, and NonTrivialL. The fifth field is a direct appeal to the upstream real structure SatisfiesLawsOfLogic applied to the transported comparison. Downstream lemmas simply project the fifth field or feed the whole package into the real uniqueness theorem.
why it matters
This is the recovered-real entry point for the Law-of-Logic forcing argument. Downstream, lawsL_to_real is the one-line projection of the transport field, and RCL_is_unique_functional_form_of_logicL uses the package to conclude that any such $C$ has derived cost whose multiplicative consistency polynomial is forced into the RCL shape $P(u,v)=2u+2v+c,uv$. That is the recovered-real twin of the real uniqueness theorem that pins the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, which sits behind T5 J-uniqueness in the forcing chain. Without this structure, the LogicReal side cannot inherit the real analytic surface or close the uniqueness argument by transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.