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