The first index law: powers add over a product

Identifier: F:nat-pow-add
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all natural numbers a, m and n, a^(m+n) = a^m * a^n.

Formal statement

theorem Nat.pow_add : ((a : AxNat) -> ((m : AxNat) -> ((n : AxNat) -> Eq.{1} AxNat (AxNat.pow a (AxNat.add m n)) (AxNat.mul (AxNat.pow a m) (AxNat.pow a n)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

4 direct dependencies 7 direct dependents

Evidence

kernel-Nat.pow_add

Kind: kernel-term
Status: checked

Supports: For all natural numbers a, m and n, a^(m+n) = a^m * a^n.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- pow_add 2>/dev/null | grep -xFc 'Nat.pow_add	3	((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.pow x0 (AxNat.add x1 x2)) (AxNat.mul (AxNat.pow x0 x1) (AxNat.pow x0 x2)))))')" -ge 1

Evidence notes

`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 the row at all is a machine-checked proof. Proved by induction on the exponent `n`: the base case is `mul_one` reversed (both `a^(m+0)` and `a^0` compute definitionally), and the step chains the induction hypothesis, `mul_assoc`, and `pow_succ` backwards. The command names its own subject twice over -- `nat_theorem_inventory` exits non-zero for a name that does not exist, and the `grep -q` requires the admitted declaration to be printed; verified 2026-08-16 that a fabricated name exits 1. TIGHTENED 2026-08-17: the command matched the NAME only, which a weakened statement survives. Lane `nat-prime-divisor` measured this concretely on its own theorem — spelling a primality bound `1 <= p` instead of `2 <= p` still type-checks, still admits, and passes every name-only checker, while being satisfied by p = 1. The kernel cannot see a weaker statement; only comparing the rendered TYPE can. This now matches the full type exactly (grep -qxF), so any change to the proposition breaks it.

footprint-Nat.pow_add

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`theorem_axiom_footprint` reports `nat Nat.pow_add 0` directly, and `nat_axiom_inventory` bounds it: the enumeration reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, and a theorem cannot depend on a trusted declaration the environment does not contain, so an empty trusted surface bounds every individual footprint by []. Counting `Declaration::Axiom` alone would NOT suffice -- `Opaque` has no proof body and `Quotient` admits `Quot.sound` -- so the enumeration covers all three.

Provenance

{
  "date": "2026-08-14",
  "established_by": "not established in this ledger",
  "source": "proposition extracted from the S:number strand of the math-education concept graph; statement authored here, nothing copied",
  "prior_art": [
    {
      "who": "classical / folklore",
      "what": "the index law a^(m+n) = a^m * a^n is an immediate induction on the exponent and appears in every elementary treatment; no single originating source is meaningful",
      "attribution": "standard textbook attribution; this lane did not consult a primary source"
    }
  ]
}