rationalTrace_two_pow_eq_two
plain-language theorem explainer
If an anchor-free ratio-orbit map has doubled rational trace equal to 2 at the integer 2, then the same trace equals 2 at every pure power of two. Cost and character-factorization arguments cite this to freeze the dyadic ray before lifting to all naturals. The proof is two-step induction on the exponent, feeding the d'Alembert identity for the rational trace at each step.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). Write $T_F$ for the doubled rational trace of $F$. If $T_F(2)=2$, then $T_F(2^k)=2$ for every natural number $k$.
background
In the real-character factorization of native cost, maps $F$ act on ratio orbits (integer numerator over a nonzero distinction-orbit denominator). The doubled trace is packaged as an honest real-valued function on rational displays: $T_F(x)$ is the trace display of $F$ at the orbit of the rational $x$.
The ambient hypothesis pack SansAnchorHypotheses is the anchor-free structural pack matching PRC native-cost hypotheses without an anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Under that pack one already has $T_F(1)=2$ and the multiplicative d'Alembert identity
$T_F(xy)+T_F(x/y)=T_F(x),T_F(y)$ for nonzero rationals $x,y$.
The local goal is to lock the entire dyadic ray once the single value $T_F(2)=2$ is known, before any extension from powers of two to arbitrary naturals.
proof idea
Fix $k$ and run Nat.twoStepInduction on the exponent.
- Base $k=0$: $2^0=1$, so $T_F(1)=2$ by
rationalTrace_one. - Base $k=1$: immediate from the hypothesis $T_F(2)=2$.
- Step: assume the claim at $m$ and $m+1$. Apply
rationalTrace_dAlembertat $x=2^{m+1}$ and $y=2$ (both nonzero). The product identity $2^{m+1}\cdot 2=2^{m+2}$ and the quotient identity $2^{m+1}/2=2^m$ rewrite the d'Alembert equation to $T_F(2^{m+2})+T_F(2^m)=T_F(2^{m+1}),T_F(2)$. Substitute the two inductive values and $T_F(2)=2$, then finish bylinarith.
why it matters
This lemma is the dyadic half of the freeze-at-two program inside real character factorization. Its sole recorded consumer is rationalTrace_nat_eq_two_of_two_eq_two, which lifts $T_F(2)=2$ from pure powers of two to every natural $n\ge 1$. That lift is the bridge from a single integer calibration to a constant rational trace on $\mathbb{N}$, feeding uniqueness of the real character of native cost under the anchor-free pack.
In the broader Recognition stack the doubled-trace d'Alembert law is the rational shadow of the Recognition Composition Law that forces the J-cost (T5). Holding $T_F\equiv 2$ on the dyadic ray is the discrete counterpart of the constant character that later matches the unique J-cost factorization; without it the passage from structural native-cost hypotheses to a rigid real character would stall at the integer 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.