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