Named statement
forall p m d q n e r s f. IRatEq(p,m,d,q,n,e) -> IRatEq(q,n,e,r,s,f) -> IRatEq(p,m,d,r,s,f)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; 66,239 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: ece8e6152f2026a946640ae397e7bb249f4e0afa100380d3831522708328c8e8
Certificate SHA-256: 44f7e7884fd34f582768032ea2b91b9a24e45744b83f23368eae49755d0aebbf
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.