Exact named statement
forall k. exists f p. Factorial(S(S k),f) /\ (Pow(3,k,p) /\ Le(2*p,f))Complete certificate and independent checks
125 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: 906291d44d802e2ac53f432d1d7ae6b05c1920dda811c18335f095def75f9293
Bundle SHA-256: f99f5b94eb22287763f6a6bb48442810c51672f1c13147237cd61c8310601252
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
constructed actual factorial k plus two and power three to k with twice power lower bound not yet a finite exponential sum bound
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.