HA + independent Lean evidence · Research, not Alpha admission

ND0382 — IRatValid

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

Conservative definition

Parameters: p, m, d

¬d = 0

Definition prerequisites

Theorem uses (notation, not proof premises)