rationalSignCharacter_of_pos
plain-language theorem explainer
For every positive rational the real sign character equals +1. Cost and character-factorization arguments cite this when restricting the degenerate anchor character to the positive ray, and when checking that the real character candidate is principal on positive integer orbits. The proof is a one-line simplification of the piecewise definition under the positivity hypothesis.
Claim. If $x \in \mathbb{Q}$ satisfies $x > 0$, then the rational sign character of $x$ equals $1$ (as a real number).
background
In the real-character factorization layer of the cost module, the rational sign character is the piecewise map on $\mathbb{Q}$ that sends $0$ to $0$, positives to $+1$, and negatives to $-1$. It is the degenerate anchor character against which non-degenerate extractions from the doubled trace are compared.
The surrounding development builds real multiplicative characters from ratio-orbit data under sans-anchor hypotheses, tying the cost side of Recognition Science to the Recognition Composition Law and the unique $J$-cost $J(x)=(x+x^{-1})/2-1$. Positive rationals (and positive integer orbits) are the natural domain on which the principal character should be identically one.
Upstream, the definition of the sign character is purely arithmetic; the factorization theorems then feed that value into trace-display identities and positivity statements for candidate characters.
proof idea
Term-mode via simp on the definition of the rational sign character. Unfolding the piecewise definition, the branch $x=0$ is ruled out by ne_of_gt from $x>0$, and the remaining positive branch returns $1$ by the hypothesis $0<x$. No external lemmas beyond the definition and basic order facts are required.
why it matters
This is the positive-ray normalization of the degenerate anchor in real character factorization. Downstream, realCharacterCandidate_principal_on_pos_int uses it to show that under sans-anchor hypotheses the candidate character is at least $1$ on every positive integer orbit, and realCharacterCandidate_trace_of_pos uses positivity of the underlying rational to relate the candidate plus its inverse to the trace display.
In the broader RS cost story, characters extracted from the doubled trace must recover the principal (trivial) character on positives when the anchor is pure sign; that is the baseline against which non-trivial $J$-driven extractions are measured. The result is local arithmetic bookkeeping rather than a forcing-chain step (T5–T8), but it is required scaffolding for any claim that the real character candidate is well-normalized on the positive phi-ladder side of the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.