Foundation Universal Forcing Forced Integers Forced Difference Neg Swap

The negation swap

The integers are the familiar number system built from zero, one, and the operation of subtraction. The Recognition Science framework constructs its own arithmetic from a primitive notion of counting, and this declaration, forced_difference_neg_swap, records a basic fact about how subtraction behaves inside that framework. It states that for any two counts a and b, the negative of their difference equals the difference taken in the opposite order: -(a - b) = b - a. This is the additive mirror of a symmetry the framework already established for ratios, where the reciprocal of a quotient a/b is b/a.

The declaration is proved as a theorem in the framework's machine-checked library, meaning the statement follows from the framework's own axioms and definitions without additional assumptions. The proof is a direct algebraic manipulation, using the ring structure of the integers. The theorem is part of a larger certificate that shows the framework's forced arithmetic embeds into the standard integers, preserving zero, one, addition, and multiplication, and that every integer can be expressed as a difference of two forced counts. This embedding is injective, so distinct forced counts remain distinct when mapped to integers.

A companion theorem, forced_difference_fixed_iff, uses the negation swap to characterize when a difference equals its own negative. A number equal to its negative must be zero, so the condition a - b = -(a - b) holds exactly when a = b. The framework reads this as a structural parallel: just as the reciprocal involution on ratios fixes a value only at the unit a = b, the negation involution on differences fixes a value only on the diagonal. Both forced layers, integers and ratios, carry the same comparison geometry, an involution that swaps two counts and is fixed precisely where the counts agree.

The theorem does not claim that the framework's arithmetic is the integers themselves, only that it embeds into them. It does not assert that every integer arises as a single forced count; the surjectivity result is about differences, not individual elements. The negation swap is a statement about the additive structure of differences, not about multiplication or any other operation. The framework's library proves the theorem, but the framework does not claim that this symmetry is unique to its construction; the same algebraic identity holds in any ring.

/-- Negation swaps the two counts of a forced difference: `−(a − b) = b − a`. This
is the additive analogue of the reciprocal swap `(a/b)⁻¹ = b/a` on forced ratios. -/
theorem forced_difference_neg_swap (a b : LogicNat) :
    -(toInt a - toInt b) = toInt b - toInt a := by ring

/-- Negation swaps the two counts of a forced difference: `−(a − b) = b − a`. This
is the additive analogue of the reciprocal swap `(a/b)⁻¹ = b/a` on forced ratios. -/
theorem forced_difference_neg_swap (a b : LogicNat) :
    -(toInt a - toInt b) = toInt b - toInt a := by ring

/-- **The additive analogue of the reciprocal fixed-point law.** The negation
involution fixes a forced difference exactly on the diagonal `a = b` — just as the
reciprocal involution fixes a forced ratio exactly on the unit `a = b`. The two
forced layers, integers and ratios, carry the same comparison geometry: an
involution that swaps two counts, fixed precisely where the counts agree. -/
theorem forced_difference_fixed_iff (a b : LogicNat) :
    (toInt a - toInt b = -(toInt a - toInt b)) ↔ a = b := by
  rw [forced_difference_neg_swap]
  constructor
  · intro h
    have hz : toInt a - toInt b = 0 := by omega
    exact (forced_difference_zero_iff a b).mp hz
  · intro h; subst h; ring

What this page does not claim

The framework's arithmetic is not claimed to be identical to the standard integers, only embedded into them. The theorem does not assert that every integer is a single forced count, only that every integer is a difference of two forced counts. The negation swap is a statement about additive structure, not about multiplication or any other operation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UniversalForcing/ForcedIntegers.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: