Exact named statement
forall k d p r. Pow(2,k,d) ->
Pow(3,S(2*k),p) ->
Pow(2,k+2,r) ->
(~d=0) /\ ((~p=0) /\ ((~r=0) /\ ((Le(d,p)) /\ (Le(d,r)))))Complete certificate and independent checks
128 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: a41d4293a571408ac987bb69b06a49ec1afd6527e75e6d2404265714b00fb69e
Bundle SHA-256: 59a7b1470dfeb2ff50255f79fa96efc0cb349ddcb36ba6ffd8fcc0643ee68c02
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
actual supplied dyadic logarithm and exponential cutoff powers are positive and both cutoff powers dominate the actual dyadic denominator including zero precision
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.