NonTrivialL
plain-language theorem explainer
Non-triviality for a comparison operator on recovered reals: some positive recovered real has nonzero derived one-argument cost. Cited when assembling the recovered-real Law of Logic package and when transporting non-triviality to Mathlib reals. Pure definitional Prop (existential), not a proved existence claim.
Claim. A comparison operator $C$ on recovered reals is non-trivial when there exists a recovered real $x>0$ such that the derived cost $C(x,1)$ is not the recovered zero.
background
This module is the recovered-real mirror of the real Law-of-Logic comparison surface. Structural axioms (identity, non-contradiction, scale invariance, non-triviality) are stated natively on LogicReal; analytic regularity is transported to the already-checked real theorems.
LogicReal is the Cauchy completion of the recovered rationals (via the canonical completion of $\mathbb{Q}$ and the equivalence with recovered rationals), wrapped to avoid polluting global instances. A comparison operator is a binary map $C:\mathrm{LogicReal}\times\mathrm{LogicReal}\to\mathrm{LogicReal}$. The derived one-argument cost is $r\mapsto C(r,1)$, with $1$ and $0$ injected from Mathlib reals by fromReal.
Non-triviality is the demand that this derived cost is not identically zero on the positive cone: some $x>0$ has nonzero cost. That matches the real-side non-triviality field used to force a genuine cost rather than the zero functional.
proof idea
Definitional only: the body is the Prop $\exists x:\mathrm{LogicReal},, 0<x\land C(x,1)\neq 0$ (with $0,1$ via real injection and the derived-cost abbreviation). No tactics or lemmas.
why it matters
One of the four native structural fields of the recovered-real Law of Logic package. Downstream, SatisfiesLawsOfLogicL requires this field alongside identity, non-contradiction, and scale invariance, then attaches the transported real analytic/polynomial surface.
The bridge theorem nonTrivialL_to_real pushes a witness through toReal, using order and inequality transport, so non-triviality on recovered reals implies the already-verified real non-triviality for the transported comparison operator. That keeps the functional-equation forcing chain (J-uniqueness / RCL side) aligned when the cost is written over recovered reals rather than Mathlib $\mathbb{R}$.
No open scaffold: this is the Prop interface those parents consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.