The constructed Int is initial among Z-structures

Identifier: F:int-characterization-initial
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

A `Z-structure` is a carrier R with a point e and two endomorphisms up, down that are mutually inverse (down(up x) = x and up(down x) = x for every x) -- a pointed set with an automorphism, and NOTHING else: no generation, no aperiodicity, no order. Under only those two inverse laws, there is a map f : Int -> R with f(0) = e, f(t+1) = up(f(t)) and f(t-1) = down(f(t)), and it is the UNIQUE such map: any g : Int -> R satisfying the same three equations agrees with f at every point. This is the universal property of Int as the initial object in the category of Z-structures. It is weaker than `Int.Characterization.categorical` (F:int-characterization-categorical), which additionally assumes the target is GENERATED by e under +-1 and APERIODIC at e, and concludes the comparison map is a bijection. The two extra hypotheses are what rule out Z/n (fails aperiodicity) and Z sqcup Z (fails generation) as counter-models to categoricity; neither is needed for mere initiality, because a Z-structure's defining axioms are exactly the two inverse laws, not those two further ones. Uniqueness is stated pointwise (`g t = f t`), not as function equality -- there is no funext in this kernel (ADR-1595) to promote the pointwise claim to one.

Formal statement

theorem Int.Characterization.initial.{u} : ((x0 : Sort (u)) -> ((x1 : x0) -> ((x2 : ((x2 : x0) -> x0)) -> ((x3 : ((x3 : x0) -> x0)) -> ((x4 : ((x4 : x0) -> Eq.{u} x0 (x3 (x2 x4)) x4)) -> ((x5 : ((x5 : x0) -> Eq.{u} x0 (x2 (x3 x5)) x5)) -> And (And (Eq.{u} x0 (Int.Characterization.iter.{u} x0 x1 x2 x3 Int.zero) x1) (And (((x6 : Int) -> Eq.{u} x0 (Int.Characterization.iter.{u} x0 x1 x2 x3 (Int.add x6 Int.one)) (x2 (Int.Characterization.iter.{u} x0 x1 x2 x3 x6)))) (((x6 : Int) -> Eq.{u} x0 (Int.Characterization.iter.{u} x0 x1 x2 x3 (Int.add x6 (Int.neg Int.one))) (x3 (Int.Characterization.iter.{u} x0 x1 x2 x3 x6)))))) (((x6 : ((x6 : Int) -> x0)) -> ((x7 : And (Eq.{u} x0 (x6 Int.zero) x1) (And (((x7 : Int) -> Eq.{u} x0 (x6 (Int.add x7 Int.one)) (x2 (x6 x7)))) (((x7 : Int) -> Eq.{u} x0 (x6 (Int.add x7 (Int.neg Int.one))) (x3 (x6 x7)))))) -> ((x8 : Int) -> Eq.{u} x0 (x6 x8) (Int.Characterization.iter.{u} x0 x1 x2 x3 x8)))))))))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

kernel-Int.Characterization.initial

Kind: kernel-term
Status: checked

Supports: Int admits a structure-preserving map out of it into any Z-structure, and that map is the unique one -- with an empty axiom footprint.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example characterization_status 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^int-universal-property[[:space:]]+Int[.]Characterization[.]initial[[:space:]]+\[\][[:space:]]')" -ge 1

Evidence notes

Anchored on both the declaration name and an empty footprint column, matching the convention of F:int-characterization-categorical's own evidence row.

int-initial-not-vacuous

Kind: kernel-term
Status: checked

Supports: The theorem is not vacuous: instantiated at (Int, 0, (+1), (-1)) with the two inverse-law hypotheses discharged by the ring laws (add_assoc, add_zero, add_neg, add_comm) -- the same construction categorical_at_int uses for the stronger theorem -- and pushed back through the trusted gate with an empty footprint.

Checker command

cargo test -q -p axeyum-lean-kernel --lib characterization::characterization_tests::initial_is_not_vacuous_it_instantiates_at_the_carrier_itself

Evidence notes

A theorem whose hypothesis list nothing satisfies is axiom-free and worthless; this closes that for the two inverse laws exactly as categorical_at_int closes it for the full four-hypothesis list of categoricity.

int-initial-uniqueness-load-bearing

Kind: exhaustive-enumeration
Status: checked

Supports: Dropping the packaged uniqueness clause's `g 0 = e` hypothesis (Weakening::IntInitialDropUniqueZero) while the proof still supplies the real equation makes the kernel REFUSE Int.Characterization.initial, at the declaration itself.

Checker command

cargo run -q -p axeyum-lean-kernel --example characterization_status 2>/dev/null; test $? -eq 0

Evidence notes

24/24 injected defects refused, one of which is this one; the checker_command re-runs the mutation control on every invocation.

int-trusted-surface-empty

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.Characterization.initial.

Checker command

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

Evidence notes

A declaration cannot depend on a trusted declaration the environment does not contain, so an empty integer surface bounds every declaration in it, including Int.Characterization.initial.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum-lean-kernel characterization::universal_property module (universal-properties lane)",
  "source": "Named and proved from the already-admitted Int.Characterization.iter_zero, iter_succ, iter_pred and rec_unique -- see docs/research/09-decisions/adr-1610-name-the-universal-properties.md for why this is a separate, weaker theorem than Int.Characterization.categorical (F:int-characterization-categorical) rather than a restatement of it."
}