ESL technical demonstration · 2026
Beyond “nonzero”
Certifying floating-point Heat-Method numerics with Amp, Wolfram Mathematica 15, and Lean 4.
Built by ESLIsraeli reseller of Wolfram products · Wolfram global sales — Israel ↗
Starting point · Ferumlab article
A mathematically positive field can become a computational void.
Heat Method dependency
(M + ΔtK)u = Mu₀
X = −∇u / ‖∇u‖
X = −∇u / ‖∇u‖
If tiny temperatures become exact zero, the normalized direction field is undefined or misleading.
The article’s response
- Replace one implicit solve with many explicit substeps.
- Use Decimal or mpmath arbitrary precision.
- Choose approximately one substep per grid dimension.
Our question: does this merely make values nonzero—or make them correct?
Amp as the orchestrator
One claim ledger. Three independent evidence lanes.
Wolfram 15exact algebra + numerical experiments
→
Ampsource audit · build · traceability
→
Lean 4kernel-checked exact theorems
article → normalized mathematicsreproducible scriptsmachine-readable evidenceformalization mapadversarial audit
Wolfram process
Exact first. Precision becomes an explicit engineering parameter.
01 · derive
Exact Q1 operators
Construct rational mass and stiffness matrices before any numerical rounding.
Mₑ = hₓhᵧ/36 · A
Kₑ = 1/(6hₓhᵧ) · B
Kₑ = 1/(6hₓhᵧ) · B
02 · execute
Controlled arithmetic
Run the same normalized stencil at MachinePrecision and 500 digits without downcasting the result path.
03 · classify
Explain every zero
Separate prescribed boundary zeros, finite-front zeros, and unexpected behind-front zeros.
The exact interior stencil
Positivity is conditional—not a property of the word “explicit.”
uᵏ⁺¹ᵢⱼ = (1 − 8r/3)uᵏᵢⱼ + (r/3) Σ₍ₚ,ᵩ₎∈N₈₍ᵢ,ⱼ₎ uᵏₚᵩ, r = Δtₛ/h²
0 ≤ r ≤ 3/8
CFL-style condition ensuring all nine stencil weights are nonnegative
Σw = 1
Constant data is preserved by the interior stencil; boundary treatment remains a separate contract
Finite propagation is also exact: after k steps, a local eight-neighbor stencil cannot reach nodes more than k Chebyshev edges away.
Measured evidence
Mesh refinement crosses the binary64 precision wall.
37,647
reachable interior nodes rounded to zero
0 negatives
the CFL positivity contract held in both article-sized runs
What we corrected beyond the article
“Arbitrary precision” must cover the entire data path.
Me, Ke = q1_element_matrices(float(dx), float(dy))
Ke = [[datatype(Ke[i,j]) ...]]
# rounded binary64 coefficients do not
# become exact after conversion
Tr = np.zeros((n,m))
G = np.zeros((n-1,m-1,2))
# arbitrary values are downcast on output
Three algorithmic issues found
- Fixed ε = 10⁻⁶: lumped mass scales as h²; valid corner nodes become inactive near N = 501.
- Unused boundary_values: accepted by the API but never imposed.
- n = max(Nₓ,Nᵧ): a geometry heuristic, not a convergence certificate.
Nonzero propagation and temporal accuracy are different claims.
Lean 4 proof layer
The theorem prover checks the contract—not the screenshot.
✓
centerCoeff_nonneg
r ≤ 3/8 ⇒ 0 ≤ 1 − 8r/3
r ≤ 3/8 ⇒ 0 ≤ 1 − 8r/3
✓
q1Update_nonneg
nonnegative stencil + CFL ⇒ nonnegative update
nonnegative stencil + CFL ⇒ nonnegative update
✓
constant_preserved
all-equal neighborhood remains equal
all-equal neighborhood remains equal
✓
zero_stencil_stays_zero
the basis of finite-front classification
the basis of finite-front classification
theorem q1Update_nonneg
(hr₀ : 0 ≤ r)
(hr : r ≤ 3 / 8)
(hc : 0 ≤ c)
(h₁ ... h₈ : 0 ≤ nᵢ) :
0 ≤ q1Update r c n₁ ... n₈ := by
have hcCoeff := centerCoeff_nonneg hr₀ hr
have hnCoeff := neighborCoeff_nonneg hr₀
positivity
Build: 8,656 jobs · exit 0
No sorry · no admit · no axiom
Trust boundary
Formal proof and numerical evidence answer different questions.
Formally proved
Exact local algebra
Coefficient signs, positivity preservation, constant preservation, and zero-stencil behavior over real numbers.
Numerically validated
Concrete execution
110/300 grids, 500-digit stress case, zero classification, temporal refinement, and exported figures.
Not claimed
Outside this proof
IEEE-754 hardware correctness, Wolfram/SciPy internals, irregular-mesh convergence, and the full Poisson distance reconstruction.
A kernel-checked theorem cannot rescue a mistranscribed model. Amp maintains the mapping from article → normalized mathematics → Wolfram implementation → Lean theorem.
Corrected Python implementation
The audit became executable, independently checked evidence.
field = solve_explicit_q1(
n=71,
diffusion_factor=Fraction(1, 100_000_000),
steps=70,
backend="decimal",
precision=500,
fixed_values={(2, 3): Decimal("7")}
)
assert isinstance(min_positive, Decimal)
assert unexpected_zeros == 0
Fixes implemented
- Q1 matrices constructed directly in float, Decimal, or mpmath—never converted from float64.
- Boundary and fixed values imposed after every substep.
- CFL violation fails loudly outside 0 ≤ r ≤ 3/8.
- Finite-front diagnostics distinguish algorithmic zeros from underflow.
- Arbitrary-precision fields remain arbitrary precision through output.
9 / 9
Python tests passed
3.469×10⁻¹⁸
max |Python − Wolfram|
60 → 0
stress-case underflow zeros
Real-life implications
Tiny fields drive large decisions.
Geometry & robotics
Geodesic distance, path planning, mesh parameterization, collision envelopes, and navigation around narrow passages.
Physics & engineering
Heat transfer, diffusion, electrostatics, reaction transport, FEM preconditioning, and multiscale simulation.
Medical & scientific
Anatomical surface distance, segmentation propagation, dose fields, molecular surfaces, and uncertainty-sensitive inverse problems.
Failure is not limited to a blank plot. A zero gradient can change a direction field, reroute an optimizer, break a normalizer, or silently bias a downstream Poisson solve.
Commercial usage
From research artifact to numerical assurance pipeline.
Product engineering
- Precision policies selected from mesh and tolerance.
- Regression gates for positivity, residuals, and unexpected zeros.
- Golden arbitrary-precision references for optimized C++/GPU solvers.
- Lean contracts for safety-critical numerical kernels.
Customer-facing assurance
- Reproducible evidence packs for design reviews.
- Traceable separation of proved, validated, and assumed claims.
- Early warning before increasing mesh density breaks binary64.
- MIT-licensed foundation for commercial adaptation.
digital twinsCAE/FEM platformsrobotics SDKsmedical imagingsimulation certificationsolver QA
Deliverable
Executable. Audited. Formally scoped.
13 / 13
Wolfram audit checks passed
8,656
Lean build jobs completed
Repository contents
- Reusable Wolfram package and Mathematica notebook
- Corrected Python solver with 9 regression/property tests
- Build, audit, CSV, JSON, and visual evidence
- Pinned Lean 4 + Mathlib proof project
- Claim-to-proof formalization map and MIT license
ESL · IsraelWolfram technical expertise, numerical engineering, and formal assurance.