ALL 4 ARC_Object AXIOMS extract_objects_impl · 0 sorry
[AXIOM 1] :: is_not_empty
NON-EMPTY
Runtime check. BFS returns Nonempty only when seed pixel passes non-background filter.
is_not_empty := h_ne
if h_ne : pixels.Nonempty then — Lean propagates proof
✓ PROVEN — RUNTIME
if h_ne : pixels.Nonempty then — Lean propagates proof
[AXIOM 2] :: is_monochrome — IRF-BFS-MONO-FC CLOSED
MONOCHROME
Every pixel in the object has the seed color.
BFS_MaxInv.is_mono added to Envelope Invariant.
VISIT+color branch: h_color : g q = color → h_mono_new carries forward.
SKIP/nocolor: is_mono unchanged (comp unchanged).
BFS_MaxInv.is_mono added to Envelope Invariant.
VISIT+color branch: h_color : g q = color → h_mono_new carries forward.
SKIP/nocolor: is_mono unchanged (comp unchanged).
is_monochrome := by intro p hp; exact h_max_proof.is_mono p hp
BFS_MaxInv.is_mono: ∀ p ∈ comp, g p = color — carried via BFS_Inv
✓ PROVEN — NO SORRY
BFS_MaxInv.is_mono: ∀ p ∈ comp, g p = color — carried via BFS_Inv
[AXIOM 3] :: is_connected — IRF-BFS-CONN CLOSED
CONNECTED
Any two pixels have a path inside the object.
BFS_ConnInv carries: ∀ p ∈ comp, connected4 seed p.
connected4_step: single BFS expansion extends path.
trans + symm: p1→seed→p2 = p1→p2.
BFS_ConnInv carries: ∀ p ∈ comp, connected4 seed p.
connected4_step: single BFS expansion extends path.
trans + symm: p1→seed→p2 = p1→p2.
exact connected4_in_finset_trans pixels p1 cell p2
(connected4_in_finset_symm pixels cell p1 (h_conn_proof p1 hp1))
(h_conn_proof p2 hp2)
✓ PROVEN — NO SORRY
(connected4_in_finset_symm pixels cell p1 (h_conn_proof p1 hp1))
(h_conn_proof p2 hp2)
[AXIOM 4] :: is_maximal — IRF-BFS-MAX CLOSED
MAXIMAL — THE FINAL BOSS
No adjacent same-color pixel was excluded.
BFS_MaxInv envelope: ∀ p ∈ comp, adj q → g q = color → q ∈ comp ∨ q ∈ queue ∨ q ∈ visited.
Queue = [] → middle term vanishes. visited_color closes second case.
BFS_MaxInv envelope: ∀ p ∈ comp, adj q → g q = color → q ∈ comp ∨ q ∈ queue ∨ q ∈ visited.
Queue = [] → middle term vanishes. visited_color closes second case.
simp only [List.mem_nil_iff, false_or] at h_env
-- h_env : p_out ∈ pixels ∨ p_out ∈ final_visited
rcases h_env with h | h_vis
· exact h
· exact h_max_proof.visited_color p_out h_vis hp_color
✓ PROVEN — THE ENVELOPE COLLAPSED
-- h_env : p_out ∈ pixels ∨ p_out ∈ final_visited
rcases h_env with h | h_vis
· exact h
· exact h_max_proof.visited_color p_out h_vis hp_color
PROOF CHAIN — FULL DEPENDENCY LOG
✓ arc_cell_fintype — Fintype (ARC_Cell H W) via Fin H × Fin W
✓ unvisited_decreases — Finset.card_lt_card (termination measure)
✓ flood_fill_bfs — partial removed, termination_by wired
✓ adjacent4_cells_sound — b ∈ cells → adjacent4 a b (rcases + omega)
✓ adjacent4_cells_complete — adjacent4 a b → b ∈ cells (ext + omega)
✓ adjacent4_cells_spec — iff biconditional (IRF-BFS-ADJ CLOSED)
✓ flood_fill_bfs_monochrome — queue induction, 3 branches (IRF-BFS-MONO)
✓ connected4_in_finset_mono — S₁⊆S₂ lifts paths
✓ connected4_in_finset_trans — path concatenation (path12 ++ path23.tail)
✓ connected4_step — single BFS step extends path
✓ BFS_ConnInv — obj_conn + queue_adj carried through loop
✓ BFS_MaxInv — envelope + visited_color + is_mono carried
✓ BFS_Inv — combined invariant structure
✓ flood_fill_conn — returns Σ'(result, visited, conn_proof, max_inv)
✓ extract_objects_impl — 0 sorry in is_not_empty / monochrome / connected / maximal
⬚ IRF-ARC-DSL-003-COVER — extract_objects covers all non-bg pixels (downstream)
⬚ IRF-ARC-DSL-003-DISJOINT — objects pairwise disjoint (downstream)
⬚ IRF-ARC-DSL-TAUSELECT — foldl invariant for tau_select (unrelated)
EPOCH 3 — DSL HANDS next targets