echoAttachment
plain-language theorem explainer
Records the black-hole echo falsifier row: LIGO/Virgo/KAGRA GWTC-3 ringdown/post-merger searches, with sensitivity 0.10 in echo amplitude ratio and RS target 1/φ ≈ 0.618, flagged not yet sensitive. Verification and GWTC-3 status certificates cite it when assembling the §7 register. The body is a plain structure literal, no proof.
Claim. The black-hole echo phenomenology attachment is the dataset record with sector "Black-hole echo phenomenology", channel LIGO/Virgo/KAGRA GWTC-3 GR ringdown / post-merger echo search, units echo amplitude ratio, numerical sensitivity $0.10$, Recognition Science target scale $0.618$ (i.e. $1/\varphi$), and current-sensitivity flag false.
background
The module attaches named observational channels and numerical scales to every row of the quantum-gravity master-plan §7 falsifier register. An attachment is a six-field record: sector label, dataset name, units string, dimensionless (unless units say otherwise) sensitivity, RS target scale or band, and a Boolean saying whether present data already reach that target. Purpose is falsifiability accounting, not confirmation; records stay deliberately conservative.
DatasetAttachment is that structure. Sibling rows cover BMV, Hawking temperature, leading-log entropy, Page curve, $\Omega_\Lambda$, dark-energy $w$, QNMs, and PTA. For echoes, the doc states GWTC-3 reports no post-merger echoes in analyzed events, while the RS damping target is the dimensionless amplitude ratio $1/\varphi\approx 0.618$ (the Berry creation threshold $\varphi^{-1}$ from the forcing chain).
Upstream edges into foundation and gravity modules are incidental name collisions in the dependency graph; the definition itself only instantiates the local structure with string and real literals.
proof idea
Not a proof: a structure-value definition. It fills the six DatasetAttachment fields by literals: sector and dataset strings naming the GWTC-3 echo channel, units "echo amplitude ratio", sensitivity = 0.10, rsTargetScale = 0.618, and currentlySensitive = false. Downstream positivity lemmas (echo_sensitivity_pos, echo_target_pos) simply unfold this def and close with norm_num.
why it matters
Closes the echo row of the §7 falsifier-register dataset layer so the master certificate can demand positive sensitivity and positive RS target on every row. Feeds echo_sensitivity_pos and echo_target_pos, which are conjoined in falsifier_dataset_register_one_statement and packed into FalsifierDatasetRegisterCert. The same pair is required by gwtc3_echo_dataset_positive and the echo_dataset_positive field of GWTC3RingdownStatusCert, tying the register to published GWTC-3 qualitative status (no post-merger echoes reported).
Framework link: the target $0.618$ is $\varphi^{-1}$, the Berry creation / echo-damping scale. The honest currentlySensitive = false keeps the register from overclaiming: GWTC-3 names the channel and rules out large echoes, but does not yet probe the $\varphi$-suppressed amplitude. No open sorry; this is structural bookkeeping for later empirical comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.