echo_target_pos
plain-language theorem explainer
The black-hole echo dataset row carries a strictly positive RS target scale: the dimensionless post-merger echo amplitude ratio 0.618 (≈1/φ). Anyone wiring the GWTC-3 echo falsifier into the register certificate or the ringdown status lemma cites this positivity fact. The proof is a pure unfold of the attachment record followed by numerical normalization.
Claim. The echo phenomenology dataset attachment has strictly positive RS target scale: $0 < 0.618$, where $0.618$ is the RS target dimensionless echo amplitude ratio (approximately $1/\varphi$).
background
This module attaches named observational channels, sensitivity numbers, and RS target scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachment is bookkeeping for falsifiability: a named dataset, a sensitivity scale, an RS target, and a flag for whether current data already reach that target. No row claims empirical confirmation of RS.
A dataset attachment is a record with sector, dataset name, units, sensitivity, and rsTargetScale. The predicate for a positive target is simply $0 < D.\mathrm{rsTargetScale}$. The echo row records LIGO/Virgo/KAGRA GWTC-3 tests of GR (ringdown / post-merger echo search), units "echo amplitude ratio", sensitivity $0.10$, and RS target $0.618$. The module doc notes GWTC-3 reports no post-merger echoes in analyzed events; the RS damping target is the dimensionless amplitude ratio $1/\varphi \approx 0.618$.
proof idea
Term-mode proof by unfolding. Expand the positive-target predicate to $0 < D.\mathrm{rsTargetScale}$, then expand the echo attachment so the target field is the concrete literal $0.618$. Close with norm_num, which discharges $0 < 0.618$ by numerical evaluation. No external lemmas are required beyond the two local definitions.
why it matters
This lemma is one half of the echo-row positivity package. Downstream, gwtc3_echo_dataset_positive packages it with the matching sensitivity positivity fact as a conjunction used by the GWTC-3 ringdown status module. The same fact is wired into falsifierDatasetRegisterCert, the structural certificate that every register row has positive sensitivity and positive RS target.
In the broader RS picture the target $1/\varphi$ is the Berry-scale / golden-ratio amplitude ratio that appears throughout the forcing chain (φ forced at T6; related thresholds such as the Berry creation scale $φ^{-1}$). The register does not claim echoes have been seen; it only pins the numerical RS prediction against the GWTC-3 null search so the prediction is auditable and falsifiable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.