abs_toInt_of_nonnegFlag
plain-language theorem explainer
When a signed orbit is flagged nonnegative, its absolute-value orbit, read as a natural and cast to ℤ, recovers the orbit's integer value. Order and balance lemmas for signed orbits cite this bridge between the structural abs and the recovered Int. The proof rewrites by the abs-to-natAbs identity and applies the standard ofNat-natAbs rule under the flag-to-nonnegativity equivalence.
Claim. For every signed orbit $z$, if the structural nonnegative flag of $z$ is true, then $\mathrm{nat}(|z|)\colon\mathbb{Z}$ equals the recovered integer of $z$. Equivalently, under $0\le z$ in the recovered $\mathbb{Z}$, the absolute-value orbit displays exactly $z$.
background
Signed orbits are the internal model of integers in the primitive recognition calculus: a pair of distinction-nat sides (positive and negative legs) with a recovery map to Lean's Int. The absolute value of a signed orbit is the distinction-nat absolute difference of those legs; its toNat is the iteration count of that orbit position.
The nonnegative flag is a computable Bool from structural comparison of the two legs (leq of neg against pos). Upstream, that flag is equivalent to recovered nonnegativity: the flag is true if and only if $0\le z$ in $\mathbb{Z}$. Separately, the absolute-value display identity states that the nat of the internal abs equals Int.natAbs of the recovered integer.
This module builds the order surface on those signed orbits (reflexivity, totality, trichotomy, sign-flag exclusivity) so that integer order is certified from recognition structure rather than assumed as a primitive.
proof idea
Term proof in two steps. First rewrite the left-hand side by the absolute-value display theorem, replacing z.abs.toNat with Int.natAbs z.toInt. The goal becomes the cast of that natAbs equal to z.toInt. Discharge by Int.ofNat_natAbs_of_nonneg, feeding nonnegativity of z.toInt obtained by modus ponens on the flag-equivalence theorem from the hypothesis that the nonnegative flag is true.
why it matters
This is the display bridge that lets nonnegative signed orbits be replaced by the positive orbit of their absolute value under balance. Immediate parents include the one-line balance-from-nonneg-flag lemma, the iff relating balance against ofOrbit abs to the nonnegative flag, and the dual negate/abs characterization for the negative flag. Those feed the closed integer-order certificate ("the internal signed-orbit order surface is closed") and ratio-orbit balance identities used when multiplying by reciprocal numerators.
In the Recognition foundation stack this sits under arithmetic and integers reconstructed from logic, before the forcing chain's later physics landmarks (J-uniqueness, phi, eight-tick, D=3). It does not itself force constants; it seals that internal order and abs agree with recovered ℤ on the nonnegative cone, which later certificates assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.