Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitZeroLeIffNonnegFlagChoiceFree

show as:
view Lean formalization →

Choice-free bridge between the signed-orbit order and the Boolean nonnegativity flag: zero is at most a signed orbit exactly when that orbit's nonnegFlag is true. Anyone building ratio or integer order without Classical.choice cites this. The argument reuses the choice-free order foundation and the integer display only as a verifier, not as the definition of ≤.

claimFor every signed orbit $s$, one has $0 \leq s$ if and only if the Boolean nonnegativity flag of $s$ is true, with the order and the flag characterized without routing through Mathlib's $\mathbb{Z}$ order (hence without $\mathrm{Classical.choice}$).

background

Primitive Recognition Calculus builds rationals and order from orbits of positive distinctions and signed orbits, rather than from Mathlib integers as the primary objects. A signed orbit packages a sign with an underlying positive orbit; the Boolean nonnegFlag is a constructive witness that the sign is nonnegative.

The companion module on choice-free signed-orbit order records the problem this file solves: the older characterizations le_iff_toInt_le and nonneg_iff_toInt_nonneg go through SignedOrbit.toInt and Mathlib's ordered integers, which import Classical.choice. Every downstream rung (ratio reflexivity, cross-multiplication order on ratio orbits) would otherwise inherit that taint.

Cross-multiplication order on ratio orbits compares $p$ and $q$ by asking whether the signed product $p.\mathrm{num}\cdot q.\mathrm{den}$ is $\leq$ $q.\mathrm{num}\cdot p.\mathrm{den}$ after casting dens via SignedOrbit.ofOrbit. That comparison needs a clean $0\leq s$ test.

proof idea

The module is a thin Grow layer over the choice-free signed-orbit order foundation and the integer/orbit arithmetic imports. It exposes a single named equivalence (sibling zero_le_iff_nonnegFlag_cf) linking the order predicate $0\leq s$ to the Boolean flag, proved by aligning the choice-free nonnegativity characterization with the flag's definition rather than by re-deriving order from toInt. No separate classical case split on the sign is introduced.

why it matters in Recognition Science

Inside the Foundation forcing stack, ratio and integer order must stay choice-free so later rungs (J-cost comparisons, defect distances, and the path toward T5–T8) do not silently depend on classical choice. This module closes the zero-versus-flag gap that SignedOrbitOrderChoiceFree flags: once $0\leq s$ is interchangeable with the flag, cross-multiplication lemmas such as those in RatioOrbitLeReflTotal can stay constructive. No downstream used_by edges are recorded yet; the file is infrastructure for the Grow order ladder rather than a leaf physics claim.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (1)