Headlines: the curated consumer facade (G8)

Category: Special (facade — the reconstruction's actual API in one import).

import CsdLean4.Headlines gives a reviewer or downstream consumer exactly the modules carrying the corpus's 51 headline claims — the rows of specs/validation-claims.tsv (canonical; human view specs/VALIDATION-LEDGER.md) — without pulling the full 400+-module implementation surface through a single flat root. Created 2026-08-06 (BACKLOG G8, the adopted half of the 2026-08-06 external review's facade recommendation); extended 2026-08-13 (Q17 census): CL-032…CL-051, admitted under the criteria in VALIDATION-LEDGER.md — the necessity audit's named strongest-direction omissions, the 2026-08-12/13 tranche's starred headliners, and the Q18 conversions. The exhaustive root CsdLean4 remains available for whole-corpus consumers; Tests/AxiomAudit.lean remains the axiom gate.

The example := @… block at the bottom is the drift guard: it elaborates every ledger constant by its full name, so a rename, namespace move, or deletion of any headline breaks this module's build (stronger than scripts/check-validation-ledger.sh's per-file leaf grep — on creation day this guard immediately caught FOUR wrong ledger constants: three rows recording CSD.SigmaLayer.* for theorems living in CSD.RecordLayer.*, and CL-001's missing OnticSetup.TrialModel prefix; all fixed in the tsv same day). check-validation-ledger.sh also enforces that every ledger module is imported above, so the facade cannot silently drop a headline.

The 31 headline claims, by layer

• LF1 — typicality → frequencies: CSD.LF1.OnticSetup.TrialModel.main_theorem_ae (CL-001), CSD.LF1.freq_tendsto_of_iid (CL-002).
• LF2 — operational stratum: CSD.LF2.OperationalPackage.fromPreparation (CL-003), CSD.LF2.PurePreparation.born_rank_one_direct (CL-004), CSD.LF2.OperationalPackage.effect_gleason_representation (CL-005 — Busch's effect-Gleason, proved), CSD.LF2.weights_sum_eq_one (CL-006), CSD.LF2.QuantumChannel.cptp_capstone (CL-007).
• LF3 — the singlet chain: CSD.LF3.LF3_main_theorem (CL-008), CSD.LF3.LF3_singlet_frequency_convergence_born (CL-009).
• LF4 — Born from Kähler volume: CSD.LF4.fs_volume_eq_dirichlet (CL-010), CSD.RecordLayer.globalRecordClosure_born (CL-011, replacing CSD.LF4.born_frequency_convergence_N 2026-08-24 -- preparation-indexing removed), CSD.LF4.fubiniStudy_forced_by_symmetry (CL-012), CSD.LF4.obsFlow_not_ergodic (CL-013), CSD.LF4.projectedFlow_eq_unitary_family (CL-014), CSD.LF4.projectedFlow_phase_lift (CL-015), CSD.LF4.manyToOneSetup_born_frequency (CL-016).
• LF5 — measurement dynamics: CSD.LF5.measurementFlow_realises_dilation (CL-017), CSD.LF5.measurement_flow_born_frequency (CL-018).
• LF6 — entanglement / open systems: CSD.LF6.decoherence_offdiagonal_vanish (CL-019), CSD.LF6.no_product_partition_realises_singlet (CL-020), CSD.LF6.no_product_partition_realises_ghz (CL-021).
• C1 shared-domain obstruction: CSD.LF6.no_compatible_global_chsh_assignment_realises_singlet (CL-031 — no measurable shared-context outcome family compatible with any global CHSH assignment reproduces the singlet at the four CHSH settings; added 2026-08-10, replacing the false type-separation claim, see specs/publication-errata.md) and CSD.LF6.c1_singlet_contextual_capstone (CL-052, added 2026-08-13, Q19 — the positive half: an explicit measurable shared-context family on (KSigma 4, kMuPsi) reproduces the singlet, the full P_st table at every context, and no global CHSH assignment is compatible with it — the C1 separation two-sided, existence and obstruction in one statement).
• Mathlib-staged (CSD-free): QuantumInfo.vonNeumannEntropy_subadditive (CL-022), QuantumInfo.strong_subadditivity_of_relEntropy_monotone (CL-023 — SSA from the explicit hDPI premise, by design), Projectivization.wigner_rigidity (CL-024 — existence clause; see the module scope note).
• Record layer (Σ): CSD.RecordLayer.swap_luders_marginal (CL-025), CSD.RecordLayer.povm_selector_born (CL-026), CSD.RecordLayer.projectiveMeasurementCapstone (CL-027).
• CV / Thermo: CSD.CV.commute_of_disjointSupport (CL-028), CSD.Thermo.vonNeumannEntropy_le_pinching (CL-029), CSD.Thermo.landauer_bound (CL-030).

The 2026-08-13 census extension (Q17): CL-032 … CL-051

• Forcing / no-go tier (the necessity audit's named omissions): Matrix.StoneC1.stone_continuous (CL-032 — the second unconditional necessity), CSD.CV.no_exact_finite_ccr (CL-033), CSD.RecordLayer.no_everywhere_correlation / no_exact_collapse / collapse_accuracy_bound (CL-034/035/036 — the trilemma price list), CSD.SigmaLayer.compositeAlgReconstruction (CL-037 — tensor forcing), CSD.RecordLayer.posMeasure_noRecord_pointer (CL-038 — the third leg on the pointer).
• Record layer / measurement: CSD.LF4.qubitBorn (CL-039 — the A7-faithful context-fixed qubit Born), CSD.RecordLayer.nullSeamGenClosure (CL-047 — the third horn at every N), CSD.RecordLayer.recordKernel_eq_transProb (CL-048) and CSD.RecordLayer.measure_eq_fubiniStudy_of_record_statistics_invariant (CL-049) — the Q18 conditioner conversions, CSD.RecordLayer.povm_sector_born (CL-050 — the dynamical POVM Born), CSD.RecordLayer.pointer_luders_born_prep (CL-051 — records and update on one arena).
• Chaos / records tranche: CSD.Empirical.QuantumChaos.deficitKick_record_halfLife (CL-040 — derived coupling), deficitKick_phaseFlip_halfLife (CL-041 — DH-exact rate), ledgerEntropy_le (CL-042 — the entropy ledger).
• QI / open systems / CV: CSD.Empirical.QM.QEC.shor_corrects_Z_degenerate (CL-043 — Shor-9 degeneracy as a theorem), CSD.LF6.lindbladSemigroup_hasDerivAt (CL-044 — the master equation), CSD.CV.norm_commutator_velocity_le (CL-045 — the explicit LR velocity), CSD.CV.vacuum_clustering (CL-046).

Claim-status vocabulary, scope qualifications, and the open-work queue live in specs/VALIDATION-LEDGER.md, specs/reconstruction-status.md, and specs/future-work.md / specs/BACKLOG.md; no import here upgrades a qualified claim.

Drift guard — every ledger constant, by full name (CL-001 … CL-031)

The drift guard: each example elaborates one ledger constant by its full name (universe metavariables generalized at top level; the one noncomputable data def marked as such). A rename, namespace move, or deletion of any headline fails this build.