Conservative definition
Parameters: ab, ac, D, N
∀ x. ∀ y. S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ z. ab = z · S (S x · ac) + y) → y ≤ DHA + independent Lean evidence · Research, not Alpha admission
Full irrationality (IR072/G121) remains open. Stable: 432. Alpha v35: 4,318. This checkpoint changes neither catalogue.
Parameters: ab, ac, D, N
∀ x. ∀ y. S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ z. ab = z · S (S x · ac) + y) → y ≤ D