CV083 — geometric tail sandwich — irrationality research

Exact named statement

forall r z p b y u h q a. r+z=(2*z)*p ->
  y=b*r+u ->
  h=p*b ->
  Le(u*q,(9*a)*(z*h)) ->
  (y+z*b=(2*z)*h+u) /\ ((Le(y*q,(2*q+9*a)*(z*h))) /\ (Le((2*p)*(z*h),y*p+z*h)))

PD0001 — Le

Fully expanded target AST

Complete certificate and independent checks

14 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: 6ab738597b29754dfe8c2ecd8edd19ed02b665f859a9b263e2eb80903c75afbd
Bundle SHA-256: c6ba62017eda3d139acc2d7694d8e37d2d02da904b4054901c0d2ac9103bde0a

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

natural arithmetic geometric prefix plus actual split and tail bound imply exact balance and both denominator cleared bounds without division cancellation or analytic limit

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