add_left_cancel
Left cancellation holds for addition in the logic naturals: a + b = a + c implies b = c. Workers deriving arithmetic from the recognition functional equation cite this when manipulating equations in the orbit. The proof transfers the hypothesis to Nat via toNat, cancels there with omega, and pulls back with fromNat.
claimFor all elements $a, b, c$ of the logic naturals, if $a + b = a + c$ then $b = c$.
background
The logic naturals form an inductive type with an identity constructor representing the zero-cost element and a step constructor for generator iterations, mirroring the multiplicative orbit under the self-similar fixed point. Addition is equipped with a recovery isomorphism to ordinary natural numbers, witnessed by the toNat_add theorem that preserves addition and the fromNat_toNat bijection. This declaration sits in the ArithmeticFromLogic module that builds Peano arithmetic from the Law of Logic functional equation.
proof idea
The tactic proof first applies congrArg toNat to the input equality. It rewrites both sides with toNat_add to expose ordinary addition in Nat. Omega then cancels the common summand to yield toNat b = toNat c. Finally congrArg fromNat followed by rewriting with fromNat_toNat recovers the desired equality in the logic naturals.
why it matters in Recognition Science
The lemma is applied directly by add_right_cancel to obtain right cancellation via commutativity. It also appears in step_mu_tau_numerator_offset_forced, where it helps force the offset n to equal the spatial dimension D = 3 in the mass numerator family. This supports the overall transfer principle between the logic-derived arithmetic and standard Nat, which underpins the phi-ladder mass formulas and the eight-tick octave in the Recognition Science framework.
scope and limits
- Does not establish addition cancellation for non-logic structures.
- Does not replace the need for the toNat_add recovery theorem.
- Applies exclusively to the addition operation defined on the logic naturals.
- Does not address uniqueness of addition or other arithmetic properties.
Lean usage
rw [add_comm a c, add_comm b c] at h; exact add_left_cancel hformal statement (Lean)
286theorem add_left_cancel {a b c : LogicNat} (h : a + b = a + c) : b = c := by
proof body
Tactic-mode proof.
287 have hcast := congrArg toNat h
288 rw [toNat_add, toNat_add] at hcast
289 have hnat : toNat b = toNat c := by omega
290 have := congrArg fromNat hnat
291 rw [fromNat_toNat, fromNat_toNat] at this
292 exact this
293
294/-- Right cancellation: `a + c = b + c ⇒ a = b`. -/