TACTICAL BURN ORDER — DEPENDENCY CHAIN strict sequence
IRF-BFS-ADJ ← ACTIVE
→
IRF-BFS-TERM full
→
IRF-BFS-MAX
→
IRF-BFS-CONN
→
DSL-003-COVER/DISJOINT
→
DSL-006 synthesis
→
ARC_Solution
ACTIVE BURN 1 item
[IRF-BFS-CONN] :: ACTIVE BURN — BURNING NOW
CONNECTIVITY INVARIANT — BFS Parent Chain
Replaces shift_cell-based generator with explicit if-based generator.
Each branch directly constructs the neighbour ARC_Cell with a Fin proof.
omega crushes the Manhattan distance arithmetic immediately.
Two sub-theorems filed:
· adjacent4_cells_sound: b ∈ cells → adjacent4 a b (forward)
· adjacent4_cells_complete: adjacent4 a b → b ∈ cells (backward)
· adjacent4_cells_spec: biconditional (iff) combining both
split_ifs / simp / omega
rcases / ext / Fin.ext_iff
Two sub-theorems filed:
· adjacent4_cells_sound: b ∈ cells → adjacent4 a b (forward)
· adjacent4_cells_complete: adjacent4 a b → b ∈ cells (backward)
· adjacent4_cells_spec: biconditional (iff) combining both
theorem adjacent4_cells_sound ...
(hb : b ∈ adjacent4_cells a) : adjacent4 a b := by
simp [adjacent4_cells, ...] at hb
rcases hb with (⟨_, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩)
<;> simp [adjacent4] <;> omega
theorem adjacent4_cells_complete ...
(hadj : adjacent4 a b) : b ∈ adjacent4_cells a := by
rcases hadj with (⟨hrow, hcol⟩ | ⟨hcol, hrow⟩)
· rcases hcol ... → RIGHT/LEFT branch
· rcases hrow ... → DOWN/UP branch
<;> ext <;> simp [Fin.ext_iff] <;> omega
(hb : b ∈ adjacent4_cells a) : adjacent4 a b := by
simp [adjacent4_cells, ...] at hb
rcases hb with (⟨_, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩)
<;> simp [adjacent4] <;> omega
theorem adjacent4_cells_complete ...
(hadj : adjacent4 a b) : b ∈ adjacent4_cells a := by
rcases hadj with (⟨hrow, hcol⟩ | ⟨hcol, hrow⟩)
· rcases hcol ... → RIGHT/LEFT branch
· rcases hrow ... → DOWN/UP branch
<;> ext <;> simp [Fin.ext_iff] <;> omega
unblocks: IRF-BFS-CONN · IRF-BFS-MAX · flood_fill_bfs correctness chain
RECENTLY CLOSED since session start
[CLOSED] :: extract_objects — THE BIG SORRY
extract_objects IMPLEMENTATION
The original `sorry` in extract_objects is gone. Delegates to extract_objects_run → extract_objects_impl → flood_fill loop.
STATUS: BURNED
[CLOSED] :: IRF-BFS-TERM
BFS TERMINATION — partial removed
termination_by: unvisited_count s + queue.length
unvisited_decreases: PROVEN via Finset.card_lt_card
SKIP branch: omega. VISIT branch: omega after h_dec.
STATUS: BURNED
unvisited_decreases: PROVEN via Finset.card_lt_card
SKIP branch: omega. VISIT branch: omega after h_dec.
[CLOSED] :: arc_cell_fintype
Fintype (ARC_Cell H W)
Equiv from Fin H × Fin W. Required for Finset.univ and the unvisited_count termination measure.
STATUS: BURNED
[CLOSED] :: IRF-BFS-MONO
is_monochrome — flood_fill_bfs_monochrome
Induction on queue across 3 branches: SKIP / VISIT+color / VISIT+nocolor.
Proven: p ∈ result → g p = color ∨ p ∈ comp (∅ seed → g p = color).
STATUS: BURNED
Proven: p ∈ result → g p = color ∨ p ∈ comp (∅ seed → g p = color).
[CLOSED] :: connected4_in_finset refl+symm
Set-local connectivity — refl + symm
connected4_in_finset_refl: singleton path. connected4_in_finset_symm: path reversal + adjacent4_symm.
STATUS: BURNED
PENDING BOSS FIGHTS 4 BFS core
[IRF-BFS-CONN] :: PENDING → unblocked by IRF-BFS-ADJ
AXIOM 3: is_connected
Must prove: ∀ p1 p2 ∈ comp, connected4_in_finset comp p1 p2.
Strategy: define BFS_tree (parent pointers from BFS expansion). Every pixel p was enqueued from some parent p' via adjacent4_cells. The BFS tree gives a path from seed to any p. Compose: seed→p1 and seed→p2 → reverse → seed→p1→p2.
BFS tree path
transitive closure
Strategy: define BFS_tree (parent pointers from BFS expansion). Every pixel p was enqueued from some parent p' via adjacent4_cells. The BFS tree gives a path from seed to any p. Compose: seed→p1 and seed→p2 → reverse → seed→p1→p2.
depends on: IRF-BFS-ADJ (for path-step adjacency)
[IRF-BFS-MAX] :: PENDING → unblocked by IRF-BFS-ADJ
AXIOM 4: is_maximal
Must prove: if p adjacent to comp and g p = color, then p ∈ comp.
Strategy: by_contra. Assume p ∉ comp but p adjacent to p' ∈ comp. When p' was visited, adjacent4_cells p' was computed. By ADJ spec, p ∈ adjacent4_cells p'. p was filtered (p ∉ visited), so p was enqueued. Queue runs to completion → p was dequeued → p visited → p ∈ comp. ⊥
by_contra
queue exhaustion
Strategy: by_contra. Assume p ∉ comp but p adjacent to p' ∈ comp. When p' was visited, adjacent4_cells p' was computed. By ADJ spec, p ∈ adjacent4_cells p'. p was filtered (p ∉ visited), so p was enqueued. Queue runs to completion → p was dequeued → p visited → p ∈ comp. ⊥
depends on: IRF-BFS-ADJ (adjacent4_cells_spec)
[IRF-BFS-ADJ-COMPLETE] :: PENDING (inside current burn)
adjacent4_cells_complete — backward direction
adjacent4 a b → b ∈ adjacent4_cells a.
Wired into adjacent4_cells_spec. The omega + ext + Fin.ext_iff combination should close all 4 branches (RIGHT/LEFT/DOWN/UP). May need `cases` on Fin values to expose the nat arithmetic.
rcases / ext / omega
Wired into adjacent4_cells_spec. The omega + ext + Fin.ext_iff combination should close all 4 branches (RIGHT/LEFT/DOWN/UP). May need `cases` on Fin values to expose the nat arithmetic.
[tau_select_minimal ×2] :: PRE-EXISTING
τ_γ₁ selector — foldl invariant
Unrelated to BFS. foldl accumulates minimum — need to thread
induction hypothesis through foldl state. Pre-existing since τ_γ₁ work.
Low priority relative to BFS chain.
foldl induction
DOWNSTREAM — BLOCKED ON BFS CHAIN 3 items
[IRF-ARC-DSL-003-COVER] :: downstream
extract_objects_covers
Every non-background cell belongs to some object. Follows from extract_objects_impl loop coverage. Unblocked when BFS chain closes.
loop induction
[IRF-ARC-DSL-003-DISJOINT] :: downstream
extract_objects_disjoint
No cell in two objects. Follows from BFS visited-set monotonicity: once visited, never seeded again. Closes after IRF-BFS-TERM full.
visited monotone
[IRF-ARC-DSL-006] :: future boss
Synthesis Engine
find f | f(X₁)=Y₁ ∧ f(X₂)=Y₂. The Boss Fight 2. All object-level transforms (translate, recolor, reflect) must be in scope. Requires full BFS chain first.
Boss Fight 2
> lake build PTTE.ARCGrid
> ✓ connected4_in_finset_refl
> ✓ connected4_in_finset_symm
> ✓ arc_cell_fintype
> ✓ unvisited_decreases (Finset.card_lt_card)
> ✓ flood_fill_bfs [termination_by unvisited+queue.length]
> ✓ flood_fill_bfs_monochrome (induction/3 branches)
> ✓ extract_objects → extract_objects_run (no sorry)
> ⚡ adjacent4_cells_spec — BURNING NOW (split_ifs/omega)
> ✗ sorry: IRF-BFS-CONN (is_connected) — awaiting ADJ
> ✗ sorry: IRF-BFS-MAX (is_maximal) — awaiting ADJ
> ✗ sorry: IRF-ARC-DSL-003-COVER
> ✗ sorry: IRF-ARC-DSL-003-DISJOINT
> ✗ sorry: tau_select_minimal ×2
> 7 sorrys remaining · burn order: ADJ → MAX → CONN → COVER → DISJOINT