HA + independent Lean evidence · Research, not Alpha admission

ND0445 — NatLinearBound

Full irrationality (IR072/G121) remains open. Stable: 432. Alpha v35: 4,318. This checkpoint changes neither catalogue.

Conservative definition

Parameters: alpha, beta, gamma, ab, ac, bb, bc, cb, cc, N

∀ x. ∀ y. ∀ z. ∀ n. S x ≤ N → S y ≤ S (S x · ac) ∧ (∃ m. ab = m · S (S x · ac) + y) → S z ≤ S (S x · bc) ∧ (∃ m. bb = m · S (S x · bc) + z) → S n ≤ S (S x · cc) ∧ (∃ m. cb = m · S (S x · cc) + n) → gamma · n ≤ alpha · y + beta · z

Definition prerequisites

PD0002 · PD0013 · PD0001

Theorem uses (notation, not proof premises)

CV095