Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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-…
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…
cs.LO2026
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…