target_global_identity_from_one_point_calibration
plain-language theorem explainer
Names the open target that one-point calibration of a PRC ratio character at the orbit of 2 forces calibration on every nonzero ratio orbit. Anyone tracking the remaining gap after native cost uniqueness and per-direction rigidity would cite it. The body is a pure Prop alias with no proof content.
Claim. The proposition asserting: every primitive-recognition ratio character that is calibrated at the ratio orbit of $2$ is calibrated at every nonzero ratio orbit (global identity from a single calibration point).
background
In the continuum layer of Primitive Recognition Calculus, costs on positive ratios are measured by the J-cost $J(x)=(x+x^{-1})/2-1$, the unique continuous solution of the Recognition Composition Law fixed by the forcing chain (T5). Ratio orbits are the quotient-native carriers; characters on those orbits encode multiplicative cost data without classical choice on $\mathbb{R}$.
The module develops forced $J$ on the completion and per-direction rigidity for calibrated characters. Native cost uniqueness already pins the cost formula along generated directions once local data match $J$. What remains is whether calibration at a single generator (the orbit of two) propagates across all independent prime directions at once.
Upstream, field-display $J$ on classical $\mathbb{R}$ agrees with the quotient-native cost on rational displays, but the capstone path stays choice-free on ratio orbits. Constants and cost dynamics live in one countable field; the continuum is not required for that loop.
proof idea
No proof. The declaration is a one-line def equating this name to the Prop target_OnePointCalibrationForcesGlobalIdentity. It records an open target rather than discharging it. Sibling results supply per-direction rigidity and forced $J$ on the completion; they are not applied here.
why it matters
This is the residual all-prime-directions statement that native cost uniqueness leaves open. The continuum capstone gives rigidity along each direction and forces the canonical cost to the $J$ formula on the completion; global identity from calibration only at two is the missing propagation step across independent primes.
In the Recognition framework it sits under T5 J-uniqueness and the RCL: if one-point calibration at two spreads to every nonzero orbit, the character is forced to the global $J$-cost everywhere, closing the uniqueness story on the quotient-native carrier without classical choice. No downstream theorems currently consume it (used-by is empty); it is a named open target for future work, not a proved link in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.