Mathlib v4.30 source proposition Int.dvd_gcd

`build_int_prelude` admits `Int.dvd_gcd_nat` 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. New proof, lane int-dvd-mirrors: `int_prelude/dvd_gcd_mirrors.rs`'s `declare_dvd_gcd_nat` -- Mathlib's actual `Int.dvd_gcd` (the Nat-typed-divisor form; the existing `p.dvd_gcd` is instead Mathlib's `Int.dvd_coe_gcd`, see F:ml430-int-dvd-coe-gcd-6bda035e). `natAbs (ofNat c) ≡ c` by `rfl`, so `nat_abs_dvd_nat_abs_of_dvd` applied to each hypothesis already produces `Nat.dvd c (natAbs a)`/`Nat.dvd c (natAbs b)` up to that defeq -- no cast bridge lemma needed. `Nat.dvd_gcd` closes it; its conclusion is defeq to the stated goal by `Int.gcd`'s own definition. Needed a mixed-binder theorem builder (`theorem_mixed`, local to the new module) since `IntDev::int_theorem` forces every binder to `Int` and this statement's divisor `c` is `Nat`-typed. `int_theorem_inventory`'s rendered type matches this fact's `formal.statement` (`∀ {a b : ℤ} {c : ℕ}, ↑c ∣ a → ↑c ∣ b → c ∣ a.gcd b`). `int_theorem_inventory` exits non-zero for a name that does not exist, and the `grep -c` count (tested `-ge 1`, not piped into `grep -q`) requires the admitted declaration to actually be printed; the anchor requires the exact name followed by whitespace, so it cannot match a longer sibling name sharing the same prefix. Verified both ways: the real name greps to a count `-ge 1`; grepping a fabricated name (`Int.dvd_gcd_nat_bogus_xyz`) makes `int_theorem_inventory` fail closed (exit 1, "no Int declaration matches").

`prelude_axiom_inventory --require-axiom-free integer` enumerates the built Int environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration (measured: integer axiom=0). A theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds every individual theorem's footprint by []. int_prelude_tests::every_int_declaration_is_checked_and_axiom_free and derived_laws_have_no_axiom_footprint (both re-run on every int_prelude:: sweep) additionally confirm this theorem's own Kernel::axiom_footprint directly.