add_pos
plain-language theorem explainer
The positive component of a signed-orbit sum is just the sum of the positive components. Anyone working with signed orbit arithmetic (mediants, ratio comparisons, seed-closed levels) cites this as a simp fact. The proof is pure definitional equality (rfl).
Claim. For any two signed orbits $a$ and $b$ (each a pair of distinction naturals interpreted as $\mathrm{pos}-\mathrm{neg}$), the positive part of their sum equals the sum of the positive parts: $(\mathrm{add}\,a\,b)_{\mathrm{pos}} = a_{\mathrm{pos}} + b_{\mathrm{pos}}$.
background
In the Primitive Recognition Calculus, a signed orbit is a pair of distinction naturals (pos, neg) with intended meaning pos - neg. Addition on signed orbits is componentwise: the sum has positive part a.pos + b.pos and negative part a.neg + b.neg.
This lives in the IntegerRational layer of the foundation, which builds integer and rational structure on top of orbit arithmetic. Distinction naturals are the nonnegative counting type used throughout PRC; signed orbits are the first step toward differences and ratios used in mediant constructions and density arguments.
Upstream, positivity lemmas for monotone multiplicative maps (Cost and PRCNativeCostStructuralLedger) establish that related cost functions stay positive above the unit, but this particular fact is purely structural on the signed-orbit type itself.
proof idea
One-line definitional proof: rfl. The theorem is marked @[simp], so it unfolds automatically whenever a goal mentions the positive projection of a signed-orbit sum. No lemmas are applied; equality holds by the definition of add on SignedOrbit.
why it matters
Componentwise projection lemmas keep signed-orbit arithmetic usable under simp. Downstream, ltQ_mediant rewrites mediant comparisons via SignedOrbit.add_pos (and the companion add_neg) to show mediants sit strictly between positive ratio orbits. The same fact feeds seed-closed level positivity and multilevel composition in the Unified Forcing Chain, and appears in Born-rule normalization and nonnegativity arguments in Measurement, as well as open-first-quadrant product positivity in the Gravity SevenGaps Wick analysis.
It is scaffolding glue rather than a deep forcing step: it does not itself force phi, the eight-tick octave, or D = 3, but it keeps the integer/rational orbit layer transparent so those later chain steps can reason about sums without unfolding structure fields by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.