8 papers
Optimal Finite Interval Discrepancy via Binary Refinement
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
DeLeo, Henderschedt, and Wells introduced a finite-horizon version of the classical de Bruijn--Erdos interval discrepancy problem. Starting from the unit interval, one repeatedly s…
Multiplier obstructions for Legendre pairs of length 333
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
A Legendre pair of length 333 would yield a Hadamard matrix of order 668, the smallest order presently unresolved by the Hadamard conjecture. We study the structured case in which…
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
ErdÅs Problem 30 asks for sharp asymptotics of the Sidon extremal function , and Singer's construction is the classical source of lower-bound examples matching the main term…
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…