Conservative definition
Parameters: d, i, a
(∃ x. i = 2 · x ∧ a = 0) ∨ (∃ x. i = S (2 · x) ∧ i · a = 2 · d)HA + 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: d, i, a
(∃ x. i = 2 · x ∧ a = 0) ∨ (∃ x. i = S (2 · x) ∧ i · a = 2 · d)