Below its own base, a number has floor logarithm zero

`build_nat_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so producing this row at all is a machine-checked proof. The first theorem about `Nat.log` that carries a HYPOTHESIS, and the one that fixed the shape of the definition. `Nat.logAux`'s guard is two nested `Nat.ble` cuts, and the two cuts commute semantically but not for proof cost: only the OUTERMOST cut collapses the whole term with a single rewrite. `n < b` refutes `b <= n`, so that cut was put outermost and this proof is one `Eq.rec` over `Nat.ble_eq_false_of_lt`; with the cuts the other way round it would have needed a second case analysis on `2 <= b` as well. Nothing was given up for it -- `ble zero y` reduces to `Bool.true` unconditionally, so the outer cut never blocks the base-0 and base-1 equations, which stay pure `refl`. The induction on `n` carries the hypothesis in its motive (`fun m => Lt m b -> Eq (log b m) 0`) because `n` is both the fuel and the argument; the induction hypothesis is never used. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Ec` consumes the pipe and the count is tested, so the exit status depends on what the run found.

A theorem with a hypothesis can be admitted with a type nothing can discharge, so this is the check that matters for this row: the test builds a `Lt 3 5` witness BY HAND out of `Nat.zero_le` and four `Nat.le_succ_succ` steps, confirms by `Kernel::infer` that it really is a `Lt 3 5`, applies `Nat.log_of_lt` to it, and checks the inferred conclusion against `Eq (log 5 3) 0`. The negative control is `log 2 8`, where the hypothesis does NOT hold and the value is 3, so the conclusion cannot be true of every argument pair.

`nat_axiom_inventory --require-axiom-free nat` enumerates the built Nat environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration. This matters more than usual here: Mathlib's `Nat.log` is defined by WELL-FOUNDED recursion on `n / b`, and the Lean equation compiler's route to that carries `Quot.sound`/`propext`. The fuel-based structural definition in `nat_prelude/log.rs` was chosen so that this row stays empty, and this command is what makes the claim falsifiable rather than asserted.