Paper suitability assessment
Is this the right demonstration paper?
A compact biomedical geometry algorithm that connects Mathematica reproduction, selective Lean proof, production C++, and Parasoft verification.
8/10 Strong candidate—with synthetic data and honest clinical limits
What the paper offers
Small enough to finish—rich enough to matter
Concrete algorithm
Three-point conduction speed and direction on a 3D triangle, with explicit geometric filtering.
Biomedical relevance
Electroanatomic mapping for atrial fibrillation provides a credible safety-sensitive context.
Production connection
The original platform was implemented in C++ with Qt and VTK, making the final C++ phase natural.
coordinates + local activation times → triangle quality → speed + in-plane direction
Four pages keep the claim ledger manageable while still exposing geometry, numerical sensitivity, data limitations, and implementation risk.
Suitability scorecard
Excellent end-to-end fit—not an exact clinical reproduction
Mathematica
9/10
Ideal for geometry, synthetic wavefronts, high precision, noise sweeps, and reference exports.
Lean 4
7/10
Useful for selected geometric properties, but the paper itself is not theorem-heavy.
C++ + Parasoft
9/10
Strong numerical, boundary, robustness, static-analysis, and coverage targets.
Exact paper figures
3/10
Patient data and source are unavailable except by request.
Overall demonstration
8/10
Best presented as algorithm verification using known synthetic ground truth.
Workflow mapping
Every phase has a real job
NormalizeClaims, equations, units, domains, ambiguities
MathematicaExecutable oracle and synthetic ground truth
Lean 4Selected exact geometric guarantees
C++ / ParasoftProduction behavior, safety, tests, coverage
EvidenceTraceability and explicit limitations
The normalized specification—not the notebook—is the shared source of truth for Mathematica, Lean, and C++.
Why Mathematica fits
Build a stronger oracle than the paper provides
Known synthetic truth
- Generate irregular electrode points.
- Assign activation times from a wavefront with known speed and direction.
- Recover the wavefront and quantify error.
- Add controlled coordinate and timing noise.
Executable evidence
- Exact and high-precision formulations.
- Accepted/rejected triangle visualization.
- Error versus noise and degeneracy plots.
- Golden, boundary, and invalid vectors for C++.
synthetic truth → paper algorithm → recovered speed/direction → measured error
This validates the algorithm independently without pretending to reproduce unavailable patient-specific results.
Why Lean 4 fits
Formalize the scientific invariants—not every calculation
Useful proof targets
- Normal is orthogonal to both triangle edges.
- Constructed direction lies in the triangle plane.
- Quality ratio is invariant under uniform scaling.
- Ideal planar wavefront recovery under explicit assumptions.
Keep expectations honest
- The paper has no formal theorem section.
- Real-number proofs do not prove IEEE-754 execution.
- Clinical conclusions are empirical, not Lean targets.
- Blocked claims remain visibly blocked.
best theorem: ideal constant planar wavefront ⇒ recovered direction and speed
Lean adds independent assurance when it proves the normalized claim—not a transcription generated from Mathematica code.
Why C++ and Parasoft fit
The algorithm has exactly the right failure surface
Numerical hazards
Small time differences, small sin(theta), rounding outside the acos domain, overflow, and non-finite values.
Geometric hazards
Collinear points, near-degenerate and elongated triangles, orientation, permutation, and unit conversion.
Verification evidence
Static analysis, golden and property tests, runtime checks, branch/condition coverage, and justified suppressions.
Mathematica provides
High-precision expected values and justified tolerances.
Lean provides
Properties that become concrete C++ test obligations.
Parasoft verifies the actual implementation; Mathematica and Lean connect it back to the intended mathematics.
Blockers and interpretation risks
Two issues make the demo more credible
Unavailable clinical evidence
- No patient electrode dataset.
- No EnSite export samples.
- No MRI registration data.
- Source code is “available upon request.”
Consequence: Figures 4–6, 0.61 m/s average, and 70% overlap cannot be independently reproduced.
Formula interpretation
- The printed
tan(alpha)needs unambiguous parentheses. vdenotes both scalar speed and a later vector.xpq − xpsappears directional, not scaled to physical speed.- Orientation and time-sign conventions are implicit.
Consequence: derive and document the convention before coding.
These are ideal issue-ledger entries—not reasons to stop. Synthetic ground truth lets us test the corrected interpretation.
Recommended demonstration scope
Prove the kernel before rebuilding the platform
Include now
- Figure 3 geometry and all four filters.
- Synthetic planar wavefronts and noise.
- Mathematica notebook, package, audit, and exports.
- Selected Lean proofs with a pinned toolchain.
- Standalone C++ core and CMake tests.
- Parasoft reports and cross-language comparison.
Defer
- Qt interface and complete VTK visualization.
- EnSite file-format reverse engineering.
- MRI registration.
- Patient-specific Figures 4–6.
- The reported 70% overlap result.
- Any claim of clinical validation.
Smallest useful definition of done: a verified conduction-velocity mathematical kernel with traceable evidence.
Success criteria
What a convincing demo must prove
Mathematica recovers known synthetic wavefronts within defined tolerances.
Every geometric filter has boundary and invalid-input tests.
The Mathematica build and paper-specific audit pass.
Selected Lean theorems compile without proof placeholders.
C++ builds cleanly with strict warnings.
C++ and Mathematica agree across deterministic vectors.
Lean-derived properties hold in the production tests.
Parasoft findings are fixed, justified, or explicitly blocked.
Coverage satisfies the selected project policy.
Clinical claims remain marked as not independently reproduced.
The result should say exactly what is formally proved, numerically validated, implementation-verified, and unavailable.
Ready-to-paste kickoff prompt
Start with scope, evidence, and release gates
Use the wolfram-mathematica skill and relevant C/C++/Parasoft guidance to build an end-to-end verification demonstrator from C:\Amp_demos\Biosense-19-7-2026\ieee-biomed-heart.pdf.
Create the project under C:\Amp_demos\Biosense-19-7-2026\heart-cv-verification. Reproduce the paper's triangle-based conduction-velocity kernel using synthetic planar wavefronts with known ground truth. Build a Mathematica package/notebook/audit and exported reference vectors; selectively prove central geometric properties in Lean 4 without sorry; implement a standalone C++ kernel; run differential, property, boundary, and robustness tests; verify with Parasoft C/C++test; and produce claim-to-evidence traceability.
Do not claim reproduction of patient-specific figures or clinical findings because the source data is unavailable. Investigate the ambiguous tan(alpha) parentheses and the paper's scalar/vector use of v before coding. Use explicit domains, units, numerical tolerances, and release gates. Continue through implementation and verification rather than stopping at a plan.
Full prompt: START_PROCESS_PROMPT.mdThe full prompt beside this presentation contains the exact artifacts, phase gates, Lean targets, C++ tests, and Parasoft expectations.