Foundation Primitive Recognition Calculus Grow Signed Orbit Le Congr Of Balanced

The order is well-behaved

A signed orbit is an ordered list of recognition events, where each event is a discrete record of something being recognized. The framework's library is a machine-checked collection of formal theorems about such structures. One theorem, le_congr_of_balanced_cf, states a simple compatibility property: if two signed orbits are balanced against each other, and two other signed orbits are balanced against each other, then the first pair's order comparison is the same as the second pair's. In symbols, if balanced means the two orbits have the same length and matching signs at every position, then a ≤ b if and only if a' ≤ b'.

This is a congruence theorem, a statement that the order relation respects the balancing equivalence. It is proved in the framework's library as a theorem, meaning it is derived from earlier definitions and lemmas with no unproved assumptions. The proof chains together two simpler facts: that balancing on the left preserves order, and that balancing on the right preserves order. The result is that the order on signed orbits is well-defined with respect to balancing, which is a necessary condition for any later construction that identifies balanced orbits with each other.

In Recognition Science, this theorem is a small but load-bearing step. The framework models recognition events as a discrete record, and signed orbits are the objects that carry information about how those events accumulate. The congruence property ensures that if two orbits are balanced, they are interchangeable for the purpose of order comparisons. This is what makes it possible to talk about a quotient structure, where balanced orbits are treated as the same object, without ambiguity.

What the theorem does not claim is just as important. It does not say that every pair of signed orbits is comparable; the order relation is partial, not total. It does not say that balancing is the only equivalence relation that preserves order, nor does it say anything about what the order means physically. The theorem is purely structural: it establishes a compatibility condition, nothing more.

theorem le_congr_of_balanced_cf {a a' b b' : SignedOrbit}
    (ha : SignedOrbit.balanced a a') (hb : SignedOrbit.balanced b b') :
    SignedOrbit.le a b ↔ SignedOrbit.le a' b' :=
  (le_congr_left_of_balanced_cf ha).trans (le_congr_right_of_balanced_cf hb)

What this page does not claim

The theorem does not state that all signed orbits are comparable under the order. The theorem does not identify balancing as the only equivalence preserving order. The theorem does not assign physical meaning to the order relation.

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