Exact named statement
forall d x L j a b. ~d=0 ->
Le(x,L*d) ->
Le(2*L,S j) ->
((S j)*d)*b=x*a ->
Le(2*b,a)Complete certificate and independent checks
23 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: 0ed9c296638e7d978dbfb8e18e70dba5fbd546cda5f0e856d746cddb49f5ba40
Bundle SHA-256: 8c573ecc91ad5f0f76f2f09bf876aa3d6c442aaab055155a442382b3dc4ae9e4
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 halving of each supplied exponential recurrence step beyond twice an arbitrary natural argument bound by positive full coefficient cancellation including zero argument without a finite sum or analytic assumption
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.