nx_autoformalize.nx

nx_autoformalize.nx -- AUTOFORMALIZATION rungs 1-4: informal arithmetic claim -> FORMAL Peano terms -> a derivation CHECKED by the LCF-style v2 kernel. This is the computational Frontier Radar's number-one OPPORTUNITY (momentum 33, researcher-measured 2025/26: autoformalization / proof assistants) getting its first sovereign organ -- the census found the gap, this closes rungs 1-4. 2026-07-15: the af_* machinery moved VERBATIM to nx_autoformalize_lib.nx (pure lib, no main) so other organs can compose the verifier -- the propose->verify loop (nx_nofloat_propose_verify_gate: the no-float LLM proposes, this kernel disposes). This organ = the same battery over the lib; behavior unchanged and re-proven by the battery below. SCOPE (honest): "<n|what> [plus|times <n|what>] =|<|<= <n>" (digits or number-words zero..twelve). A FALSE claim ("2 + 2 = 5") formalizes but is REFUTED; out-of-grammar text -> UNSUPPORTED (honest, no guess). The frontier meaning of autoformalization is LLM->Lean at paper scale -- this is rungs 1-4 of that ladder. Modes: no-arg = gate battery (expect_exit 0); argv[1] = one informal claim -> verdict. license_tier: ORIGINAL expect_exit: 0