HA + independent Lean evidence · Research, not Alpha admission

ND0444 — IRatLe

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

Conservative definition

Parameters: p, m, d, P, M, D

¬d = 0 ∧ (¬D = 0 ∧ p · D + M · d ≤ m · D + P · d)

Definition prerequisites

ND0382 · PD0001

Theorem uses (notation, not proof premises)

AP032 · CV075 · CV076 · CV077 · CV080 · CV084 · CV085 · CV091 · CV093 · CV099 · CV102 · SQ007