Named statement
forall p m d k. IRatValid(p,m,d) -> ~(k=0) -> IRatEq(p,m,d,p*k,m*k,d*k)Every named predicate expands conservatively to the existing HA syntax. These definitions contain no accuracy promises or theorem assumptions.
Fresh HA and independently compiled Lean checks
Download the exact canonical proof bundle (gzip) · Original run record.
1 local nodes; 17,627 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: b07b8ed827c19e15e27f3dd746a89445ec5326208631ec81e298da144cd716fb
Certificate SHA-256: 429fa6e2ea7a800c115327a3c465951c47da8e46ffcc71e40e3654e61c1303f0
Current checked leaves · Larger planning cone · Local definition DAG.
This is local exact-certificate evidence, not an Alpha/Stable admission or a completed irrationality proof.