In a nutshell: Classical mathematics has no definition of space. Space in modern mathematics is Rn—the Cartesian product of real numbers. But each real number requires infinity (Dedekind cuts, Cauchy sequences, infinite decimals). Each point in Rn is zero-dimensional. Space is ∞×0—undefined algebra masquerading as foundation. We present VOID: mathematics built from finite observation where operations cost budget, infinity cannot be constructed, and every operation either terminates or returns U when budget exhausts. Core mechanism: Every operation costs µ-ticks of budget and generates heat (dissipated budget), obeying strict conservation: Binitial = Bfinal ⊕h. Mathematical content is encoded via strictly bounded naturals (Fin) and bounded rational pairs (Fin), so all values and results are constructed and computed within finite, explicitly delimited resource limits—never crossing into actual or potential infinity. Probability values and all rational outputs are always derived within these finite bounds; operations return True, False, or explicit U (undecidable) if the budget can no longer support exact distinction. Key results: (1) Exhausted operations return U, making computational limits explicit. Classical systems crash, hang, or hallucinate; VOID admits "I cannot afford this computation." (2) Quantum-like superposition emerges when classical determination exceeds available resources. (3) Information operations exhibit thermodynamic asymmetry: reading preserves budget, writing and erasure generate heat. (4) Paradoxes requiring infinite regress (Russell, Halting, Gödel) return U instead of crashing---they're defunded, not solved. (5) We construct probability, geometry, and entropy without infinite types—demonstrating that infinity is eliminable even in domains where it appears essential. Verification: 2500+ lines of Coq formalization relative to Martin-Löf type theory and are available at https://github.com/probabilistic-minds-consortium/void-mathematics-fully-finite-coq-verified (the project repository). All operations maintain conservation B= B′ ⊕h. All modules handle U explicitly. Zero axioms beyond constructive type theory.