2 papers
cs.LO2026
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
We present a sorry-free Lean 4/mathlib4 formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension, using true differential-form pullback via the Frechet der…
math.CO2026
Pair-Trace Absorption Certificates for Regular Induced Subgraphs
Arthur F. Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz
We study a fixed-core absorption problem for regular induced subgraphs. A set is q-modular if all induced degrees are congruent modulo q. Given a q-modular witness A and a retained…