Conservative definition
Parameters: ub, uc, H
∀ x. S x ≤ H → ∃ y. S y ≤ S (S x · uc) ∧ (∃ z. ub = z · S (S x · uc) + y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 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: ub, uc, H
∀ x. S x ≤ H → ∃ y. S y ≤ S (S x · uc) ∧ (∃ z. ub = z · S (S x · uc) + y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))