AP080 — requested power precision — irrationality research

Exact named statement

forall d e a b M g k u v D E C r. ~d=0 ->
  ~e=0 ->
  Le(a,M*d) ->
  Le(b,M*e) ->
  Le(b*d,a*e+g) ->
  Le(a*e,b*d+g) ->
  Pow(a,S k,u) ->
  Pow(b,S k,v) ->
  Pow(d,S k,D) ->
  Pow(e,S k,E) ->
  Pow(M,k,C) ->
  Le((r*(S k))*(g*C),d*e) ->
  ~D=0 /\ (~E=0 /\ (Le(r*(v*D),r*(u*E)+D*E) /\ Le(r*(u*E),r*(v*D)+D*E)))

PD0020 — Pow · PD0001 — Le

Fully expanded target AST

Complete certificate and independent checks

138 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: 486fc0a6d7574427552d0fefc51c3ea3d4176a018a649275113340d0cf60d1d1
Bundle SHA-256: b99a77859fb3f803516deef4349cb3c9bbf9345efccbe959770537b6f782c1e6

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.

AP076 · AP077 · AP078 · AP079

Scope

prove requested rational power precision under an explicit input budget by constructing denominator product powers and replaying actual successor and product identities without cancellation or analytic axioms

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.