IO-OI: Components for a de Sitter Completion (restricted timestamp deposit)

Abstract

RESTRICTED — timestamp deposit. Not released for circulation. IO-OI is an inventory of components offered for evaluation on the de Sitter side of the entanglement-first-law programme. It is explicitly not a paper seeking endorsement, and no co-authorship or review by any other party is claimed or implied. Contents: (i) a machine-checked proof of the so(n) quadratic Casimir eigenvalue in the defining representation, derived from the matrix generators rather than from a definition of the answer (Lean 4.33.0-rc2, 0 sorry, standard three axioms, vacuity-audited WEAK 0, replacing a prior file that audited WEAK 5/5 and was withdrawn); (ii) a SPARC test of a_0 = cH_0/2pi with per-galaxy M/L marginalisation, in which the positive result is small (0.34 points on ~20% RMS, t = +5.90) and the negative result is firm -- a_0 = 2cH_0, the value the Deser-Levin/Milgrom vacuum route derives, is excluded by roughly an order of magnitude under every statistic; (iii) a problem statement on the missing 4pi^2, locating the candidate mechanism in the established AdS first law, where the Euclidean periodicity (2pi) and the horizon area normalisation (4) multiply to give 8piG rather than cancelling. Epistemic tagging is explicit throughout: [thm] machine-checked, [emp] empirical with stated residual, [conj] conjecture, [open] named gap. Prior claims of 'zero free parameters' and of 'fully machine-checked' status are withdrawn; a parameter-accounting budget replaces the former. AI systems assisted drafting, symbolic checking, and formal verification under the author's direction. They are not authors, are not co-signatories, and performed no peer review. No AI-generated verdict appears as evidence.