pair_two_case_split
plain-language theorem explainer
On positive rationals, if a character value u at the two-axis is 2 or 1/2, the product uv hits 2P or its inverse, and v squared hits P squared or its inverse, then v itself is P or 1/P. Anyone proving that pair-product consistency plus two-point calibration forces prime-axis calibration cites this. The proof is exhaustive rational case analysis with linear combinations and positivity contradictions.
Claim. Let $u,v,P\in\mathbb{Q}$ with $P\neq 0$ and $P\ge 1$. Suppose $u\in\{2,2^{-1}\}$, $uv\in\{2P,(2P)^{-1}\}$, and $v^2\in\{P^2,(P^2)^{-1}\}$. Then $v\in\{P,P^{-1}\}$.
background
In the Primitive Recognition Calculus, native costs are calibrated on ratio orbits. The two-orbit is the distinguished base axis; primes supply the remaining axes. A ratio character $\chi$ assigns orbit values whose induced cost must match the native J-cost on calibrated axes.
The local setting is the pure rational arithmetic behind character transport: $u$ is the character value on the two-axis, $v$ on a probed prime axis, and $P\ge 1$ is the prime display. Pair-product consistency constrains $uv$ relative to $2P$; squaring consistency constrains $v^2$ relative to $P^2$. Nonzero product lemmas (orbit arithmetic) keep denominators live.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) motivate why calibration on two plus pairs should force calibration on every prime; this lemma is the field-level case split that makes that transport algebraic.
proof idea
Tactic proof by nested rcases on the three disjunctions. First obtain $P^4\ge 1$, $2P\neq 0$, and $P^2\neq 0$.
Case $u=2$: if $uv=2P$ then $v=P$ by linarith. If $uv=(2P)^{-1}$, derive $4Pv=1$; both square branches yield contradictions ($16P^4=1$ against $P\ge 1$, or $15=0$).
Case $u=2^{-1}$: if $uv=2P$ then $v=4P$; both square branches contradict ($15P^2=0$ with $P^2>0$, or $16P^4=1$). If $uv=(2P)^{-1}$, obtain $vP=1$ and conclude $v=P^{-1}$ by field simplification.
Tools: linear_combination, linarith/nlinarith, positivity, norm_num, field_simp, and mul_ne_zero/inv_mul_cancel₀.
why it matters
This is the core rational engine for character_pair_two_calibration_forces_prime_calibration: prime-pair products plus base two-point calibration force cost calibration on every native prime axis. Downstream doc: the all-prime family is not independent data once the pair field and the base ledger's two-calibration are present; this was the transport the round-1 premise ledger was missing.
In the Recognition framework it shrinks the native-cost hypothesis surface: uniqueness and minimality arguments no longer need an independent prime-axis calibration family. It sits under the PRC native-cost minimality development that refutes over-strong signed factorizations (zero-flat countermodels) while recovering the slim calibrated class. Landmark contact is indirect: J-uniqueness (T5) and the recognition cost stack motivate why character-generated costs must hit the two-orbit and then transport; the lemma itself is pure $\mathbb{Q}$ arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.