Named statement
forall p m d q n e. IRatEq(p,m,d,q,n,e) -> IRatEq(m,p,d,n,q,e)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; 18 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: c23712611e4fa9d7630c08e3f0543d4d8d6df6e7b03c01b0b5c02da8ea18c135
Certificate SHA-256: 73a5ab398f643e71657f904a78d43e58a8c327ded87ae1eecb6376a5b3389aba
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.