Foundation Primitive Recognition Calculus Integer Order Negative Flag Mul Of Neg

Sign of a product

The declaration establishes a sign rule for multiplication in the framework's signed-orbit calculus. A signed orbit is a discrete record of a recognition event, carrying a sign flag that marks it as nonnegative or negative. The rule states that when you multiply a negative orbit by a nonnegative orbit, the product is negative, provided the nonnegative orbit is not balanced with zero. In plainer terms: a negative number times a positive number is negative, and a negative number times zero is zero, not negative.

This is a theorem in the machine-checked library of formal theorems, meaning it is proved from the framework's definitions. It is not a new assumption or a separate rule; it follows from how multiplication and the sign flags are defined. The theorem is part of a larger set of closed order laws for the signed-orbit surface, which govern how the ordering of orbits behaves under operations like addition, negation, and multiplication.

The rule matters because it shows the signed-orbit calculus behaves like ordinary arithmetic in this respect. The framework does not introduce a novel sign convention; it reproduces the familiar sign of a product. This is a consistency check, not a discovery about the physical world. The theorem does not claim anything about the magnitude of the product, only its sign. It also does not claim that multiplication is commutative or associative; those are separate properties proved elsewhere.

In Recognition Science, this theorem is a small step in building the ordered structure of signed orbits. It is used to reason about comparisons and orderings, which are fundamental to the framework's account of recognition and cost. The practical consequence is that the framework's internal arithmetic is reliable: signs multiply as expected, so later constructions that depend on sign do not need to re-check this basic fact.

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

What this page does not claim

The theorem does not claim anything about the magnitude of the product, only its sign. The theorem does not claim that multiplication is commutative or associative. The theorem does not claim that the signed-orbit calculus is the only way to represent signs.

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: