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