The complex numbers are constructible in this kernel at zero trusted declarations, as a pair setoid over the constructed reals

Identifier: F:complex-ring-constructed-axiom-free
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let Complex be the one-constructor inductive with two CReal fields -- CReal being the Bishop setoid of regular rational sequences, itself constructed and axiom-free -- and let Complex.Equiv z w be the DEFINED relation CReal.Equiv (re z) (re w) AND CReal.Equiv (im z) (im w). Then the nine equality-only laws of the Real package -- add_comm, add_assoc, add_zero, add_neg, mul_comm, mul_assoc, mul_one, mul_zero, left_distrib -- all hold over Complex in Equiv form, each by a theorem whose axiom footprint is empty, and the whole environment carrying them has a trusted surface (Axiom + Opaque + Quotient) of zero. No quotient is taken at either level, so Quot.sound is not needed; no funext and no propext are needed either. Eq Complex is NOT the equality of complex numbers; Complex.Equiv is, and every law that mentions equality says so in its own statement.

Formal statement

Complex : Type, Complex.mk : CReal -> CReal -> Complex, Complex.Equiv : Complex -> Complex -> Prop := fun z w => And (CReal.Equiv (Complex.re z) (Complex.re w)) (CReal.Equiv (Complex.im z) (Complex.im w)); and for each L in {add_comm, add_assoc, add_zero, add_neg, mul_comm, mul_assoc, mul_one, mul_zero, left_distrib}, Complex.L is a checked Theorem with Kernel::axiom_footprint = [].

Dependencies

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

15 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

complex-mul-assoc-footprint

Kind: kernel-term
Status: checked

Supports: Associativity of complex multiplication -- the law whose two sides are the same eight monomials in different orders, and the one that pays for the ring calculus on its own -- is a checked theorem with an empty axiom footprint.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example complex_ring_witness 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^law[[:space:]]+Complex[.]mul_assoc[[:space:]]+\[\]$')" -ge 1

Evidence notes

Anchored on the law name AND the empty-footprint column, so a rename or a witness that grew a dependency on a trusted declaration both fail. The `law` rows go to stdout; the summary goes to stderr, which is why this row and the population row below capture different streams.

complex-left-distrib-footprint

Kind: kernel-term
Status: checked

Supports: Distributivity -- the law that ties the additive and multiplicative structures together, so the pair of rows cannot both pass on additive-only work.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example complex_ring_witness 2>/dev/null) && test "$(printf '%s\n' "$out" | grep -Ec '^law[[:space:]]+Complex[.]left_distrib[[:space:]]+\[\]$')" -ge 1

Evidence notes

Second law, from the interaction of the two operations rather than from either alone.

complex-ring-population

Kind: kernel-term
Status: checked

Supports: All nine laws hold, every named declaration is checked with an empty footprint, the whole environment's trusted surface is zero, and the carrier is inhabited and Equiv-discriminating on BOTH components -- the example exits non-zero otherwise.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example complex_ring_witness 2>&1) && test "$(printf '%s\n' "$out" | grep -Ec '9/9 ring laws have an EMPTY axiom footprint')" -ge 1

Evidence notes

Captures BOTH streams: the per-declaration and per-law rows go to stdout and the summary to stderr, so the obvious `2>/dev/null` form silently matches nothing and passes for the wrong reason -- the same trap the creal population row records. The nine come from ComplexPrelude::ring_laws read out of the kernel, so dropping or duplicating a law flips the exit status instead of shrinking a count.

complex-trusted-surface-zero

Kind: kernel-term
Status: checked

Supports: The environment carrying Complex, CReal, Rat, Int and Nat together has a trusted surface of zero -- Axiom AND Opaque AND Quotient, not Axiom alone.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example complex_ring_witness 2>&1) && test "$(printf '%s\n' "$out" | grep -Ec 'trusted surface = 0 \(empty\)')" -ge 1

Evidence notes

Opaque has no proof body and Quotient admits Quot.sound, so an Axiom-only count can read zero while trusted declarations are present. This anchors on the count the example computes over all three kinds.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel complex module (ADR-0521; agent-complex-foundation lane)",
  "source": "hand-built as a pair carrier over the CReal setoid of ADR-0512"
}