G6 LLC submits formal capability statement to NASA Glenn Research Center for lunar infrastructure contract

Today, G6 LLC submitted a capability statement to NASA Glenn Research Center in response to the Lunar Enabling Infrastructure Accelerator (LEIA) presolicitation — Notice ID 80GRC026R0008 — targeting the in-space manufacturing technology area.

The submission introduces AXLE — Algebraic eXpression Language for Evaluation — G6 LLC's Lean 4 / Mathlib4 formal verification framework. AXLE contains 1,080 machine-verified theorems with zero axioms beyond Mathlib4, including a Gronwall contraction bound establishing basin stability with proved radius ε₀ = 1/3.

For lunar in-space manufacturing, AXLE provides what autonomous fabrication systems currently lack: formally proved threshold models for regolith-derived material processing — sintering boundaries, structural phase transitions, fabrication quality self-assessment — that operate without real-time Earth communication.

The full framework is published open-access across the Principia Orthogona series on Zenodo and SSRN, with source at github.com/TOTOGT/AXLE. Every theorem is reproducible from a clean Mathlib4 install. Every open obligation is documented by name and difficulty rating in OPEN_QUESTIONS.md.

G6 LLC is a registered small business (NAICS 541715), fiscally sponsored by the New York Foundation for the Arts, and will present five accepted works at the XII Bienal da Sociedade Brasileira de Matemática in Natal, Brazil in August 2026. The Draft BAA is expected in June. G6 LLC intends to submit a full proposal in September.

🜁

G6 LLC  ·  g6llc@proton.me  ·  +1 (646) 342-3751