Named statement
forall p m d h. IRatValid(p,m,d) -> IRatEq(p,m,d,p+h,m+h,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; 12,628 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: 75ff1c4c0f8885d395438dd9f33aaf6274d3fd1e4d34e982a9db50255d05105e
Certificate SHA-256: 2a65c3ea35af78fb33f9939d215a4a11169112140ba30faa0726a22ec2d51db7
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.