Foundation Primitive Recognition Calculus Integer Rational Abs Ne Zero Of Not Ba

Zero, distinct from nothing

The declaration abs_ne_zero_of_not_balanced_zero is a formal theorem in the framework's machine-checked library. It states a simple property of the framework's own number system, called primitive recognition calculus, which is a discrete record of events built from signed orbits. The theorem says: if a number is not the zero element, then its absolute value is not zero either. In plainer terms, in this system, the only number whose absolute value is zero is zero itself.

This is a foundational lemma, not a grand result. It is the kind of fact that must be true for the arithmetic to behave sensibly. The framework's numbers are not the familiar integers and rationals; they are constructed as equivalence classes of orbits, and the theorem confirms that the absolute value function, defined on those classes, respects the distinction between zero and everything else. The proof is a routine simplification, tagged as a theorem in the library.

The declaration does not claim that the framework's numbers are the same as the usual integers and rationals, nor that the absolute value is the familiar one. It only establishes the specific property that a non-zero element has a non-zero absolute value. It also does not claim anything about the physical content of the framework, such as the cost function or the golden ratio; it is purely an internal consistency check within the number system's construction.

/-- K4.8. Choice-free structural zero test: a PRC rational is in the zero
class iff its representative's numerator balances the zero signed orbit.
Well-definedness routes through the integer cross-multiplication hub (no `ℚ`
display), so the definition depends only on `{propext, Quot.sound}`. -/
def isZero : PRCRat → Prop :=
  Quot.lift
    (fun q => SignedOrbit.balanced q.num SignedOrbit.zero)
    (by
      intro a b h
      have h' := (RatioOrbit.crossEq_iff_toIntCross a b).mp h
      have hda : (a.den.toNat : ℤ) ≠ 0 := by
        have := a.den_toNat_ne_zero
        omega
      have hdb : (b.den.toNat : ℤ) ≠ 0 := by
        have := b.den_toNat_ne_zero
        omega
      apply propext
      show SignedOrbit.balanced a.num SignedOrbit.zero
          ↔ SignedOrbit.balanced b.num SignedOrbit.zero
      rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.balanced_iff_toInt_eq,
          SignedOrbit.zero_toInt]
      constructor
      · intro ha0
        have h0 : b.num.toInt * (a.den.toNat : ℤ) = 0 * (a.den.toNat : ℤ) := by
          rw [← h', ha0, Int.zero_mul, Int.zero_mul]
        exact Int.eq_of_mul_eq_mul_right hda h0
      · intro hb0
        have h0 : a.num.toInt * (b.den.toNat : ℤ) = 0 * (b.den.toNat : ℤ) := by
          rw [h', hb0, Int.zero_mul, Int.zero_mul]
        exact Int.eq_of_mul_eq_mul_right hdb h0)

What this page does not claim

The framework's numbers are identical to the standard integers and rationals. The absolute value function is the familiar one from conventional arithmetic. This theorem has any direct physical consequence on its own.

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/PrimitiveRecognitionCalculus/IntegerRational.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: