balanced_ofOrbit_abs_iff_nonnegFlag
plain-language theorem explainer
A signed orbit is integer-equivalent to the non-negative orbit built from its absolute value exactly when its non-negative flag is set. Order and sign lemmas in the Primitive Recognition Calculus cite this as the bridge between the internal balance relation and the nonnegativity flag. The proof rewrites balance to integer equality, then splits: one direction uses nonnegativity of a natural cast, the other applies the absolute-value-to-integer identity under a true flag.
Claim. For every signed orbit $z$, $z$ is balanced with the signed orbit obtained by viewing $|z|$ as a non-negative orbit if and only if the non-negative flag of $z$ equals true. Equivalently, $z$ and $\mathrm{ofOrbit}(|z|)$ represent the same integer precisely when $z$ is flagged non-negative.
background
In the Primitive Recognition Calculus, integers are carried as signed orbits: a pair of distinction-orbit positions (positive and negative legs) together with sign flags. Absolute value abs is the distinction-orbit absolute difference of those legs. The constructor ofOrbit lifts a plain orbit position to a signed orbit on the non-negative side.
Balance is the internal integer equality of K4.9: two signed orbits $a,b$ satisfy $a.\mathrm{pos}+b.\mathrm{neg}=b.\mathrm{pos}+a.\mathrm{neg}$. The bridge theorem balanced_iff_toInt_eq states that this relation holds exactly when the conservative integer displays agree: $a.\mathrm{toInt}=b.\mathrm{toInt}$. The non-negative flag is characterized by nonnegFlag_eq_true_iff as nonnegativity of that integer display.
Upstream, abs_toInt_of_nonnegFlag already records that if the flag is true then the natural absolute value, cast to $\mathbb{Z}$, equals toInt. The present statement packages that identity into an iff with balance against ofOrbit of the absolute value.
proof idea
Term-mode proof. Rewrite the goal with balanced_iff_toInt_eq and ofOrbit_toInt, so the claim becomes
$z.\mathrm{toInt}=(|z|.\mathrm{toNat}:\mathbb{Z})$ iff the non-negative flag is true.
Left-to-right: assume the integer equality, rewrite the flag via nonnegFlag_eq_true_iff, substitute the equality, and finish by Int.natCast_nonneg on $|z|.\mathrm{toNat}$.
Right-to-left: assume the flag is true and apply the symmetric form of abs_toInt_of_nonnegFlag, which supplies exactly $(|z|.\mathrm{toNat}:\mathbb{Z})=z.\mathrm{toInt}$.
why it matters
This is a local sign-display lemma inside IntegerOrder: nonnegativity of a signed orbit is equivalent to being balanced with the absolute-value orbit. The negative counterpart not_balanced_ofOrbit_abs_of_negativeFlag is an immediate corollary (assume balance, pull the flag true, contradict a true negative flag via exclusivity of the sign flags).
Downstream it feeds the closed certificate integer_order_certificate, whose fields package the signed nonnegativity and flag displays that the order surface exposes. In the broader Recognition stack this sits in the foundation layer that builds integers and order from recognition orbits before the forcing chain (T5 J-uniqueness through T8 dimension) and the mass ladder; it does not itself force $\varphi$ or $D=3$, but it keeps the integer order surface choice-free and internal to $\delta$-orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.