abs_toInt_of_negativeFlag
plain-language theorem explainer
When a signed orbit is flagged strictly negative, its absolute-value orbit, read as a natural and cast to ℤ, equals the classical negation of the recovered integer. Order and balance lemmas cite this bridge between structural abs and sign flip. Proof: flag implies toInt < 0, rewrite by abs_toNat, finish with the standard natAbs identity on nonpositive integers.
Claim. Let $z$ be a signed orbit. If the negative flag of $z$ is true, then $(\lvert z\rvert)_{\mathbb{N}}$ viewed in $\mathbb{Z}$ equals $-z^{\mathbb{Z}}$, where $\lvert z\rvert$ is the absolute-value distinction orbit of $z$ and $z^{\mathbb{Z}}$ is the integer recovered from $z$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: each carries a positive and negative distinction count, a nonnegative flag, and recovery maps into classical $\mathbb{N}$ and $\mathbb{Z}$. The absolute value of a signed orbit is the distinction-nat absolute difference of those two counts; its toNat display is the iteration count of that orbit.
The negative flag is the Boolean negation of the structural nonnegative flag. Upstream, negativeFlag_eq_true_iff_toInt_neg equates that flag with classical strict negativity of the recovered integer. Separately, abs_toNat states that the natural display of the absolute-value orbit equals Int.natAbs of the recovered integer.
This module builds the internal order surface on signed orbits (reflexivity, totality, trichotomy, flag characterizations of $\le 0$ and $< 0$). The present lemma is the signed-display identity needed when the orbit sits strictly below zero.
proof idea
Term-mode, three steps. First apply negativeFlag_eq_true_iff_toInt_neg (modus ponens on the hypothesis) to obtain $z^{\mathbb{Z}} < 0$. Rewrite the left-hand side by abs_toNat, replacing the structural abs display with Int.natAbs z.toInt. Conclude with the Mathlib identity Int.ofNat_natAbs_of_nonpos on le_of_lt of that negativity fact, which converts natAbs of a nonpositive integer into its classical negation.
why it matters
Closes the negative branch of the abs-display bridge used throughout the integer-order surface. Downstream, balanced_of_negativeFlag applies it to show a negative orbit is balanced against the negation of the orbit built from its abs; that is the signed-orbit form of $z + \lvert z\rvert = 0$ when $z < 0$. The same identity is invoked in the ratio-orbit balance lemma num_mul_recipNonzero_num_balanced_ofOrbit_den_mul_abs, where abs of a nonzero numerator appears in a denominator product.
It also sits under integer_order_certificate, the package that records the closed display laws for truncated subtraction, $\le$, abs-diff, and signed nonnegativity. In the Recognition foundation stack this is arithmetic infrastructure (integers and order recovered from logic orbits), not yet a forcing-chain landmark (T5–T8), but it is required before rational and ladder constructions can treat signed magnitudes uniformly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.