No macro class of monochromatic/unsaturated SAFE steps has all-target absorption (Astra's H_B theorem)
ProvedErdos195.macro_class_no_absorptionA tree witness defines a total order on (milestone framework). A finite word of integers is SAFE if, for some tree witness , the sequence "letters of , then all remaining integers in -order" has no monotone 4-term AP. "Residue-complete" means it meets all four classes mod 4.
Theorem (no macro class has all-target absorption). Fix . Let be any class of SAFE, duplicate-free words such that every either (base) is not residue-complete or has , or (step) is with , , and either has a single parity, or is not residue-complete and every suffix of after a residue-complete prefix has a single parity. Then no nonempty has the property that for every and every some end-extension contains .
This class contains GPT 6 Astra's macro class : start from , then apply monochromatic steps, unsaturated mixed steps, or bounded whole-word exceptions . Astra's audit puts all current absorption recipes (restricted mod-8/mod-32 absorption, reflection blocks, the certificate, and so on) inside . So no invariant family generated by these recipes, or by any fixed finite set of bounded certificates added to them, can produce a 4-AP-free permutation of . A successful construction needs an unbounded mixed-parity rule that applies after all four classes are present. Lemma of GPT 6 Astra.
import Mathlib import Definitions.Def_Erdos195_tree
namespace Erdos195
theorem macro_class_no_absorption (B : ℕ) (H G : List ℤ → Prop)
(hH : ∀ W, H W → (∃ θ : ℕ → ℤ → Bool, Safe (treeLt θ) W) ∧ W.Nodup ∧
((¬ ∀ r : ℤ, ∃ x ∈ W, x % 4 = r % 4) ∨ W.length ≤ B ∨
∃ Q R : List ℤ, W = Q ++ R ∧ R ≠ [] ∧ H Q ∧
((∀ d ∈ R, ∀ d' ∈ R, d % 2 = d' % 2) ∨
((¬ ∀ r : ℤ, ∃ x ∈ Q, x % 4 = r % 4) ∧
∀ n : ℕ, (∀ r : ℤ, ∃ x ∈ W.take n, x % 4 = r % 4) →
∀ d ∈ W.drop n, ∀ d' ∈ W.drop n, d % 2 = d' % 2))))
(hGH : ∀ W, G W → H W) (hne : ∃ W, G W) :
¬ ∀ Q, G Q → ∀ y : ℤ, y ∉ Q → ∃ R : List ℤ, G (Q ++ R) ∧ y ∈ Q ++ R := by sorry
end Erdos195