pta_sstar_same_base
plain-language theorem explainer
PTA stochastic GW strain and S-star periapsis residual share the same recognition correction φ^(-44). Channel auditors cite this when collapsing those two D5 falsifiers onto one base scale. The equality is definitional: both sides expand to φ raised to the negative strong-field rung.
Claim. The PTA correction equals the S-star correction: both equal $\varphi^{-s}$, where $s$ is the strong-field rung ($s = 44$).
background
This module assigns each QG falsifier channel a φ-power from the rung address of its observable. The recognition substrate maps a length $L$ to $r(L) = \log_\varphi(L/\ell_{\mathrm{sub}})$, and the correction at rung $r$ scales as $\varphi^{-r}$ relative to the Planck-scale value.
For astrophysical black holes the half-area (strong-field) rung is $s = 44$: the horizon cell count is $\varphi^{2s}$ in the φ-ladder, and half the horizon information is processed at $s = 44$. That is the same rung appearing in the baryon asymmetry $\eta_B = \varphi^{-44}$.
PTA correction is the stochastic GW strain at that injection rung; S-star correction is the periapsis timing residual at the same rung. Both are defined as $\varphi^{-s}$ with $s$ the strong-field rung.
proof idea
One-line term proof by rfl. Both sides are definitionally phi ^ (-strongFieldRung), so Lean closes the equality by reduction with no lemmas or rewriting.
why it matters
In the D5 channel table, PTA and S-star are the two entries whose predicted correction is exactly $\varphi^{-44}$ (EHT is $2\cdot\varphi^{-44}$, Cassini $3\cdot\varphi^{-44}$, ringdown $\varphi^{-1}$). This theorem records that shared base formally, so later comparisons need not re-expand the two defs.
The shared rung is structural, not accidental: the same half-area address $s = 44$ that sets the baryon asymmetry also sets the strong-field GW injection scale. No downstream consumer is wired yet; the result is a local identity inside the channel-rung derivation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.