Conservative definition
Parameters: ab, ac, r, N
∀ x. ∀ y. ∀ z. S S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ n. ab = n · S (S x · ac) + y) → S z ≤ S (S S x · ac) ∧ (∃ n. ab = n · S (S S x · ac) + z) → S r · z ≤ r · yHA + 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, r, N
∀ x. ∀ y. ∀ z. S S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ n. ab = n · S (S x · ac) + y) → S z ≤ S (S S x · ac) ∧ (∃ n. ab = n · S (S S x · ac) + z) → S r · z ≤ r · y