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