Exact named statement
forall t k x y. Pow(t,S(2*k),x) ->
Pow(t*t,k,y) ->
x=t*yComplete certificate and independent checks
27 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: 1c4010443924fa4b57d39c7f9952916050880d32d433ee211b5b5cef8a1a4f0f
Bundle SHA-256: 84a656f636badc245aa0408832eadba4f4cdc185f95f94d4ba2e540ccdf4113d
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
normalize both actual supplied power computations to the squared base by explicit doubled exponent induction and a final successor allowing zero base and zero index without cancellation
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.