positive
plain-language theorem explainer
PRC-native strict positivity on a ratio-orbit display: the signed numerator is nonnegative and not balanced against zero. Downstream action and cost-algebra results cite it to restrict paths and costs to the positive cone. The body is a two-conjunct Prop definition on the numerator only.
Claim. A ratio orbit $q$ (signed numerator over a nonzero orbit denominator) is positive when its numerator is nonnegative in the signed-orbit sense and is not balanced with the zero signed orbit.
background
In the Primitive Recognition Calculus, rationals are built from orbit data rather than classical $\mathbb{Z}$ and $\mathbb{Q}$. A ratio orbit is a display with a signed-orbit numerator and a nonzero distinction-natural denominator. Signed orbits carry an internal balance relation: two signed orbits balance when the sum of one side's positive length with the other's negative length equals the swapped sum.
Nonnegativity of a signed orbit means it balances some purely positive orbit (an orbit of a distinction natural). The zero signed orbit is the neutral element for that balance calculus. Positivity of a ratio orbit is then stated entirely on the numerator: nonnegative and not balanced with zero. The denominator's nonzero status is already part of the ratio-orbit structure, so it is not restated in the positivity predicate.
This sits in the rational-field layer that lifts integer-orbit arithmetic toward a PRC-native ordered field used by cost and action developments.
proof idea
Definitional, not a proof. The predicate is the conjunction of signed-orbit nonnegativity of the numerator with the negation of balance between that numerator and the zero signed orbit. No lemmas are applied; consumers unfold or rewrite with the companion characterizations (e.g. positivity iff the classical rational image is positive).
why it matters
Strict positivity is the gate for admissible paths and cost-rate calculus in the action layer. Euler–Lagrange uniqueness for the cost rate (critical paths among positive continuous trajectories are constantly $1$) and the implication from the EL equation to the constant ground state both quantify over positive paths. Convexity of the $J$-action on interpolations and the local-to-global minimum principle likewise live on admissible (strictly positive) path space; the straight-line interpolation constructor preserves positivity on $[0,1]$.
In cost algebra, the canonical recognition cost system and right-cancellation for cost composition use the positive cone so that the $J$-cost geometry stays on the side where the Recognition Composition Law and the unique $J(x)=\cosh(\log x)-1$ minimum at $1$ are well-behaved. The definition is the PRC-native stand-in for $q>0$ before classical embeddings are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.