Two-variable AM-GM over the constructed rationals, proved by a producer-found sum-of-squares certificate

The proof term was NOT written by a person. `crate::psatz::rat::prove` parsed the goal into a polynomial, factored the difference's Gram matrix over the affine basis with an exact rational LDL^T, cleared denominators to one integer scale, emitted the `sq_nonneg`/`add_nonneg` fold, proved the certificate's identity with `ring::rat::prove_eq`, and handed the assembled term to `Kernel::add_declaration`. `rat_prelude/psatz_inequalities.rs` has NO hand-written fallback: if the producer declines, `build_rat_prelude` fails, so the presence of this theorem in the environment is itself the evidence that the search ran and succeeded. `Kernel::add_declaration` re-checks the emitted term against the stated type, so a line in this tool's output for the exact name is a machine-checked proof having been admitted. `--release` is used for speed, not necessity: this binary builds logic/nat/int/rat and no constructed prelude. `grep -c` (never `-q`) both avoids a SIGPIPE-under-pipefail false negative and independently asserts the whitespace-anchored `theorem` row is present, so a theorem demoted to an axiom would fail this check rather than pass it. A named filter matching nothing exits 1 in the tool itself, verified 2026-09-05 (`no_such_rat_theorem_xyz` -> exit 1), so a deleted theorem cannot read as a re-derived one. The separators are `[[:space:]]`, not `\t`: POSIX ERE does not interpret `\t` as a tab, so a tab-anchored pattern matches NOTHING under the GNU grep a script gets, while an interactive shell's ugrep wrapper masks it.

`rat_theorem_inventory`'s third column is `Kernel::axiom_footprint` joined by commas, so an EMPTY third column is an empty footprint; `grep -cx ''` (never `grep -q`, which lies under `pipefail`) counts the blank field and exits 1 when there is none, so a theorem that grew a footprint fails rather than reporting a smaller number. Independently, `rat_prelude_tests::every_rat_declaration_is_checked_and_axiom_free` derives its population from `Environment::iter`, not from a literal list, and asserts an empty footprint for every `Rat.`-prefixed theorem or definition; measured 2026-09-05 the whole prelude is 454 derived, 454 with an empty footprint, 0 asserted.

Six mutants, RUN twice -- before and after these theorems joined the prelude -- all six killed both times, exit 0 both times, baseline 29 tests. The two the brief named: flipping a cleared form's coefficient sign killed 5 then 12, and changing the verified-witness refusal reason killed exactly 1 both times. The two counts that MOVED are the mutants that now also break `build_rat_prelude`, which is what the no-fallback design predicts. This row pins the PRODUCER's guards, not the statement: it says the search cannot silently degrade, and says nothing about the statement being true, which the kernel-term row above is what settles.