Tacet Turns Pre-Registration Into a Typing Rule, With Lean 4 Metatheory and No Admitted Gaps

arXiv 2608.27451·medium signalXBlueskyLinkedInCopy link

Tacet is a language and type system in which an empirical analysis declares what it generated and what it expects to find, and is refused any claim it cannot afford or cannot properly test. A sample selected by reading outcomes permanently sets a purity bit and is recorded as having examined everything it read, so it can never be granted a one-sided or confirmatory price without the system asking about intent, and whether a comparison is paired or clustered is computed statically from declared functional dependencies before any data is read. Because the wealth transformer is antitone in the realized p-value, affordability is checkable before the analysis runs; the metatheory is machine-checked in Lean 4 with no admitted gaps and demonstrated on the SWE-bench Verified leaderboard and BIG-Bench Hard.