Foundation Primitive Recognition Calculus Grow Signed Orbit Order Choice Free

A choice-free ordering

A signed orbit is a pair of natural-number counts, one positive and one negative. Think of a tally sheet with two columns, pluses and minuses. The order on such pairs answers a simple question: when is one signed orbit at least as large as another? The natural answer is to subtract the counts and ask whether the result is nonnegative. The grow (a discrete record of how a system expands) framework establishes that this comparison can be made entirely with the finite positions of the counts, without relying on the axiom of choice.

The axiom of choice is a standard tool in mathematics, but the framework's library of machine-checked theorems aims to keep its proofs as free of extra assumptions as possible. The earlier ordering of signed orbits used the integer display, which carried a choice dependence. This framework re-grounds the order using only the natural-number positions of the counts. The key equivalence is that one signed orbit is nonnegative exactly when its negative count's position is at most its positive count's position, written as natural numbers (the counting numbers 0, 1, 2, ...).

The framework proves the standard order properties for this relation: reflexivity (every orbit is at least itself), transitivity (if A is at least B and B is at least C, then A is at least C), totality (any two orbits are comparable), and antisymmetry up to balanced length (if each is at least the other, their counts are equal). Each proof is a direct calculation on natural numbers. The machine-checked library confirms that every theorem here depends only on two standard logical principles, propositional extensionality and quotient soundness, and not on the axiom of choice.

In Recognition Science, this choice-free ordering is the base for the ratio (a comparison of two amounts) ordered-field tower, which later steps in the framework build upon. The practical payoff is a cleaner foundation: the order on signed orbits stands on its own, without an extra assumption that the rest of the framework does not need.

/-- Internal nonnegativity collapses to a pure ℕ inequality on δ-orbit positions,
through the choice-free `balanced_iff_toNat_eq` bridge (NOT `nonneg_iff_toInt_nonneg`). -/
theorem nonneg_iff_toNat_le (z : SignedOrbit) :
    SignedOrbit.nonneg z ↔ z.neg.toNat ≤ z.pos.toNat := by
  unfold SignedOrbit.nonneg
  constructor
  · rintro ⟨k, hk⟩
    rw [SignedOrbit.balanced_iff_toNat_eq] at hk
    have hp : (SignedOrbit.ofOrbit k).pos = k := rfl
    have hn : (SignedOrbit.ofOrbit k).neg = DistinctionNat.zero := rfl
    rw [hp, hn, DistinctionNat.toNat_zero] at hk
    omega
  · intro h
    refine ⟨DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat), ?_⟩
    rw [SignedOrbit.balanced_iff_toNat_eq]
    have hp : (SignedOrbit.ofOrbit (DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat))).pos
        = DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat) := rfl
    have hn : (SignedOrbit.ofOrbit (DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat))).neg
        = DistinctionNat.zero := rfl
    rw [hp, hn, DistinctionNat.toNat_zero, DistinctionNat.toNat_ofNat]
    omega

/-- Reflexivity of the signed-orbit order, choice-free. -/
theorem le_refl_cf (a : SignedOrbit) : SignedOrbit.le a a := by
  rw [le_iff_toNat_cf]; omega

/-- Transitivity, choice-free. -/
theorem le_trans_cf (a b c : SignedOrbit)
    (hab : SignedOrbit.le a b) (hbc : SignedOrbit.le b c) : SignedOrbit.le a c := by
  rw [le_iff_toNat_cf] at hab hbc ⊢; omega

/-- Totality, choice-free. -/
theorem le_total_cf (a b : SignedOrbit) :
    SignedOrbit.le a b ∨ SignedOrbit.le b a := by
  rw [le_iff_toNat_cf, le_iff_toNat_cf]; omega

/-- Antisymmetry up to balanced-length equivalence, choice-free. -/
theorem le_antisymm_balanced_cf (a b : SignedOrbit)
    (hab : SignedOrbit.le a b) (hba : SignedOrbit.le b a) : SignedOrbit.balanced a b := by
  rw [le_iff_toNat_cf] at hab hba
  rw [SignedOrbit.balanced_iff_toNat_eq]
  omega

/-- The signed-orbit order, characterized purely at the ℕ-level on δ-orbit positions.
This is the choice-free replacement for `le_iff_toInt_le`. -/
theorem le_iff_toNat_cf (a b : SignedOrbit) :
    SignedOrbit.le a b ↔ b.neg.toNat + a.pos.toNat ≤ b.pos.toNat + a.neg.toNat := by
  unfold SignedOrbit.le
  rw [nonneg_iff_toNat_le]
  have hp : (SignedOrbit.sub b a).pos = b.pos + a.neg := rfl
  have hn : (SignedOrbit.sub b a).neg = b.neg + a.pos := rfl
  rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_add]

What this page does not claim

This framework does not prove the full ordered-field structure for signed orbits; it only establishes the order properties. The choice-free order does not change the meaning of the order, only the proof method. The framework does not define signed orbits; it re-grounds their existing order.

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/Grow/SignedOrbitOrderChoiceFree.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: