ptaCorrectionValue
plain-language theorem explainer
Defines the PTA channel correction as φ to the minus strong-field rung, i.e. the base fractional amplitude for stochastic GW strain at the strong-field injection scale. Anyone working the nHz PTA falsifier or comparing channel prefactors cites this value. The body is a one-line φ-power at the shared strong-field address (rung 44).
Claim. The PTA correction is $\varphi^{-s}$, where $s$ is the strong-field rung (half-area horizon information rung on the $\varphi$-ladder). With $s=44$ this is $\varphi^{-44}$, the fractional scale of the stochastic GW strain at strong-field injection.
background
This module assigns each QG falsifier channel a $\varphi$-power from the rung address of its observable. A length $L$ has rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$; the recognition correction at that rung scales as $\varphi^{-r}$ relative to the Planck-scale value.
For astrophysical black holes the horizon cell count sits on the $\varphi$-ladder at a strong-field rung $s$. The half-area rung (half the horizon information processed) is $s=44$, the same address that appears in the baryon asymmetry $\eta_B=\varphi^{-44}$. PTA samples the stochastic GW strain at that injection rung, so its base correction is exactly $\varphi^{-s}$.
Sibling channel values (EHT, S-star, Cassini) are integer multiples of this same base; ringdown is the separate one-rung reflection $\varphi^{-1}$.
proof idea
Pure definition: the real is $\varphi$ raised to the integer power $-s$, with $s$ the strong-field rung constant already fixed in-module. No tactic proof; downstream positivity uses zpow_pos and phi_pos.
why it matters
Anchors the PTA row of the D5 channel table and the shared base for several equalities. Downstream, pta_sstar_same_base identifies it with the S-star periapsis residual; eht_eq_two_times_pta and cassini_eq_three_times_pta recover the geometric prefactors 2 (shadow-to-photon-ring projection) and 3 (Shapiro path integral) by rfl. ptaDerived packages it as the derived PTA prediction (rung 44, prefactor 1), and ptaCorrectionValue_pos records positivity.
Framework-wise it is the gravity-side use of the same rung-44 address as $\eta_B$, tying strong-field GW injection to the $\varphi$-ladder forced by T5–T6 (J-cost uniqueness and the self-similar fixed point). It does not reopen the forcing chain; it only places the PTA observable on that ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.