Boolean conjunction is commutative

Identifier: F:bool-and-comm
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

Recorded description

For all Booleans x and y, x && y equals y && x.

Formal statement

((x : Bool) -> ((y : Bool) -> Eq.{1} Bool (Bool.and x y) (Bool.and y x)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

import-Bool.and_comm

Kind: kernel-term
Status: checked

Supports: `Bool.and_comm`'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:bool-and-comm|')" -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 48 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 `((x : Bool) -> ((y : Bool) -> Eq.{1} Bool (Bool.and x y) (Bool.and y x)))`. `formal.statement` is that string verbatim.

footprint-Bool.and_comm

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: the imported proof term reaches no Lean axiom, opaque or quotient declaration

Checker command

scripts/check-imported-fact-lean-axioms.sh Bool.and_comm

Evidence notes

Two kernels, independently. `Kernel::axiom_footprint` walks this declaration's transitive dependencies in the IMPORTED environment and reports an empty footprint; a real Lean 4.30.0 binary's `#print axioms Bool.and_comm` reports no axioms. 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/bool-and-comm.ndjson, declaration `Bool.and_comm` from Lean 4.30.0 `Init`",
  "prior_art": [
    {
      "who": "the Lean 4 developers (leanprover/lean4)",
      "what": "`Bool.and_comm` 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."
    }
  ]
}