# Validation report

- Wolfram checks: 12 passed, 0 failed.
- Exact dyadic enumeration: 62 phase/register cases (m=1 through 5).
- Independent numerical comparison: direct Fourier sums versus geometric-series sine ratios.
- Lean status is recorded separately in `lean_build_report.txt`.

## Scope

The QPE distribution and selected identities are symbolically or numerically validated in a bounded ideal-noiseless model. Only the resource-count recurrence is intended for Lean formal proof.