structural_forces_positive
plain-language theorem explainer
Under the structural native-cost ledger on a map F of rational orbits, F is nonnegative on every positive orbit. Positivity is derived, not assumed: recognizing a positive imbalance never pays. The structural stratification certificate cites this as its positivity field. Proof applies uniqueness of the structural target, rewrites via the cross-display identity onto the closed J-cost, and invokes J-nonnegativity on positive orbits.
Claim. Let $F$ map rational orbits to rational orbits and satisfy the structural native-cost ledger: reciprocity, normalization invariance, the nonzero composition law, unit-zero, the single orbit-2 anchor, sign reversal, monotonicity, and zero-orbit calibration. Then for every orbit $q$ with positive rational display, the rational display of $F(q)$ is nonnegative: $0 < q^{\mathrm{rat}} \Rightarrow 0 \le (F q)^{\mathrm{rat}}$.
background
The ambient module builds a structural ledger for native cost on ratio orbits: integer-numerator / nonzero-orbit-denominator displays of rational imbalance. The structural hypothesis package is the slim native package (reciprocity, normalization invariance, nonzero composition law, unit-zero, single orbit-2 anchor) plus sign reversal, monotonicity, and a zero-orbit calibration of the doubled trace. Compared with earlier slim ledgers, countable prime-pair products and signed-unit calibration are dropped; nothing that replaces them names the canonical cost.
Positivity is the predicate that $F$ never returns a negative rational display on a positive orbit. The doc-comment states the intended meaning directly: recognizing a difference never pays, and this is to be derived rather than postulated. The closed-form cost on orbits is the standard J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely by the Recognition Composition Law in the T5 step of the forcing chain; sibling lemmas record that this J is nonnegative on positive rationals and vanishes only at the unit orbit.
Upstream uniqueness for the structural target identifies any $F$ obeying the ledger with that closed form on each orbit, so positivity reduces to a property of J rather than an extra axiom on F.
proof idea
Term-mode proof, four steps. Fix an orbit $q$ with positive rational display. Apply the structural uniqueness theorem at $q$ under the structural hypotheses on $F$, obtaining that $F(q)$ matches the uniqueness target. Feed that equality into the cross-display identity, which rewrites the target display as the closed J-cost evaluated on the orbit. Rewrite once more by the sibling that identifies the orbit J with the rational J-display. Conclude by the sibling nonnegativity lemma for J on positive orbits.
why it matters
This is the positivity half of free-side structural stratification. Downstream, the structural stratification certificate packages four fields: uniqueness of the structural native-cost target, contraction of the slim ledger, this positivity theorem, and inhabitedness of the gauge orbit after the anchor is removed. Together those claims say the surviving anchor is a genuine unit gauge: the gauge orbit is inhabited (so the anchor is a real choice, not a redundancy) and the anchor value determines everything else (so it is the only choice).
In the Recognition framework this discharges the slogan that positivity is a theorem, not an axiom. It sits under the native-cost / J-uniqueness line (T5 and the Recognition Composition Law): once structural hypotheses force $F$ onto the closed J-cost, nonnegativity is inherited from $J\ge 0$ on positive displays. No open scaffold remains on this declaration; claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.