TY - RPRT TI - Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0 AU - David B. Hulak AU - Arthur F. Ramos AU - Ruy J. G. B. de Queiroz PY - 2026 UR - https://arxiv.org/abs/2605.01028 ID - 2605.01028 ER -