HA + independent Lean evidence · Research, not Alpha admission

ND0383 — IRatEq

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

Theorem uses (notation, not proof premises)

AP019 · AP020 · AP021 · AP036