Foundation Primitive Recognition Calculus Grow Signed Orbit Le Congr Left Of Balanced Choice Free

A small congruence lemma

A ledger (a discrete record of events) in Recognition Science grows by steps, and each step can be thought of as moving along an orbit. Some orbits are balanced: they have the same number of forward and backward moves, so their net displacement is zero. The question is whether two balanced orbits behave identically when compared with any third orbit.

This result proves that they do. The theorem le_congr_left_of_balanced_cf states: if two signed orbits are balanced, then one is less than or equal to a third orbit exactly when the other is. In symbols, for balanced a and a', we have a ≤ b if and only if a' ≤ b. The proof is short: balanced orbits have the same natural-number representation, so the comparison reduces to a fact about natural numbers, which the omega tactic settles.

In plain language, this is a congruence property. It says that for purposes of ordering, balanced orbits are interchangeable on the left side of a comparison. The result is a small but necessary piece of the framework's foundation: it ensures that the ordering on orbits respects the equivalence that balance defines.

In Recognition Science, this lemma supports the larger structure of the forcing chain. It is not a standalone discovery but a working part of the calculus that the framework builds on. The result is machine-checked, meaning a computer verified every step of the proof from the axioms.

theorem le_congr_left_of_balanced_cf {a a' b : SignedOrbit}
    (h : SignedOrbit.balanced a a') :
    SignedOrbit.le a b ↔ SignedOrbit.le a' b := by
  rw [SignedOrbit.balanced_iff_toNat_eq] at h
  constructor
  · intro hle
    rw [le_iff_toNat_cf] at hle ⊢
    omega
  · intro hle
    rw [le_iff_toNat_cf] at hle ⊢
    omega

What this page does not claim

This answer does not claim that balanced orbits are equal as objects, only that they compare identically in the ordering. This answer does not claim that the theorem establishes any property of the physical constants or particle masses.

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