Encyclopedia Foundation Foundation Primitive Recognition Calculus Integer Order

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Integer Order

A machine-checked library proves that the basic objects of Recognition Science, signed orbits, form a totally ordered line, and that this order behaves exactly like the usual order on whole numbers.

Verify this page

Integer order in the signed orbit

In Recognition Science, the primitive objects are signed orbits, a discrete record of events that carries a magnitude and a sign. The integer order module in the machine-checked library of formal theorems asks a simple question: can these objects be compared, and does that comparison behave like the order on ordinary integers? The answer, proved as a theorem, is yes. The library shows that every pair of signed orbits is comparable, that the comparison is transitive, and that adding the same orbit to both sides of a comparison leaves the result unchanged.

The key structure is a comparison function, written cmp, which returns whether one signed orbit is less than, equal to, or greater than another. The library proves that this function is consistent with the underlying order relation: if cmp a b says less, then a is indeed less than b, and similarly for greater. It also proves that the comparison is invariant under adding a common orbit, and that negating both sides swaps the order. These are exactly the properties one expects from an ordered group, and they hold here without any extra assumptions.

The module also establishes a certificate, a single theorem that bundles all these order properties into one statement. This certificate is a formal guarantee that the signed orbits form a totally ordered set, meaning there are no incomparable pairs and no cycles in the ordering. The proof uses the underlying representation of signed orbits as integers, so the order on signed orbits is not a new invention but a faithful mirror of the standard order on the integers.

This matters because the rest of the framework builds on these objects. If the order were inconsistent, any later theorem that relies on comparing magnitudes or signs would be built on sand. The integer order module closes that gap: it shows that the basic vocabulary of comparison, less than, greater than, and equality, is well founded and behaves exactly as the integers do. This is a foundation stone, not a headline result, but it is the kind of stone that lets the rest of the building stand.

THEOREM le_total · le_trans · cmp_add_left · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean
le_total · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:44 
theorem le_total (a b : SignedOrbit) :
    SignedOrbit.le a b ∨ SignedOrbit.le b a := by
  rw [SignedOrbit.le_iff_toInt_le, SignedOrbit.le_iff_toInt_le]
  omega
le_trans · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:31 
theorem le_trans {a b c : SignedOrbit}
    (hab : SignedOrbit.le a b) (hbc : SignedOrbit.le b c) :
    SignedOrbit.le a c := by
  rw [SignedOrbit.le_iff_toInt_le] at *
  omega
cmp_add_left · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:2497 
theorem cmp_add_left (a b c : SignedOrbit) :
    SignedOrbit.cmp (SignedOrbit.add c a) (SignedOrbit.add c b) =
      SignedOrbit.cmp a b := by
  cases hcmp : SignedOrbit.cmp a b with
  | lt =>
      have hlt : SignedOrbit.lt a b :=
        (SignedOrbit.cmp_eq_lt_iff a b).mp hcmp
      exact SignedOrbit.cmp_eq_lt_of_lt
        ((SignedOrbit.lt_add_left_iff a b c).mpr hlt)
  | eq =>
      have hbal : SignedOrbit.balanced a b :=
        (SignedOrbit.cmp_eq_eq_iff a b).mp hcmp
      exact SignedOrbit.cmp_eq_eq_of_balanced
        ((SignedOrbit.balanced_add_left_iff a b c).mpr hbal)
  | gt =>
      have hgt : SignedOrbit.lt b a :=
        (SignedOrbit.cmp_eq_gt_iff a b).mp hcmp
      exact SignedOrbit.cmp_eq_gt_of_gt
        ((SignedOrbit.lt_add_left_iff b a c).mpr hgt)
THEOREM cmp_eq_lt_iff · cmp_eq_gt_iff · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean
cmp_eq_lt_iff · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:944 
theorem cmp_eq_lt_iff (a b : SignedOrbit) :
    SignedOrbit.cmp a b = Ordering.lt ↔ SignedOrbit.lt a b := by
  constructor
  · intro hcmp
    unfold SignedOrbit.cmp at hcmp
    by_cases hbal : SignedOrbit.balanced a b
    · simp [hbal] at hcmp
    · by_cases hflag : (SignedOrbit.sub b a).nonnegFlag = true
      · rw [SignedOrbit.lt_iff_toInt_lt]
        rw [SignedOrbit.nonnegFlag_eq_true_iff, SignedOrbit.sub_toInt] at hflag
        rw [SignedOrbit.balanced_iff_toInt_eq] at hbal
        omega
      · simp [hbal, hflag] at hcmp
  · intro hlt
    exact SignedOrbit.cmp_eq_lt_of_lt hlt
cmp_eq_gt_iff · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:973 
theorem cmp_eq_gt_iff (a b : SignedOrbit) :
    SignedOrbit.cmp a b = Ordering.gt ↔ SignedOrbit.lt b a := by
  constructor
  · intro hcmp
    unfold SignedOrbit.cmp at hcmp
    by_cases hbal : SignedOrbit.balanced a b
    · simp [hbal] at hcmp
    · by_cases hflag : (SignedOrbit.sub b a).nonnegFlag = true
      · simp [hbal, hflag] at hcmp
      · rw [SignedOrbit.lt_iff_toInt_lt]
        have hflagFalse : (SignedOrbit.sub b a).nonnegFlag = false := by
          cases hbranch : (SignedOrbit.sub b a).nonnegFlag with
          | false => rfl
          | true =>
              exfalso
              exact hflag hbranch
        rw [SignedOrbit.nonnegFlag_eq_false_iff, SignedOrbit.sub_toInt] at hflagFalse
        omega
  · intro hgt
    exact SignedOrbit.cmp_eq_gt_of_gt hgt
THEOREM integer_order_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean
integer_order_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerOrder.lean:6752 · truncated 
/-- The internal signed-orbit order surface is closed. -/
theorem integer_order_certificate : IntegerOrderCertificate where
  truncated_sub_display := DistinctionNat.toNat_truncatedSub
  leq_display := DistinctionNat.leq_eq_true_iff
  absdiff_display := DistinctionNat.toNat_absDiff
  signed_nonneg_display := SignedOrbit.nonneg_iff_toInt_nonneg
  signed_nonneg_flag_display := SignedOrbit.nonnegFlag_eq_true_iff
  signed_abs_display := SignedOrbit.abs_toNat
  signed_le_display := SignedOrbit.le_iff_toInt_le
  signed_lt_display := SignedOrbit.lt_iff_toInt_lt
  abs_nonzero_internal := by
    intro z h
    exact SignedOrbit.abs_ne_zero_of_not_balanced_zero h
  signed_le_reflexive := SignedOrbit.le_refl
  signed_le_transitive := by
    intro a b c
    exact SignedOrbit.le_trans
  signed_le_antisymmetric_balanced := by
    intro a b
    exact SignedOrbit.le_antisymm_balanced
  signed_le_total := SignedOrbit.le_total
  signed_order_trichotomy := SignedOrbit.trichotomy
  signed_negativeFlag_eq_true_iff_nonnegFlag_eq_false :=
    SignedOrbit.negativeFlag_eq_true_iff_nonnegFlag_eq_false
  signed_negativeFlag_eq_false_iff_nonnegFlag_eq_true :=
    SignedOrbit.negativeFlag_eq_false_iff_nonnegFlag_eq_true
  signed_flags_exclusive := SignedOrbit.signFlags_exclusive
  signed_flags_exhaustive := SignedOrbit.signFlags_exhaustive
  signed_zero_le_iff_nonnegFlag := SignedOrbit.zero_le_iff_nonnegFlag
  signed_lt_zero_iff_negativeFlag := SignedOrbit.lt_zero_iff_negativeFlag
  signed_zero_lt_iff_nonnegFlag_and_not_balanced_zero :=
    SignedOrbit.zero_lt_iff_nonnegFlag_and_not_balanced_zero
  signed_nonnegFlag_eq_of_balanced := by
    intro z w
    exact SignedOrbit.nonnegFlag_eq_of_balanced
  signed_negativeFlag_eq_of_balanced := by
    intro z w
    exact SignedOrbit.negativeFlag_eq_of_balanced
  signed_nonneg_iff_of_balanced := by
    intro z w
    exact SignedOrbit.nonneg_iff_of_balanced
  signed_add_congr_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.add_congr_of_balanced
  signed_negate_congr_of_balanced := by
    intro a a'
    exact SignedOrbit.negate_congr_of_balanced
  signed_sub_congr_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.sub_congr_of_balanced
  signed_sub_congr_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.sub_congr_of_balanced_left
  signed_sub_congr_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.sub_congr_of_balanced_right
  signed_nonnegFlag_sub_eq_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.nonnegFlag_sub_eq_of_balanced_left
  signed_nonnegFlag_sub_eq_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.nonnegFlag_sub_eq_of_balanced_right
  signed_negativeFlag_sub_eq_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.negativeFlag_sub_eq_of_balanced_left
  signed_negativeFlag_sub_eq_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.negativeFlag_sub_eq_of_balanced_right
  signed_nonnegFlag_sub_eq_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.nonnegFlag_sub_eq_of_balanced
  signed_negativeFlag_sub_eq_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.negativeFlag_sub_eq_of_balanced
  signed_scaleByNat_congr_of_balanced := by
    intro z w
    exact SignedOrbit.scaleByNat_congr_of_balanced
  signed_scaleByNat_balanced_zero_of_balanced_zero := by
    intro z
    exact SignedOrbit.scaleByNat_balanced_zero_of_balanced_zero
  signed_mul_ofOrbit_balanced_scaleByNat :=
    SignedOrbit.mul_ofOrbit_balanced_scaleByNat
  signed_ofOrbit_mul_balanced_scaleByNat :=
    SignedOrbit.ofOrbit_mul_balanced_scaleByNat
  signed_abs_mul := SignedOrbit.abs_mul
  signed_mul_balanced_zero_iff := SignedOrbit.mul_balanced_zero_iff
  signed_mul_not_balanced_zero_iff := SignedOrbit.mul_not_balanced_zero_iff
  signed_balanced_mul_left_iff_of_not_balanced_zero :=
    SignedOrbit.balanced_mul_left_iff_of_not_balanced_zero
  signed_balanced_mul_right_iff_of_not_balanced_zero :=
    SignedOrbit.balanced_mul_right_iff_of_not_balanced_zero
  signed_le_mul_left_iff_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.le_mul_left_iff_of_nonnegFlag_of_not_balanced_zero
  signed_lt_mul_left_iff_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.lt_mul_left_iff_of_nonnegFlag_of_not_balanced_zero
  signed_le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero
  signed_lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero
  signed_le_mul_left_iff_of_negativeFlag :=
    SignedOrbit.le_mul_left_iff_of_negativeFlag
  signed_lt_mul_left_iff_of_negativeFlag :=
    SignedOrbit.lt_mul_left_iff_of_negativeFlag
  signed_le_mul_right_iff_of_negativeFlag :=
    SignedOrbit.le_mul_right_iff_of_negativeFlag
  signed_lt_mul_right_iff_of_negativeFlag :=
    SignedOrbit.lt_mul_right_iff_of_negativeFlag
  signed_abs_mul_eq_zero_iff := SignedOrbit.abs_mul_eq_zero_iff
  signed_abs_mul_ne_zero_iff := SignedOrbit.abs_mul_ne_zero_iff
  signed_abs_mul_eq_zero_iff_balanced_zero :=
    SignedOrbit.abs_mul_eq_zero_iff_balanced_zero
  signed_abs_mul_ne_zero_iff_not_balanced_zero :=
    SignedOrbit.abs_mul_ne_zero_iff_not_balanced_zero
  signed_abs_scaleByNat := SignedOrbit.abs_scaleByNat
  signed_abs_mul_ofOrbit_right := SignedOrbit.abs_mul_ofOrbit_right
  signed_abs_mul_ofOrbit_left := SignedOrbit.abs_mul_ofOrbit_left
  signed_mul_ofOrbit_right_balanced_zero_iff :=
    SignedOrbit.mul_ofOrbit_right_balanced_zero_iff
  signed_mul_ofOrbit_left_balanced_zero_iff :=
    SignedOrbit.mul_ofOrbit_left_balanced_zero_iff
  signed_mul_ofOrbit_right_not_balanced_zero_iff :=
    SignedOrbit.mul_ofOrbit_right_not_balanced_zero_iff
  signed_mul_ofOrbit_left_not_balanced_zero_iff :=
    SignedOrbit.mul_ofOrbit_left_not_balanced_zero_iff
  signed_nonnegFlag_scaleByNat_of_ne_zero :=
    SignedOrbit.nonnegFlag_scaleByNat_of_ne_zero
  signed_negativeFlag_scaleByNat_of_ne_zero :=
    SignedOrbit.negativeFlag_scaleByNat_of_ne_zero
  signed_scaleByNat_balanced_zero_iff := SignedOrbit.scaleByNat_balanced_zero_iff
  signed_scaleByNat_not_balanced_zero_iff :=
    SignedOrbit.scaleByNat_not_balanced_zero_iff
  signed_abs_scaleByNat_eq_zero_iff := SignedOrbit.abs_scaleByNat_eq_zero_iff
  signed_abs_scaleByNat_ne_zero_iff := SignedOrbit.abs_scaleByNat_ne_zero_iff
  signed_abs_mul_ofOrbit_right_eq_zero_iff :=
    SignedOrbit.abs_mul_ofOrbit_right_eq_zero_iff
  signed_abs_mul_ofOrbit_left_eq_zero_iff :=
    SignedOrbit.abs_mul_ofOrbit_left_eq_zero_iff
  signed_abs_mul_ofOrbit_right_ne_zero_iff :=
    SignedOrbit.abs_mul_ofOrbit_right_ne_zero_iff
  signed_abs_mul_ofOrbit_left_ne_zero_iff :=
    SignedOrbit.abs_mul_ofOrbit_left_ne_zero_iff
  signed_le_scaleByNat_of_le := by
    intro z w
    exact SignedOrbit.le_scaleByNat_of_le
  signed_le_scaleByNat_iff_of_ne_zero :=
    SignedOrbit.le_scaleByNat_iff_of_ne_zero
  signed_lt_scaleByNat_iff_of_ne_zero :=
    SignedOrbit.lt_scaleByNat_iff_of_ne_zero
  signed_balanced_scaleByNat_iff_of_ne_zero :=
    SignedOrbit.balanced_scaleByNat_iff_of_ne_zero
  signed_cmp_scaleByNat_of_ne_zero :=
    SignedOrbit.cmp_scaleByNat_of_ne_zero
  signed_le_mul_ofOrbit_right_iff_of_ne_zero :=
    SignedOrbit.le_mul_ofOrbit_right_iff_of_ne_zero
  signed_lt_mul_ofOrbit_right_iff_of_ne_zero :=
    SignedOrbit.lt_mul_ofOrbit_right_iff_of_ne_zero
  signed_balanced_mul_ofOrbit_right_iff_of_ne_zero :=
    SignedOrbit.balanced_mul_ofOrbit_right_iff_of_ne_zero
  signed_cmp_mul_ofOrbit_right_of_ne_zero :=
    SignedOrbit.cmp_mul_ofOrbit_right_of_ne_zero
  signed_le_mul_ofOrbit_left_iff_of_ne_zero :=
    SignedOrbit.le_mul_ofOrbit_left_iff_of_ne_zero
  signed_lt_mul_ofOrbit_left_iff_of_ne_zero :=
    SignedOrbit.lt_mul_ofOrbit_left_iff_of_ne_zero
  signed_balanced_mul_ofOrbit_left_iff_of_ne_zero :=
    SignedOrbit.balanced_mul_ofOrbit_left_iff_of_ne_zero
  signed_cmp_mul_ofOrbit_left_of_ne_zero :=
    SignedOrbit.cmp_mul_ofOrbit_left_of_ne_zero
  signed_cmp_mul_left_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.cmp_mul_left_of_nonnegFlag_of_not_balanced_zero
  signed_cmp_mul_right_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.cmp_mul_right_of_nonnegFlag_of_not_balanced_zero
  signed_cmp_mul_left_of_negativeFlag :=
    SignedOrbit.cmp_mul_left_of_negativeFlag
  signed_cmp_mul_right_of_negativeFlag :=
    SignedOrbit.cmp_mul_right_of_negativeFlag
  signed_nonnegFlag_mul_of_nonnegFlag_of_nonnegFlag :=
    SignedOrbit.nonnegFlag_mul_of_nonnegFlag_of_nonnegFlag
  signed_nonnegFlag_mul_of_negativeFlag_of_negativeFlag :=
    SignedOrbit.nonnegFlag_mul_of_negativeFlag_of_negativeFlag
  signed_negativeFlag_mul_of_nonnegFlag_of_not_balanced_zero_of_negativeFlag :=
    SignedOrbit.negativeFlag_mul_of_nonnegFlag_of_not_balanced_zero_of_negativeFlag
  signed_negativeFlag_mul_of_negativeFlag_of_nonnegFlag_of_not_balanced_zero :=
    SignedOrbit.negativeFlag_mul_of_negativeFlag_of_nonnegFlag_of_not_balanced_zero
  signed_negativeFlag_mul_iff := SignedOrbit.negativeFlag_mul_iff
  signed_nonnegFlag_mul_iff_not_strict_opposite_sign :=
    SignedOrbit.nonnegFlag_mul_iff_not_strict_opposite_sign
  signed_nonnegFlag_mul_of_balanced_zero_left :=
    SignedOrbit.nonnegFlag_mul_of_balanced_zero_left
  signed_nonnegFlag_mul_of_balanced_zero_right :=
    SignedOrbit.nonnegFlag_mul_of_balanced_zero_right
  signed_negativeFlag_mul_eq_false_of_balanced_zero_left :=
    SignedOrbit.negativeFlag_mul_eq_false_of_balanced_zero_left
  signed_negativeFlag_mul_eq_false_of_balanced_zero_right :=
    SignedOrbit.negativeFlag_mul_eq_false_of_balanced_zero_right
  signed_mul_balanced_zero_of_balanced_zero_left :=
    SignedOrbit.mul_balanced_zero_of_balanced_zero_left
  signed_mul_balanced_zero_of_balanced_zero_right :=
    SignedOrbit.mul_balanced_zero_of_balanced_zero_right
  signed_abs_mul_eq_zero_of_balanced_zero_left :=
    SignedOrbit.abs_mul_eq_zero_of_balanced_zero_left
  signed_abs_mul_eq_zero_of_balanced_zero_right :=
    SignedOrbit.abs_mul_eq_zero_of_balanced_zero_right
  signed_mul_congr_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.mul_congr_of_balanced
  signed_mul_congr_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.mul_congr_of_balanced_left
  signed_mul_congr_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.mul_congr_of_balanced_right
  signed_nonnegFlag_mul_eq_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.nonnegFlag_mul_eq_of_balanced
  signed_nonnegFlag_mul_eq_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.nonnegFlag_mul_eq_of_balanced_left
  signed_nonnegFlag_mul_eq_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.nonnegFlag_mul_eq_of_balanced_right
  signed_negativeFlag_mul_eq_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.negativeFlag_mul_eq_of_balanced
  signed_negativeFlag_mul_eq_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.negativeFlag_mul_eq_of_balanced_left
  signed_negativeFlag_mul_eq_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.negativeFlag_mul_eq_of_balanced_right
  signed_abs_mul_eq_of_balanced := by
    intro a a' b b'
    exact SignedOrbit.abs_mul_eq_of_balanced
  signed_abs_mul_eq_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.abs_mul_eq_of_balanced_left
  signed_abs_mul_eq_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.abs_mul_eq_of_balanced_right
  signed_mul_balanced_zero_iff_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.mul_balanced_zero_iff_of_balanced_left
  signed_mul_balanced_zero_iff_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.mul_balanced_zero_iff_of_balanced_right
  signed_abs_mul_eq_zero_iff_of_balanced_left := by
    intro a a' b
    exact SignedOrbit.abs_mul_eq_zero_iff_of_balanced_left
  signed_abs_mul_eq_zero_iff_of_balanced_right := by
    intro a b b'
    exact SignedOrbit.abs_mul_eq_zero_iff_of_balanced_right
  signed_abs_mul_ne_zero_iff_of_balanced_left := b

-- … truncated for the page; open the module for the rest.

What this page does not claim

This module does not define the cost function J or prove its uniqueness. It does not establish the golden ratio or the eight-tick recognition cycle. It does not connect the integer order to any physical measurement or empirical prediction.

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/IntegerOrder.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND