calibrated_mul
plain-language theorem explainer
Calibration of a ratio character is closed under products: if a PRC ratio character acts as the identity on two ratio-orbit directions, multiplicativity forces the same on their product. Rigidity arguments cite this when propagating a single-point calibration (typically at a prime) along the cyclic subgroup it generates. The proof is a short rational-display calculation: cross-equivalence reduces to equality of verifier rationals, then character and orbit multiplicativity finish it.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $\chi$ is calibrated at orbits $x$ and $y$ (meaning $\chi(x)$ is cross-equivalent to $x$, and $\chi(y)$ to $y$), then $\chi$ is calibrated at the product orbit $x\cdot y$.
background
In the Primitive Recognition Calculus continuum layer, ratio orbits package signed integer distinctions up to scaling and carry a verifier rational display. A PRC ratio character is a multiplicative map on these orbits. Calibration at an orbit $q$ means the character acts as the identity there: $\chi(q)$ is cross-equivalent to $q$ itself. The module records that calibration at two is the single-point datum the PRC cost hypotheses actually carry.
Cross-equivalence of orbits is equivalent to equality of their rational displays (K4.10). Multiplicativity of the character on that display, together with multiplicativity of the orbit product, therefore lets identity-at-points pass to products. Upstream CostAxioms calibration normalizes the second derivative of a cost at the log-origin to 1; the character-side calibration here is the discrete counterpart used later to force the generated cost back to the canonical J-cost.
proof idea
Unfold the calibration predicate on both hypotheses and the goal. Rewrite all three cross-equivalence statements via the K4.10 bridge into equalities of rational displays. Apply the character's multiplicativity on the rational display together with the orbit product formula for that display, then substitute the two calibration equalities. The goal reduces to ordinary multiplication of equal rationals.
why it matters
This is the multiplicative closure step inside character-rigidity forcing. It feeds the square case (calibration at $p$ implies calibration at $p\cdot p$, obtained by applying the product rule to a repeated argument) and the single-prime rigidity theorem: a character calibrated at a prime direction $p$ remains the identity on $p\cdot p$ and on $p^{-1}$, and the cost it generates is forced to the canonical PRC J-cost on that direction. That local engine precedes the global all-primes step. In the RS forcing chain this supports uniqueness of the cost functional (T5 J-uniqueness territory): calibrated multiplicativity pins the character, hence the cost, to the identity/J form along generated directions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.