This is the fourth paper in the Tier-1 foundation-extension series of the Horizon-Quantized Informational Vacuum (HQIV) programme. On the discrete shell temperature ladder T (m) =1/ (m+1) T (m) = 1/ (m + 1) T (m) =1/ (m+1), the HQIV library already contains machine-checked proofs (in Lean 4) of: Zeroth law as an equivalence relation on ladder temperatures First-law finite-window energy balance Second-law nonnegative entropy-production proxy on any finite undirected graph (via the combinatorial Laplacian Dirichlet form), together with a CFL-bounded explicit-Euler energy witness Third-law eventual cooling below any ε>0 > 0 ε>0 Horizon blackbody modules define finite-shell photon number density, radiation pressure P=U/3 P = U/3 P=U/3, and entropy density s= (4/3) U/T s = (4/3) U/T s= (4/3) U/T without taking the continuum limit ω/T→∞ /T ω/T→∞. A new quantitative table demonstrates recovery of Stefan–Boltzmann T4 T⁴ T4 scaling once sufficiently many shells are occupied. The macroscopic arrow of time is derived (not postulated) as the conjunction of four audited structures already present in the discrete layer: Acyclicity of the causal partial order on the null lattice Nonnegative discrete entropy production on finite heat patches Monotonic outward shell indexing toward lower temperature Forced relaxation of under-occupied early shells toward the quadratic null-shell budget via a machine-checked Lyapunov descent (lexicographic pair) that terminates at the S3 S³ S3 null reference for every deficit-only initial horizon. A new self-contained section derives the temperature ladder T (m) =1/ (m+1) T (m) = 1/ (m + 1) T (m) =1/ (m+1) and the rational curvature–monogamy split (α, γ) = (3/5, 2/5) (, ) = (3/5, 2/5) (α, γ) = (3/5, 2/5) directly from the octonionic null-lattice mode budget and stars-and-bars counting — they are outputs of the discrete axioms, not external inputs. The thermodynamic arrow certificate and discrete parallel-Poincaré hypothesis are packaged in the public Lean 4 development (build target HQIVParallelPoincare). Supplementary Python scripts reproduce the ladder values, C3 dissipation sign, Euler monotonicity, and the finite-versus-large-cutoff blackbody comparison table.
Steven Jr Ettinger (2026) studied this question.