pith. machine review for the scientific record. sign in
theorem proved term proof high

logicNat_NNO_uniqueness

show as:
view Lean formalization →

The uniqueness theorem for recursive functions out of LogicNat asserts that any two maps from the logic-forced naturals to an arbitrary type that preserve a chosen base element and commute with the successor operation must be identical. Researchers deriving arithmetic from logic or verifying categorical natural-numbers objects would cite this when confirming that LogicNat satisfies the full NNO universal property. The proof is a direct one-line application of the upstream uniqueness theorem already proved in the categorical setting.

claimLet $N$ be the inductive type with constructors $0$ and $succ$. For any type $A$, base element $b:A$, map $s:A→A$, and functions $f,g:N→A$ such that $f(0)=b$, $f(succ(n))=s(f(n))$ for all $n$, and likewise for $g$, it holds that $f=g$.

background

LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator), realizing the smallest subset of the positive reals closed under multiplication by the generator and containing 1. The successor operation is defined simply as the step constructor. This module serves as the Mathlib-facing bridge that re-exports the NNO universal property already established in the strict categorical setting. The principal upstream result is the theorem nno_universal_uniqueness, whose doc-comment states it supplies the uniqueness half of the NNO universal property on LogicNat in the Type category.

proof idea

The proof is a one-line wrapper that applies the upstream theorem nno_universal_uniqueness from CategoricalMathlib.

why it matters in Recognition Science

This result supplies the uniqueness half of the Mathlib NNO certificate, feeding directly into the downstream theorem mathlibNNOCert_holds that assembles the full MathlibNNOCert record. It thereby confirms that the logic-forced naturals satisfy the universal property required for arithmetic derived from logic, aligning with the forcing-chain construction of natural numbers as the orbit under the generator. No open scaffolding remains at this step.

scope and limits

Lean usage

theorem mathlibNNOCert_holds : MathlibNNOCert := { exists_rec := logicNat_has_type_NNO_universal_property, unique_rec := logicNat_NNO_uniqueness }

formal statement (Lean)

  27theorem logicNat_NNO_uniqueness :
  28    ∀ {α : Type*} (base : α) (step : α → α)
  29      (f g : LogicNat → α),
  30      f LogicNat.zero = base → (∀ n, f (LogicNat.succ n) = step (f n)) →
  31      g LogicNat.zero = base → (∀ n, g (LogicNat.succ n) = step (g n)) →
  32      f = g :=

proof body

Term-mode proof.

  33  @nno_universal_uniqueness
  34

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.