nx_nofloat_propose_solve_gate.nx

nx_nofloat_propose_solve_gate.nx -- PROPOSE->VERIFY rung 2 (2026-07-15): SOLVE-FORMS. Rung 1 proved the loop on completions ("6 plus 7 equals ?" -> 12/12 kernel-certified); this rung asks the model to INVERT the operation -- "what plus 3 equals 7?" -> the no-float Qwen PROPOSES the unknown x, and the LCF kernel certifies the INSTANTIATED claim ("4 plus 3 equals 7") through a full Peano derivation. Wrong x cannot certify (kernel soundness); the model's solve-rate is REPORTED as measured data (first measured run: 1/10 -- inversion is beyond the 0.5B's 3-shot ability; every wrong proposal was kernel-CAUGHT). Teeth stay model-IQ-independent: T1 mechanism live: >=8/10 proposals parse as integers; zero generation or kernel failures T2 soundness cross-check: kernel verdict on the instantiation == independent in-gate arithmetic (0 violations) T3 NEG-CONTROL: all 10 wrong-by-one instantiations (kept IN-GRAMMAR: x+1, stepping to x-1 at the operand caps plus<=12/times<=6 -- first run taught that x+1 can land UNSUPPORTED instead of REFUTED) REFUTED T4 NEG-CONTROL unsolvable honesty: kernel solve-form 'what times 4 equals 13' -> NO-SOLUTION; its nearest instantiations REFUTED; and the LIVE model asked '2 times what equals 9?' can NEVER certify (2x=9 has no integer solution -- whatever the model proposes, the kernel must catch it) T5 determinism: re-running Q1 reproduces BYTE-IDENTICAL text (greedy no-float exceed) 2026-07-15 consolidation: templating/generation/parse/claim now ride nx_propose_verify_lib (single source of truth shared with the organ nx_propose_verify + the completion probe) -- prompts byte-identical, so the measured numbers must reproduce (that reproduction = the migration proof). Requires /home/elderwesto/nx_stage/nx_real_model.gguf. Heavy: ~2-4 min. Return from main (pool reap), never sys_exit. No hw writes (Rule 26). expect_exit: 0 license_tier: ORIGINAL