traceDisplay_one
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real-valued doubled trace of the unit ratio orbit equals 2. Anyone normalizing PRC native cost or building the real character factorization would cite this unit calibration. The proof is a short simplification through the doubled-trace definition and the unit-zero clause of the base pack, finished by numeric normalization.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without two-anchor, sign-reversing, monotone, and zero-calibrated doubled trace). Then the real display of the doubled native cost of $F$ at the unit orbit equals $2$.
background
Ratio orbits are the rational display used in the primitive recognition calculus: an integer (signed-orbit) numerator over a nonzero distinction-nat denominator, with a canonical map to $\mathbb{Q}$ via toRat. Addition and multiplication of orbits commute with that map (add_toRat, mul_toRat), and the unit orbit maps to $1$.
The module builds a real character factorization of native cost. The doubled trace of a carrier map $F$ is first valued in ratio orbits, then cast to $\mathbb{R}$ by traceDisplay: the real number underlying (nativeCostDoubledTrace F q).toRat. The hypothesis pack SansAnchorHypotheses is the anchor-free structural pack: base axioms without a two-anchor, sign-reversing and monotone native cost, and zero-calibrated doubled trace.
Among the base axioms is a unit-zero clause: the doubled-trace value at the multiplicative unit is the zero orbit (before the conventional factor of two that appears in the real display).
proof idea
Term-mode proof by simplification then numeric close. Unfold traceDisplay, the native doubled-trace wrapper, and the doubled-trace value. Apply the unit-zero field of hF.base_sans_two, so the carrier expression at the unit orbit collapses. Rewrite through mul_toRat, add_toRat, zero_toRat, one_toRat, and two_toRat to land in ordinary rationals, then norm_num yields the real equality to $2$.
why it matters
Unit calibration of the real doubled-trace display. Downstream, rationalTrace_one is a one-line rewrite: the rational-trace specialization at $1$ equals traceDisplay at the unit orbit, so this theorem supplies rationalTrace F 1 = 2 under the same pack.
In the Recognition cost stack this pins the normalization of the native cost character before real factorization and uniqueness arguments (the module imports PRC native-cost uniqueness). It is the concrete statement that the doubled display at the identity ratio is the constant $2$, matching the usual $J$-cost normalization $J(1)=0$ after the doubling convention that sends the zero orbit to the real value $2$ in the display layer. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.