add_left_neg'
plain-language theorem explainer
The recovered real numbers satisfy left additive inversion: for any element x of the Cauchy completion of the recovered rationals, -x + x equals zero. Researchers building algebraic structure on the logic-derived reals cite this result when verifying the additive group axioms. The proof reduces the claim via the equality transport equivalence and discharges the resulting identity on Mathlib reals by simplification.
Claim. For every recovered real number $x$, the additive inverse satisfies $(-x) + x = 0$.
background
The module recovers the reals from the Law-of-Logic rationals by completing LogicRat via Mathlib's Bourbaki construction on ℚ. LogicReal is the wrapper type around CompareReals.Bourbakiℝ that prevents global instance pollution while permitting reuse of completed real arithmetic; the transport map toReal realizes the canonical equivalence with Mathlib's Cauchy reals. The local setting is a transport-first API in which all algebra on LogicReal is defined by pullback along toReal. The key upstream lemma is eq_iff_toReal_eq, whose doc-comment states: 'Equality transfer: recovered real equality is exactly equality after transport to Mathlib's real line.' Analogous add_left_neg' statements already hold for LogicInt and LogicRat.
proof idea
The proof is a one-line wrapper that applies the equality transport lemma eq_iff_toReal_eq to convert the goal into an identity on the image under toReal, after which simp resolves the standard real arithmetic fact -r + r = 0.
why it matters
This declaration completes the left-inverse property for the additive structure on LogicReal, feeding the same pattern already present at the integer and rational layers. It supports the module's transport-first design so that every downstream algebraic theorem reduces to an existing Mathlib result. Within the Recognition Science foundation, the result belongs to the layer that lifts the Law-of-Logic rationals to a completed real line before the forcing chain (T0-T8) and Recognition Composition Law are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.