nonnegFlag_iff_nonneg_cf
plain-language theorem explainer
The structural nonnegative Boolean flag on a signed orbit agrees with internal nonnegativity, without routing through ℤ. Anyone building the choice-free ordered-field tower for ratios cites this bridge. The proof rewrites both sides to the same ℕ comparison of δ-orbit positions via two already choice-free lemmas.
Claim. For every signed orbit $z$, the structural nonnegative Boolean flag of $z$ equals true if and only if $z$ is internally nonnegative (i.e., there exists a positive orbit with which $z$ balances).
background
Signed orbits are the integer-like objects of the primitive recognition calculus: each carries a positive and a negative δ-orbit side. Internal nonnegativity means $z$ balances with some pure positive orbit. The structural nonnegative flag is the Boolean leq comparison of the two sides' δ-orbit positions, a computable predicate.
The parent module IntegerRational already defines order via toInt : SignedOrbit → ℤ and Mathlib's integer order. Those characterizations inherit Classical.choice. This module re-grounds the same order on finite ℕ positions of the δ-orbit, so that #print axioms stays inside {propext, Quot.sound}.
Two upstream bridges do the work: internal nonnegativity collapses to z.neg.toNat ≤ z.pos.toNat (via the choice-free balanced-length equality), and the structural Boolean leq agrees with that same ℕ order by bare induction plus omega.
proof idea
Three-step term proof. First rewrite the right-hand side with nonneg_iff_toNat_le, so internal nonnegativity becomes the ℕ fact z.neg.toNat ≤ z.pos.toNat. Unfold the structural flag to DistinctionNat.leq z.neg z.pos. Finish by leq_eq_true_iff_cf, which equates that Boolean to the same ℕ inequality. Both sides match; no toInt, no classical decidability simp.
why it matters
This is the flag-to-Prop bridge the choice-free order needs. Downstream, le_iff_nonnegFlag_sub_cf rewrites the signed-orbit order as nonnegativity of the difference via this theorem, replacing the choice-tainted le_iff_nonnegFlag_sub. That order characterization then feeds reflexivity, transitivity, totality, and antisymmetry-to-balanced, all discharged by pure omega on ℕ.
The module doc states the forced-floor receipt: every theorem here prints axioms inside {propext, Quot.sound}. That is the base the ratio_* ordered-field tower requires. In the broader Recognition stack this keeps the integer/rational layer free of classical choice before continuum or measure structure appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.