Module int_inductive 

Int as a real inductive — Lean’s ofNat | negSucc with its arithmetic defined rather than assumed (Init/Data/Int/Basic.lean:40-45, :78-166). The construction, packaged so the prelude adopts it in one call; the module header carries how Lean keeps it fast anyway. Int as a REAL INDUCTIVE — Lean’s ofNat | negSucc, with its arithmetic DEFINED.

The standard prelude represents integers with checked constructors and definitions. Ring and order facts still need separate proof terms; installing a carrier does not turn an assumed law into a theorem. It is a block Lean does not pay: Init/Data/Int/Basic.lean:40–45 declares

inductive Int : Type where
  | ofNat   : Nat → Int
  | negSucc : Nat → Int

and then DEFINES negOfNat, neg, subNatNat, add, mul and sub by matching on those two constructors (Init/Data/Int/Basic.lean:78–166). Every arithmetic identity Lean states about Int is a theorem over that definition.

How Lean keeps it fast anyway

The obvious objection to constructors is cost: ofNat n looks like a unary Peano spine, so 2 + 3 looks linear and 2 * 3 quadratic. Lean’s answer — read off its own source rather than guessed — is that Int’s arithmetic BOTTOMS OUT IN Nat’s. Look at the ofNat/ofNat arm of Int.add: it is ofNat (m + n), ONE Nat addition, and Nat literals are GMP-accelerated in Lean’s kernel. The @[extern "lean_int_add"] attribute on the same definition (Init/Data/Int/Basic.lean:126) is the COMPILER’s story, not the kernel’s: Int.ofNat itself carries @[extern "lean_nat_to_int"] (line 47) so a runtime Int is never a spine either.

LOGOS keeps compact arbitrary-precision literals and canonical constructor bridges. Public addition and multiplication have checked definition bodies. Their literal accelerations attest the complete program dependency chain and preserve each kernel’s independent arithmetic implementation. Rebinding any dependency disables the shortcut.

What this module is for

The standard prelude calls this module to install checked constructors and arithmetic. Constructors pass positivity/universe checks; arithmetic remains ordinary definitions visible to both kernels. The literal bridge below activates only for the canonical declaration signatures. The standard prelude also installs the public add/mul aliases. Other primitive operations and the ring/order axioms remain separately auditable until their derived replacements are installed.

Functions

canonical_int

The canonical Int term for a machine integer, in Lean’s representation: ofNat n for n ≥ 0, negSucc (-n-1) below. The Nat argument is a Literal::Nat, not a Succ spine, so a large integer costs one node — which is the whole point of the Nat literal bridge.

register_inductive_int

The whole adoption, as one call: Int gains Lean’s two constructors and Lean’s arithmetic.

register_int_arithmetic

register_int_constructors

Int’s two constructors, through the CHECKED door.

register_nat_arithmetic

supports_integer_polynomial_operations

Whether the public add/mul/sub vocabulary has the standard integer meaning.