Exact named statement
forall r p b a s v. ~b=0 ->
~p=0 ->
Le(r,p) ->
Le(a*v,b*s) ->
Le(p*(b*s),p*(a*v)+2*(b*a)) ->
Le(r*v,(r*2)*b+b) ->
Le((r*2)*b,r*v+b) ->
Le(r*s,(r*2)*a+3*a) /\ Le((r*2)*a,r*s+a)Complete certificate and independent checks
28 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: 3d7f11a02582d2bf7b63377cc8ec2bbabf74c584db7e7e1f5627256c208e7c84
Bundle SHA-256: 7291b21a18f894888444ab9878c95369fecca20d89d7797c733d11b451fd8d09
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
combine supplied finite cross product error two over p and reference error one over r with r at most p by positive cancellation to obtain upper error three over r and lower error one over r without constructing or identifying any analytic object
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.