The floor logarithm of n never exceeds n

Identifier: F:nat-log-le-self
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all b and n, log_b(n) <= n.

Formal statement

theorem Nat.log_le_self : ((x0 : AxNat) -> ((x1 : AxNat) -> AxNat.le (AxNat.log x0 x1) x1))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-Nat.log_le_self

Kind: kernel-term
Status: checked

Supports: For all b and n, log_b(n) <= n.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- log_le_self 2>/dev/null | grep -Ec '^Nat\.log_le_self[[:space:]]')" -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 this row at all is a machine-checked proof. The proof is `Nat.logAux_le_fuel` (a separate fact, `F:nat-logaux-le-fuel`) applied at `f := n`: since `Nat.log b n := Nat.logAux b n n` DEFINITIONALLY, `logAux_le_fuel b n n : Le (logAux b n n) n` is already `Le (log b n) n` up to delta-unfolding `log`, so no further construction is needed beyond the one application. `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.

instantiation-Nat.log_le_self

Kind: kernel-term
Status: checked

Supports: the bound is the promised statement and is strict, not vacuously reflexive, at a nontrivial argument

Checker command

cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::log_aux_le_fuel_and_log_le_self_apply_at_a_concrete_instance

Evidence notes

Applies `Nat.log_le_self` at `(b, n) = (2, 8)` and confirms the inferred conclusion is `Le (log 2 8) 8` exactly. `log 2 8` separately reduces to `3` by `Kernel::def_eq`, so this is a STRICT bound (3 < 8), not a vacuous reflexive instance of `Le`.

footprint-Nat.log_le_self

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

`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. `log_le_self`'s proof is a single application of `Nat.logAux_le_fuel`, itself axiom-free, so this row stays empty.

Provenance

{
  "date": "2026-08-28",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane nat-log-tier",
  "source": "declared by `declare_log_all` (`crates/axeyum-lean-kernel/src/nat_prelude/log.rs`), the diagonal specialization of `Nat.logAux_le_fuel`"
}