Formal-evidence review
- Coverage
- 1 exact subject binding
- Reviewer
- OpenAI Codex / GPT-5
- Independence
- Independence not asserted
Lean evidence record
12-Vertex Hamilton Counterexample: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Lean buildpassed
Unfinished proof stepsNone
Publication reviewsAccepted
Exact recorded Lean statement
The declaration this evidence supports
theorem flippedC4Blowup_counterexample :
CounterexampleStatement candidateTournamentLine counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
flippedC4Blowup_counterexample- Source commit
52ae1c0b7cff
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.jackson.flipped-c4-blowup-counterexample.lean-package.v001- Accepted-result title
- Accepted Result: A Twelve-Vertex Regular Bipartite Tournament Without a Hamilton Decomposition
- Accepted-result status
- Accepted counterexample
- Accepted-result boundary
- The explicitly encoded twelve-vertex orientation of K6,6 is a bipartite tournament, has indegree and outdegree three at every vertex, and has no Hamilton decomposition. Non-claim: This packet is intake metadata, not proof evidence. Non-claim: The flipped-C4 construction and opposite-pair observation are not claimed as new. Non-claim: Historical novelty of the class-size-three obstruction remains under specialist review. Non-claim: No first, resolves, or priority claim is made. Non-claim: Granet's sufficiently-large theorem is unaffected. Non-claim: Computational minimum order is independent corroboration and is not Lean-verified. Non-claim: The independent finite verifier and preserved second AI review are not theorem evidence or specialist review. Non-claim: No reusable source license or public source route is inferred from publication authorization.
- Declarations covered by recorded evidence
JacksonHamiltonDecomposition.flippedC4Blowup_counterexample- Lean build
- passed
- Recorded build time
- 134.5 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.29.1- Recorded source commit
52ae1c0b7cffe499aa0427ea08bed6e85eff6df3- Source SHA-256
sha256:0d8b1274eb8ff1581e77b1bb6d905243e3d29d5af714fa14fa76fb7ca046982e- Statement alignment
- accepted
Lean foundations
Standard foundations used by the proof
Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.
Classical.choiceQuot.soundpropext
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review detailsCredit for this release
Contributors and roles
Authorship and other contributions are recorded separately for this version.
Contributions
- Upstream attributionBertille Granet
Bertille Granet is credited for the prior flipped-C4 construction, opposite-pair structure, unrestricted formulation, and sufficiently-large theorem.
- Problem framing
- Proof strategy
- Direct contributionLech Mazur
Lech Mazur contributed the explicit class-size-three obstruction, matching-parity proof, and checked Lean formalization.
- Counterexample
- Formalization
- Proof strategy
- Source maintenance
Selected reviews
Review record
Each entry names the review question, exact subject coverage, and reviewer provenance recorded for this release. A selected review concerns only its named question and is not by itself proof or acceptance of a broader claim. These bindings alone do not establish that proof or computation checks were rerun.
Download exact review bindings
Public-wording review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Result-boundary review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Statement-alignment review
- Coverage
- 1 exact subject binding
- Reviewer
- Claude Fable 5
- Independence
- Independence not asserted
Citation
Cite this release
Use the version-specific citation so the authorship, scope, and public record remain attached.
Release history
Versions and public record
- Release
- Counterexample release
- Version
- v001
- Published
- Canonical page
- Open canonical page
Release chronology
This version is part of the release history. No independent external timestamp is claimed.
Scope of this release
- Computational minimum order is corroborating evidence and is not Lean-verified.
- Granet's sufficiently-large theorem is unaffected.
- Historical novelty of the class-size-three obstruction remains under specialist review.
- No independent external priority anchor is recorded.
- The flipped-C4 construction and opposite-pair structure are upstream work due to Bertille Granet.