Research & formalization
Notes and preprints on graphs, geometry, and numerical methods. Each paper includes its manuscript, citation, and a precise account of its Lean formalization.
These preprints disclose the use of AI-assisted research and proof-development tools. Each paper page includes its research-process disclosure and the precise scope, assumptions, and exclusions of its Lean formalization.
Determines exact corner-constrained sensor budgets for fault-tolerant grid sensing and bounds hypercube equidistant dimension within one.
formalized with stated exclusions
Records a reproducible 345-window census at 65,536 points and states the boundary between checked predicates and digital-net interpretation.
partial
Classifies the four exceptions to full zombie damage in bridgeless cubic graphs and proves a uniform survivor-move bound.
main result formalized
Characterizes exactly when distance histograms recover populations on grids, with optimal sensor counts and a four-parameter ambiguity description.
main result formalized
Proves the even-order net property for all even m ≥ 4 and analyzes the construction’s minimum distance.
formalized with stated exclusions
Builds an explicit graph outside the two-word uniform representation class using a general neighborhood-trace bound.
formalized with stated exclusions
Derives exact spectra of released cubic subdivision matrices and identifies the dominant and subdominant eigenvalue structure.
partial
Constructs three resolving landmarks for an infinite family of cylindrical graphs and supplies an exact finite census.
partial
Shows when a minor exclusion is redundant for topological-ball tetrahedral meshes, with explicit structural hypotheses.
partial
Gives a concrete 16-vertex obstruction to recovering every prescribed Hamiltonian cycle through the published book-embedding algorithm.
partial
Constructs an infinite dense family of flag-complex extremizers without a complete bipartite spanning subgraph.
formalized with stated exclusions
Uses exact spectral certificates to study a period-eight signing and classify short-period minimizers.
formalized with stated exclusions
Enumerates fixed-endpoint vertex-regular paths using an exact prefix-completion oracle, with polynomial delay and a 2-CNF application.
formalized with stated exclusions