Excluded middle for propositions, as Lean proves it

Identifier: F:prop-excluded-middle-classical
Proof route: imported-kernel-lean
External status: proved
Axiom footprint: lean4export-3.1.0-stream-faithfulness, axeyum-lean-import-wire-translation, lean4export-3.1.0-delivered-bytes-are-the-intended-export, Classical.choice, Quot, Quot.lift, Quot.mk, Quot.sound, propext

Recorded description

For every proposition p, either p holds or its negation holds.

Formal statement

((p : Prop) -> Or p (Not p))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

import-Classical.em

Kind: kernel-term
Status: checked

Supports: `Classical.em`'s Lean proof term type-checks against this statement in the independent Axeyum kernel.

Checker command

test "$(cargo test -p axeyum-lean-import --test imported_fact_evidence -- --nocapture 2>/dev/null | grep -c 'AXEYUM-IMPORT-FACT|F:prop-excluded-middle-classical|')" -ge 1

Evidence notes

The command greps for this fact's own marker line rather than trusting the exit status, so a suite that compiles to zero tests -- this repository's signature defect -- fails instead of exiting 0. Measured 2026-08-15: the stream hashes to the pin in `artifacts/lean-imports/MANIFEST.json`, the fail-closed importer admits 106 declarations (it publishes nothing unless the WHOLE stream translates and every declaration passes the trusted gate), and `Kernel::render_lean` of the admitted type is `((p : Prop) -> Or p (Not p))`. `formal.statement` is that string verbatim.

footprint-Classical.em

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: the imported proof term reaches six trusted declarations in our kernel's classification, three in Lean's

Checker command

scripts/check-imported-fact-lean-axioms.sh Classical.em

Evidence notes

Two kernels, independently. `Kernel::axiom_footprint` walks this declaration's transitive dependencies in the IMPORTED environment and reports `Classical.choice, Quot, Quot.lift, Quot.mk, Quot.sound, propext` -- six names, because our kernel counts the whole quotient package as trusted `Quotient` declarations; a real Lean 4.30.0 binary's `#print axioms Classical.em` reports `[propext, Classical.choice, Quot.sound]` -- three names. The first three entries are the assumptions the IMPORT adds and the constructed `kernel-lean` route does not make: that the exporter faithfully rendered Lean's environment, that our NDJSON-to-kernel-term translation preserves meaning, and that the delivered bytes are the producer's intended export -- format 3.1 has no footer, so completion is relative to the bytes handed over, which `axeyum-lean-import`'s own documentation states. They are why `axiom_footprint: []` is unavailable on this route and the validator rejects it (ADR-0454).

Provenance

{
  "date": "2026-08-15",
  "established_by": "axeyum-lean-import, lane formalized-collect -- our independent kernel ADMITTED Lean's proof term. This project did NOT construct the proof; see proof_route.",
  "source": "official lean4export NDJSON 3.1.0 stream artifacts/lean-imports/classical-em.ndjson, declaration `Classical.em` from Lean 4.30.0 `Init`",
  "prior_art": [
    {
      "who": "the Lean 4 developers (leanprover/lean4)",
      "what": "`Classical.em` in the Lean 4 core library (`Init`), with its proof term",
      "where": "leanprover/lean4 v4.30.0, githash d024af099ca4bf2c86f649261ebf59565dc8c622",
      "year": 2026,
      "attribution": "read directly from the pinned `lean4export` stream that this fact cites, and cross-checked against a real Lean 4.30.0 binary; this lane did not consult a paper or a secondary source."
    }
  ]
}