Conservative definition
Parameters: ap, an, bp, bn, H
∃ x. x = ap + an + 2 · (bp + bn) ∧ x ≤ HHA + 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: ap, an, bp, bn, H
∃ x. x = ap + an + 2 · (bp + bn) ∧ x ≤ H