01
Input
LinkedIn explanation + authoritative QPE reference.
Source identifiedCase study 01 / Quantum Phase Estimation
From a quantum claim
to a checked result.
How MantiQ handles an algorithm explanation: make its assumptions explicit, build it, test it, and show exactly what the evidence supports.
A working educational case study. Browser simulation, independent Wolfram results, and a scoped Lean proof. No quantum hardware used.
THE FIRST CHECK / IDEAL QPE
One phase. One exact outcome.
φ = 3/8 · m = 3 → |011⟩
000
001
010
011
100
101
110
111
Theoretical probability100% at 011
Then try 1/3. The certainty disappears.
The verification requirement does not.
← Swipe to navigate → or use arrow keys
01 / Input and interpretation
A useful explanation.
Not yet an engineering specification.
The supplied LinkedIn post describes the standard QPE flow. MantiQ turns that narrative into testable statements.
SOURCE IDEA / PARAPHRASED
Controlled powers encode phase.
An inverse QFT makes it observable.
Measurement gives a binary estimate.
Correct as a high-level description. But which input state, which bit order, and what does “accuracy” mean?
The screenshot was inspected manually. No OCR or automated document-ingestion capability is claimed here.
Questions that become explicit requirements
- Is the input an eigenstate?A superposition can produce multiple phase peaks.
- Can the phase fit in m bits?Only an exactly representable phase has a certain ideal outcome.
- What is being verified?A numerical model, an implementation, a theorem, or a physical device are different claims.
- What does extra precision cost?Repeated controlled-U requires 2ᵐ − 1 applications.
Technical reference: IBM Quantum Learning, “Phase estimation procedure”. Source links and reproducible artifacts are on the final slide.
02 / The MantiQ production line
Seven stages.
No silent upgrade from claim to proof.
This case study executes the modeling and verification steps. The stage map explains the methodology, not an autonomous ingestion product.
02
Convert
Manual transcription of the mathematical scope. OCR unnecessary.
Explicitly manual03
Understand
Eigenstates, phase range, bit order, exactness and cost.
Assumptions recorded04
Compute
Wolfram Fourier-sum model and a browser gate simulator.
Two implementations05
Verify
Independent probabilities, fault tests and a Lean cost proof.
Bounded evidence06
Engineer
Interactive controls, circuit trace, sampling and failure gates.
Runnable artifact07
Output
Downloadable source, notebook, proof and execution evidence.
Reproducible packageThe contract: a passing simulation is not a proof of the whole algorithm. A checked theorem is not evidence of physical hardware performance.
03 / Normalize the mathematics
Make the model small enough to inspect.
The mathematical contract
U|u⟩ = e2πiφ|u⟩
φ is a fraction of a full turn, not an angle in radians. With N = 2ᵐ, outcome y represents phase y/N, modulo one.
p(y) = | N⁻¹ ∑x=0N−1 e2πix(φ−y/N) |²
Independent browser oracle: the squared sine ratio obtained from the finite geometric series, with the removable singularity handled explicitly.
The actual simulated system
One target qubit with a diagonal unitary:
U = diag(e2πiφA, e2πiφB)
Single eigenstate: target |0⟩.
Superposition: √w |0⟩ + √(1−w) |1⟩.
The browser evolves the joint state using Hadamard gates, controlled powers, swaps, and inverse-QFT controlled-phase gates. It sums over the target qubit to obtain the displayed marginal.
Ideal, noiseless gatesm = 2…6 in the UIMSB-first displayed bitsClassical simulation
Important: the demo supplies the phases to construct U. It illustrates and checks QPE; it does not discover a secret phase or demonstrate a quantum speedup.
04 / Live executable experiment
Change the input. Inspect the evidence.
Real calculations in your browser. No backend, no hardware, no canned output.
Gate-level circuit
Outcome probabilityFixed scale: 0 to 100%
Gate simulationAnalytical referenceSample frequency
…Most likely outcome*
…Peak probability
…Phase-grid spacing
Inspect all probabilities and sampled counts
| Bits | Phase | Simulated | Reference | Count |
|---|
05 / Verification that can say no
A useful test must catch a plausible mistake.
Start with 3/8 and three estimation qubits. Each mistake below changes the simulated distribution while the independent reference remains unchanged.
011 → 101
Use QFT instead of inverse QFT
The sign error sends phase 3/8 to 5/8. The result is sharply peaked, but wrong. A clean-looking chart is not sufficient evidence.
011 → 110
Reverse the output bits
The same bits become a different number: 6/8 instead of 3/8. Asymmetric test inputs expose an error that 000 or 111 would hide.
U⁴ → I
Omit the largest power
One qubit no longer accumulates its required phase. The probability distribution disagrees with the reference and the gate blocks a pass.
A fault can be invisible for special inputs, such as zero phase. This is why the test suite uses many phases rather than relying on one successful run.
06 / Claim-by-claim evidence
What has actually been established?
The statuses apply to the stated scope. They do not combine into a blanket “QPE formally verified” claim.
| Claim | Evidence status | Artifact and boundary |
|---|---|---|
| QPE-01 · Exact 3/8 example | SYMBOLICALLY VALIDATED | Wolfram exact amplitudes and normalization; 62 dyadic cases across m = 1…5. |
| QPE-02 · Non-dyadic and mixed inputs | NUMERICALLY TESTED | Direct Fourier sum versus geometric formula; independent exported vectors, bounded cases. |
| QPE-03 · Browser gate simulator | RUNTIME CHECK PENDING | Runtime comparison loads the independently generated Wolfram vectors. |
| QPE-04 · Repeated-U resource count | FORMALLY PROVED | Lean 4: cost(m) + 1 = 2ᵐ. Only this recurrence is proved; not the simulator or full QPE. |
| QPE-05 · Hardware performance / speedup | NOT ESTABLISHED | No device run, no noise calibration, no speedup benchmark, no physical measurement. |
The repeated-U cost assumes powers are built by repetition. This toy diagonal unitary permits direct phase rotations, so the count is not this simulator’s wall-clock cost or its compiled gate count.
07 / Reproduce, inspect, extend
The evidence travels with the demo.
Open the notebook, inspect the proof, or rerun the checks. Nothing here requires access to the private MantiQ product.
Run the same checks locally
node validate.mjs wolframscript -file evidence/build.wls # From evidence/lean: lake build
Download the folder from the public source repository, preserving its structure. The HTML runs standalone; the external Wolfram comparison requires serving the folder over HTTP.
Browser-model test source · Wolfram build script · Lean build evidence
Primary technical reference:
IBM Quantum Learning: Phase estimation procedure ↗Input inspiration: the user-supplied LinkedIn group post. Screenshot inspected privately; not republished. No affiliation or endorsement by IBM or the post’s author is implied.