AP049 — half log root comparison — irrationality research

Exact named statement

forall r u h s d. ~h=0 ->
  ~d=0 ->
  Le(r,d) ->
  Le(d,s) ->
  Le(s*s,2*(d*d)) ->
  Le(2*(d*d),s*s+2*(2*d)) ->
  Le(r*(u*u),(r*2)*(h*h)+3*(h*h)) ->
  Le((r*2)*(h*h),r*(u*u)+(h*h)) ->
  Le(r*(u*d),r*(s*h)+7*(h*d)) /\ Le(r*(s*h),r*(u*d)+(h*d))

PD0001 — Le

Fully expanded target AST

Complete certificate and independent checks

38 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: ca484cb2209e8e2ed81d29e1903feb31e830a531b0e621cf00ce722956568c9b
Bundle SHA-256: 04b9f79d32692a6e9a82255c8dc6f5f969d9e7b7ebe1b4776e22906e159a5f3a

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.

AP048

Scope

compare supplied positive half log and dyadic root square witnesses at r at most d with forward error seven over r and reverse error one over r by natural cross products without constructing witnesses or assuming a real identity

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