leadingLogEntropyAttachment
plain-language theorem explainer
Attaches the leading-log black-hole entropy coefficient to LIGO/Virgo ringdown and future LISA/ET QNM spectroscopy as a falsifier-register row. RS target is c_RS = -log(φ)/2 ≈ -0.2406, with sensitivity 0.10 chosen to separate it from LQG's -1/2 (margin >0.25); current data are not yet sensitive. Downstream positivity lemmas and the master register certificate cite this record. Pure structure literal: field assignments only.
Claim. Define the dataset attachment for the leading-log entropy coefficient: observational channel is LIGO/Virgo ringdown plus future LISA/Einstein Telescope QNM spectroscopy; units are dimensionless coefficient; numerical sensitivity is $0.10$; RS target scale is $0.05$; and the row is marked not currently sensitive. The intended RS coefficient is $c_{\mathrm{RS}}=-\log\varphi/2\approx -0.2406$, set against LQG's $-1/2$.
background
This module builds structural attachments for every row of the quantum-gravity master-plan §7 falsifier register. Each attachment names an observational channel, a sensitivity scale, an RS target scale or band, and an honest flag for whether present data already reach that target. The point is falsifiability accounting, not empirical confirmation.
A dataset attachment is a six-field record: sector label, dataset name, units string, real sensitivity, real RS target scale, and a Boolean currently-sensitive flag. Sensitivity and target are dimensionless unless units say otherwise. Several future rows honestly set the flag false: the channel is named, but precision is not yet enough for the φ-suppressed target.
The leading-log entropy coefficient is the subleading correction to black-hole entropy probed by ringdown/QNM spectroscopy. Upstream entropy language in the foundation treats configuration entropy as total defect (zero defect = minimum entropy), which motivates reading logarithmic corrections as defect-scale observables rather than free fit parameters.
proof idea
Definitional structure literal, not a proved theorem. The six fields of the dataset-attachment record are filled by concrete string and numeral assignments: sector and dataset name the QNM channel, units are "coefficient", sensitivity is the numeral 0.10, RS target scale is 0.05, and currentlySensitive is false. No tactics, no lemmas, no computation beyond the literal.
why it matters
Closes one concrete row of the §7 falsifier register so the master certificate can demand positive sensitivity and positive RS target scale on every row. Downstream, the positivity lemmas for this attachment discharge those fields by unfolding and norm_num, and both feed the one-statement conjunction that every register row is numerically well-posed.
Framework role: the quoted target $c_{\mathrm{RS}}=-\log\varphi/2$ ties the row to the golden-ratio fixed point forced in the T5–T6 segment of the forcing chain, and the 0.10 sensitivity is chosen to separate RS from loop-quantum-gravity's $-1/2$ (margin $>0.25$). The currentlySensitive=false flag keeps the register honest: LIGO/Virgo ringdown plus future LISA/ET are the named path, not a claimed detection.
Together with sibling attachments (Hawking temperature, Page curve, echoes, QNMs, PTA, dark energy), this row makes the quantum-gravity falsifier list machine-checkable without new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.