Named statement
forall p m d. IRatValid(p,m,d) -> IRatEq(p,m,d,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; 83 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: e722f9ad9273a9bda607c55d52fa50d9db3ce71149d160f14a6a76ad24abbd63
Certificate SHA-256: 7417b07b645044b957b2977ee93d9769fb144f10622c64d29e3e22053fa0976f
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.