Chapter 73: The TauLib Linearity Audit

The Diagonal–Linear Correspondence (the relevant chapter, I.T37) identified a structural isomorphism between K5’s diagonal discipline and the !-free fragment of linear logic. That correspondence operates at the level of design principles. This chapter descends to the level of code. TauLib — the Lean 4 formalization of Book I — consists of 77 modules comprising approximately 15,900 lines. The Linearity Census Theorem (the relevant theorem, I.T38) reports the empirical finding: 74 of 77 modules use zero classical axioms. The remaining 3 sites — 2 uses of Classical.em in Coordinates/Primes.lean and 1 funext tactic call in Holomorphy/SpectralCoefficients.lean — are analyzed individually. The Classical.em sites are eliminable via decidable instances (Proposition [prop:em-eliminable], I.P38). The funext is a Lean kernel axiom used tactically, not a classical commitment. The chapter concludes with an honest Gap Declaration (Remark [rem:gap-declaration], I.R17): what remains unearned, and how Book III’s self-enrichment program will address it.