Conservative definition
Parameters: b, c, L, k
∀ x. ∀ y. S x ≤ k → S x ≤ L ∧ (S y ≤ S (S x · c) ∧ (∃ z. b = z · S (S x · c) + y)) ∨ L ≤ x ∧ y = 0 → y = 0HA + 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: b, c, L, k
∀ x. ∀ y. S x ≤ k → S x ≤ L ∧ (S y ≤ S (S x · c) ∧ (∃ z. b = z · S (S x · c) + y)) ∨ L ≤ x ∧ y = 0 → y = 0