Exact named statement
((forall a b. (a=b) \/ ~(a=b))) /\ (((forall a b. (Le(a,b)) \/ ~(Le(a,b)))) /\ (((forall a b. (Lt(a,b)) \/ ~(Lt(a,b)))) /\ (((forall b c i v. (BetaAt(b,c,i,v)) \/ ~(BetaAt(b,c,i,v)))) /\ (((forall a n v. (Pow(a,n,v)) \/ ~(Pow(a,n,v)))) /\ (((forall n v. (Factorial(n,v)) \/ ~(Factorial(n,v)))) /\ (((forall b c n v. (Sum(b,c,n,v)) \/ ~(Sum(b,c,n,v)))) /\ ((forall n v. (FloorSqrt(n,v)) \/ ~(FloorSqrt(n,v))))))))))PD0002 — Lt · PD0013 — BetaAt · PD0020 — Pow · PD0001 — Le · PD0051 — FloorSqrt · PD0023 — Factorial · PD0015 — Sum
Complete certificate and independent checks
153 actual local proof nodes. Each node carries its complete ordinary HA proof body.
Full canonical proof bundle · Original HA receipt · Independent Lean receipt
Target SHA-256: ed18ed2d5be19d785c821571ea8789461ac6dcc996c0e26364d9149e77d9d6f0
Bundle SHA-256: e2e83ec51ce4d3cfc724c3e68e01de0d41efde85b51707031d85ee9d7b537c8c
Checked statement containment
These exact targets occur inside this certificate. These links summarize containment, not direct dependency arrows; the downloadable bundle records every private lemma and ordered edge.
Scope
constructively decide natural equality order beta decoding powers factorials sums and integer square roots from replayed totality and value uniqueness without classical axioms or a claim of a complete CApprox verifier
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.