Punta Gorda, Florida. Operations supervisor at Federal Express; founder of F-Keys Creative LLC. Everything below was built independently and is running now.
The research below reports what the data does not support alongside what it does. Negative results are published as negative results. Selected writing quotes the source of every excerpt.
Axiom provenance for Lean 4 and Metamath. Which step introduced an axiom, and whether the theorem's own statement required it. Apache-2.0, on PyPI, the MCP registry and Reservoir.
open →A standing measurement of what 14 formal libraries across six foundations rest on. Machine-readable, CC-BY-4.0. Zero theorems resting on an unfinished proof; verified, not assumed.
open →58 deposited works with DOIs: axiom provenance, dominator analysis of classical dependence, color-vision methodology, formal epistemology. Full text, no paywall.
open →Color-vision accessibility infrastructure. One engine: Machado 2009 simulation, Brettel 1997 cone projection, CIE ΔE2000 conflict detection. Shipped across eight distribution channels with no duplicated logic.
open →Ballot boxes that live inside a notification. Create a vote, share a link, embed it anywhere.
open →Turn a phone into a programmable macro surface. No app, no extra hardware, just glass.
open →