traceDisplay_posInt_ge_two
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real doubled-trace display of any positive integer ratio-orbit is at least 2. Cost and character-factorization arguments cite this as the integer lower bound feeding the rational-trace and base-two specializations. The proof applies monotonicity from the unit orbit, uses unit-zero calibration, and casts the resulting nonnegativity into the display.
Claim. Let $F$ be a map on ratio-orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). If $q$ is a positive integer orbit (i.e. $q$ equals some natural $n\ge 1$ as a rational), then the real display of the doubled trace of $F$ at $q$ satisfies $2\le \mathrm{traceDisplay}(F,q)$.
background
In the real character-factorization module, cost is carried by maps $F$ on ratio-orbits. The anchor-free pack SansAnchorHypotheses bundles four structural conditions: base-sans-two (unit orbit maps to zero), sign-reversing, monotonicity on positive orbits, and zero-calibration of the doubled trace. These match the structural native-cost hypotheses without an external anchor.
A positive integer orbit is a ratio-orbit whose rational value is a natural number $n\ge 1$. The doubled trace of $F$ is a carrier-valued object; its real display is the cast of that carrier's rational value to $\mathbb{R}$. The local goal is a uniform lower bound of 2 for that display on every positive integer orbit, which is the integer case of the cost lower bound used later for rational traces.
Upstream, rational arithmetic on orbits (add_toRat, mul_toRat, one_toRat) lets inequalities on carriers be rewritten as ordinary rational comparisons. Monotonicity in the pack compares $F$ at the unit orbit and at $q$ once $1\le q$ is known.
proof idea
First record that the unit orbit is a positive integer orbit (witness $n=1$). Unpack the hypothesis on $q$ to a natural $n\ge 1$ with matching rational value, and deduce $1\le q$ as rationals. Apply the pack's monotonicity at the unit and at $q$ to get $F(1)\le F(q)$ in the orbit order. Rewrite via base-sans-two unit-zero so the left side is the zero orbit. Unfold the display through the doubled-trace definitions and the rational arithmetic lemmas (mul_toRat, add_toRat, two_toRat, one_toRat), then finish by norm_num and casting the resulting $0\le (F q).\mathrm{toRat}$ into the real inequality $2\le \mathrm{traceDisplay}(F,q)$.
why it matters
This is the integer lower-bound step inside real character factorization of native cost. Downstream, rationalTrace_nat_ge_two reduces the natural-number rational-trace bound to this theorem by viewing $n$ as a ratio-orbit, and traceDisplay_two_ge_two is the immediate specialization at the orbit two. Together they pin the cost floor at the first positive integers before the factorization and uniqueness arguments proceed.
In the Recognition framework the bound supports the native-cost uniqueness chain (PRC native cost uniqueness import) that feeds the J-cost story: the self-similar cost forced by the Recognition Composition Law and T5 J-uniqueness must sit above this discrete floor on integer orbits. It is a proved lemma, not scaffolding; it closes the positive-integer case of the display inequality used by the rational-trace ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.