5 papers
Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
We present a mechanically checked Isabelle/HOL bridge from the Picard-Lindelof flow infrastructure in the Archive of Formal Proofs (AFP) to selected qualitative facts for the mass-…
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…
Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Token identity is semantic information for measurement-bearing expressions. Intervals, dimension tags, and token-erased syntax can say what values a measured leaf may take, but the…
Exterior-Model Spinors in Split Rank: Exact Levi Images and Square-Determinant Obstructions
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
Let be a field with , and let denote the standard hyperbolic form on . We study the exterior spinor model together with…
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…