No relation on the constructed complex numbers satisfies seven of the Real package's ordered-ring laws

Identifier: F:complex-admits-no-compatible-order
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every pair of relations le, lt on Complex, if le is reflexive, lt is irreflexive, le composes with lt on the left (lt_of_le_of_lt), le is additive (add_le_add), le respects Complex.Equiv on both sides (le_congr), every square is le-nonneg (sq_nonneg), and lt relates zero to one (zero_lt_one), then False. The witness is the imaginary unit: sq_nonneg I gives 0 <= I*I, Complex.I_sq rewrites that to 0 <= -1, add_le_add with le_refl 1 gives 1 <= 0, and lt_of_le_of_lt with 0 < 1 gives 1 < 1. The proof is a direct term with an empty axiom footprint -- no classical reasoning is used, and double-negation elimination does not exist in this kernel's logic prelude.

Formal statement

theorem Complex.no_compatible_order : ((x0 : ((x0 : Complex) -> ((x1 : Complex) -> Prop))) -> ((x1 : ((x1 : Complex) -> ((x2 : Complex) -> Prop))) -> ((x2 : ((x2 : Complex) -> x0 x2 x2)) -> ((x3 : ((x3 : Complex) -> Not (x1 x3 x3))) -> ((x4 : ((x4 : Complex) -> ((x5 : Complex) -> ((x6 : Complex) -> ((x7 : x0 x4 x5) -> ((x8 : x1 x5 x6) -> x1 x4 x6)))))) -> ((x5 : ((x5 : Complex) -> ((x6 : Complex) -> ((x7 : Complex) -> ((x8 : Complex) -> ((x9 : x0 x5 x6) -> ((x10 : x0 x7 x8) -> x0 (Complex.add x5 x7) (Complex.add x6 x8)))))))) -> ((x6 : ((x6 : Complex) -> ((x7 : Complex) -> ((x8 : Complex) -> ((x9 : Complex) -> ((x10 : Complex.Equiv x6 x7) -> ((x11 : Complex.Equiv x8 x9) -> ((x12 : x0 x6 x8) -> x0 x7 x9)))))))) -> ((x7 : ((x7 : Complex) -> x0 Complex.zero (Complex.mul x7 x7))) -> ((x8 : x1 Complex.zero Complex.one) -> False)))))))))

Dependencies

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

5 direct dependencies 0 direct dependents

Evidence

complex-no-order-theorem

Kind: kernel-term
Status: checked

Supports: Complex.no_compatible_order is a checked theorem -- not an axiom, not an opaque -- 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 '^Complex[.]no_compatible_order[[:space:]]+theorem[[:space:]]+-$')" -ge 1

Evidence notes

The kind column distinguishes theorem from AXIOM/OPAQUE and the third column is the footprint, so an assumed version of this statement fails the row rather than passing it.

complex-i-sq-pins-the-witness

Kind: kernel-term
Status: checked

Supports: Complex.I_sq is a checked theorem, so the refutation's witness is a real one: without it Complex.I is unconstrained and I = 0 would satisfy every other law in the module.

Checker command

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

Evidence notes

Complex.ofReal_mul cannot pin I, because I is not in the image of ofReal. This is the only declaration that constrains it.

complex-no-order-declared

Kind: kernel-term
Status: checked

Supports: Neither Complex.le nor Complex.lt is declared, checked against the environment rather than inferred from the absence of the words in a source file -- the theorem and a declared order cannot both stand.

Checker command

out=$(cargo run -q -p axeyum-lean-kernel --example complex_ring_witness 2>&1) && test "$(printf '%s\n' "$out" | grep -Ec 'order refuted = true, order declared = none')" -ge 1

Evidence notes

An omission and a refutation look identical from outside, which is the whole reason this row exists in addition to the theorem row. The example probes the environment for Complex.le and Complex.lt by name and exits non-zero if either is present; verified to fail when a Complex.le definition is added.

Provenance

{
  "date": "2026-08-18",
  "established_by": "axeyum-lean-kernel complex module (ADR-0521; agent-complex-foundation lane)",
  "source": "the standard argument that a formally real field cannot contain a square root of -1, stated over this kernel's setoid equality"
}