module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree`

Choice-free order theory for signed δ-orbits: nonnegativity and ≤ reduce to pure ℕ comparisons on orbit positions via the balanced-to-toNat bridge. Downstream ratio-orbit and signed-orbit congruence modules import these lemmas to build a total preorder without classical sign case splits. The development is a short chain of iff lemmas plus refl/trans/total/antisymm for the choice-free order.

claimOn signed $\delta$-orbits, internal nonnegativity is equivalent to a pure $\mathbb{N}$ inequality on orbit positions, via the choice-free bridge $\mathrm{balanced}\Leftrightarrow\mathrm{toNat}$ equality (not the $\mathrm{toInt}$ nonnegativity route). The induced relation $\le$ is reflexive, transitive, total, and antisymmetric on balanced elements; flags and Boolean $\mathrm{leq}$ unfold to the same $\mathbb{N}$ comparison.

background

In the Primitive Recognition Calculus, signed orbits package a pair of positive $\delta$-orbit positions with a balance/sign discipline so that integers and rationals can be grown without choosing representatives. The parent IntegerRational layer supplies the underlying casts and the choice-free identity that balance is equivalent to equality of the two natural positions.

This Grow module stays inside that discipline. Nonnegativity is not routed through an integer embedding and a classical $\ge 0$ test; it collapses to a comparison of natural orbit ranks. A Boolean nonnegativity flag and a Boolean $\mathrm{leq}$ are shown equivalent to the same pure-$\mathbb{N}$ statement, so later order proofs never reopen a sign case split.

The local setting is foundation scaffolding for ratio-orbit order: once signed $\le$ is choice-free, cross-multiplication order on positive ratios can be defined by casting denominators through $\mathrm{SignedOrbit.ofOrbit}$ and comparing products in the signed monoid.

proof idea

The module is a thin lemma layer, not a single deep proof. Core iff lemmas identify nonnegativity, the nonneg flag, and Boolean $\mathrm{leq}$ with $\mathrm{toNat}$ comparisons on $\delta$-orbit positions, always through the balanced/toNat bridge. From those equivalences the order laws are routine: reflexivity and transitivity lift from $\mathbb{N}$, totality is the corresponding $\mathbb{N}$ dichotomy, and antisymmetry is stated under a balanced hypothesis so equal ranks force balanced equality. No classical $\mathrm{toInt}$ nonnegativity path is used.

why it matters in Recognition Science

Ratio-orbit order modules import this file to define $\mathrm{leQ}$ by cross-multiplication in signed orbits and to obtain reflexivity, totality, positivity, and add-monotonicity without choice. Signed-orbit congruence and multiplication lemmas (left/right congruence of $\le$ under balanced hypotheses, right-multiplication iff under a nonneg flag) likewise depend on the choice-free $\le$ package. Closing this bridge keeps the entire Grow stack aligned with the recognition program’s preference for constructive, representative-free comparisons before any continuum or forcing-chain physics is attached.

scope and limits

Does not define ratio-orbit $\mathrm{leQ}$ or density/mediant arguments; those live in importers.
Does not route nonnegativity through $\mathrm{toInt}\ge 0$; that path is explicitly avoided.
Does not prove antisymmetry without a balanced hypothesis on the compared orbits.
Does not construct integers/rationals themselves; it only orders already-formed signed orbits.
Does not address continuum completeness or physical constants from the forcing chain.

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational module_import