nonTrivialL_to_real
plain-language theorem explainer
Non-triviality of a comparison operator on recovered reals transfers to the transported real operator: some positive LogicReal with nonzero derived cost maps to a positive real with nonzero real derived cost. Anyone assembling the recovered-real Law of Logic package cites this bridge. The proof unpacks the existential and pushes inequalities and equalities through toReal/fromReal.
Claim. Let $C$ be a comparison operator on recovered reals. If $C$ is non-trivial in the recovered-real sense (there exists $x>0$ in LogicReal with derived cost $C(x,1)\neq 0$), then the real comparison operator obtained by transporting $C$ through the LogicReal-to-$\mathbb{R}$ embedding is non-trivial: some positive real has nonzero derived cost.
background
This module is the recovered-real mirror of Foundation.LogicAsFunctionalEquation. Comparison operators are binary maps $C$ used to encode Aristotelian laws of logic as structural constraints; the derived one-argument cost fixes the second slot at the multiplicative unit, $r\mapsto C(r,1)$. On ordinary reals, non-triviality means some positive ratio has nonzero derived cost, ruling out the constant-zero operator that would otherwise satisfy the constraints vacuously.
Here the same notions are stated natively on LogicReal (recovered reals). NonTrivialL asserts existence of a strictly positive LogicReal whose derived cost is not the zero LogicReal. Transport to the already-verified real surface uses the embedding toReal (and its inverse fromReal) together with a comparison-operator transport map that conjugates $C$ into a real operator.
The sibling structural fields (identity, non-contradiction, scale invariance) have parallel transport lemmas; analytic regularity is handled separately by pushing through toReal.
proof idea
Unpack the recovered-real non-triviality witness to a LogicReal $x>0$ with nonzero derived cost. Offer toReal x as the real witness. Positivity of the image follows from the order-reflection lemma relating < on LogicReal to < on $\mathbb{R}$.
For nonzero cost: assume the transported real derived cost vanishes. Unfold transport and the real derived-cost definition, cancel toReal ∘ fromReal on the unit, then use fromReal_toReal on $x$ to obtain that the LogicReal derived cost maps to real zero. Reflect equality back via eq_iff_toReal_eq to contradict the original nonzero witness.
why it matters
Non-triviality is one of the four Aristotelian-plus-bridge constraints that force a comparison operator to behave like the Recognition cost. On the real side it excludes the zero solution so that the Recognition Composition Law and J-uniqueness (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$) can pin the cost uniquely. This lemma closes the corresponding field on the recovered-real mirror, so a full SatisfiesLawsOfLogicL package can be pushed to the existing real theorem surface via transport.
No downstream consumers are wired yet (used_by is empty); the immediate role is parity with the sibling transport lemmas for identity, non-contradiction, and scale invariance. Once those are bundled, the recovered-real Law of Logic becomes a drop-in hypothesis for any development that prefers LogicReal as the native carrier before evaluating into $\mathbb{R}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.