Exact named statement
forall r p. Pow(2,S(S(18*r)),p) ->
~p=0 /\ Le(r,p)Complete certificate and independent checks
37 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: 936a988b2a6fae61ebb3206a2a33746d5c8ad2e23501f642b0528b6b9e0e7877
Bundle SHA-256: 96815002d9cbada491bb67202df76d032ac56ed7b8f0c85b32d92a1406e3368a
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
prove generic binary growth n plus one at most two to n by ordinary induction then bound the actual two to eighteen r plus two cutoff power below by r without materializing large ground powers
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.