A real computation: quantum mechanics, end to end

This module runs quantum mechanics through the calculus (the paper cites its twoStateChecks as the fuel example and leaves the rest here): the particle in a box exercises the scalar fragment and forces the rational exponents, the two-state system exercises spaces, linear maps, and the compiled path down to BLAS, and one example thus crosses four layers of the development: rational exponents in the statics, fuel in the dynamics, parametricity at the interface, and erasure on the path to the machine.

The particle in a box

The evaluator from LambdaS.Dynamics is generic in its numeric carrier, so the same definition that unit_soundness_total and erasure_correct are proved about is instantiated here at Float and executed by #eval, and compiled to C by lake build.

What the type checker is asked to prove

Two things, and both are physics rather than bookkeeping.

The uncertainty product is a pure number. ΔxΔp/ħ has type Q 1. Nothing in the term says so; it follows from ħ being kg·m²/s, Δp being kg·m/s and Δx being m, and the checker deriving it. Had any exponent been wrong the term would not typecheck at all, so the printed value cannot be a dimensionally meaningless number.

A wavefunction carries a half-power of length. In one dimension ψ has unit m^(-1/2), so that |ψ|² is a probability density at m⁻¹ and |ψ|²dx is dimensionless. This is the example that forces ℚ exponents: m^(-1/2) is not expressible in F#, in Data.Dimensional, or in the Isabelle ISQ development, all of which fix exponents to ℤ. pow is primitive here for the reason LambdaS.NonDef.sqrt_not_definable gives, and over ℚ it is total.

Numbers

CODATA values, written as exact rationals and converted to Float once per literal by Num.ofRat. The box is 1 nm wide and holds an electron; the ground state comes out near 0.376 eV, which is the textbook answer.

Units of the problem

@[reducible, inline]

abbrev LambdaS.QM.joule : UExp Examples.Base 0

The joule, kg·m²/s².

Equations

• LambdaS.QM.joule = (LambdaS.Term.mul LambdaS.Examples.kg (LambdaS.Term.mul LambdaS.Examples.m LambdaS.Examples.m)).div (LambdaS.Term.mul LambdaS.Examples.sec LambdaS.Examples.sec)

@[reducible, inline]

abbrev LambdaS.QM.action : UExp Examples.Base 0

Action, kg·m²/s, the unit of ħ.

Equations

• LambdaS.QM.action = (LambdaS.Term.mul LambdaS.Examples.kg (LambdaS.Term.mul LambdaS.Examples.m LambdaS.Examples.m)).div LambdaS.Examples.sec

@[reducible, inline]

abbrev LambdaS.QM.momentum : UExp Examples.Base 0

Momentum, kg·m/s.

Equations

• LambdaS.QM.momentum = (LambdaS.Term.mul LambdaS.Examples.kg LambdaS.Examples.m).div LambdaS.Examples.sec

Terms

@[reducible, inline]

abbrev LambdaS.QM.qty (v : ℚ) (u : UExp Examples.Base 0) : Examples.Term₀

A dimensioned literal: a magnitude times a unit constant.

Equations

• LambdaS.QM.qty v u = (LambdaS.Tm.lit v).mul (LambdaS.Tm.ucon u)

@[reducible, inline]

abbrev LambdaS.QM.num (v : ℚ) : Examples.Term₀

A dimensionless literal.

Equations

• LambdaS.QM.num v = LambdaS.Tm.lit v

@[reducible, inline]

abbrev LambdaS.QM.sub (a b : Examples.Term₀) : Examples.Term₀

Subtraction, as addition of a negated literal multiple. Λs has no primitive subtraction; a − b is a + (−1)·b, and the unit rule for add still forces both sides to agree.

Equations

• LambdaS.QM.sub a b = LambdaS.Tm.add a (LambdaS.Tm.mul (LambdaS.QM.num (-1)) b)

def LambdaS.QM.hbar : Examples.Term₀

Reduced Planck constant, 1.054571817e-34 kg·m²/s.

Equations

• LambdaS.QM.hbar = LambdaS.QM.qty (1054571817 / 10 ^ 43) LambdaS.QM.action

def LambdaS.QM.mass : Examples.Term₀

Electron mass, 9.1093837015e-31 kg.

Equations

• LambdaS.QM.mass = LambdaS.QM.qty (91093837015 / 10 ^ 41) LambdaS.Examples.kg

def LambdaS.QM.width : Examples.Term₀

Box width, one nanometer.

Equations

• LambdaS.QM.width = LambdaS.QM.qty (1 / 10 ^ 9) LambdaS.Examples.m

def LambdaS.QM.pi : Examples.Term₀

π, to fourteen places. Dimensionless, as every literal in Λs is.

Equations

• LambdaS.QM.pi = LambdaS.QM.num (314159265358979 / 10 ^ 14)

The ground state

E₁ = π²ħ² / (2mL²).

def LambdaS.QM.groundEnergy : Examples.Term₀

Equations

• One or more equations did not get rendered due to their size.

Uncertainties

For the ground state of an infinite square well, Δp = πħ/L and Δx = L·√(1/12 − 1/(2π²)).

def LambdaS.QM.deltaP : Examples.Term₀

Equations

• LambdaS.QM.deltaP = (LambdaS.Tm.mul LambdaS.QM.pi LambdaS.QM.hbar).div LambdaS.QM.width

def LambdaS.QM.deltaX : Examples.Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.QM.uncertainty : Examples.Term₀

The physics statement is the type. ΔxΔp/ħ is dimensionless, and the checker proves it from the units of ħ, Δp and Δx alone.

Equations

• LambdaS.QM.uncertainty = (LambdaS.Tm.mul LambdaS.QM.deltaX LambdaS.QM.deltaP).div LambdaS.QM.hbar

The wavefunction, where ℚ exponents are forced

ψ(x) = √(2/L)·sin(πx/L). The amplitude carries m^(-1/2).

def LambdaS.QM.amplitude : Examples.Term₀

The normalization amplitude √(2/L), at unit m^(-1/2).

Equations

• LambdaS.QM.amplitude = LambdaS.Tm.pow (1 / 2) ((LambdaS.Tm.lit 2).div LambdaS.QM.width)

def LambdaS.QM.density : Examples.Term₀

|ψ|² is a probability density, at m⁻¹.

Equations

• LambdaS.QM.density = LambdaS.Tm.mul LambdaS.QM.amplitude LambdaS.QM.amplitude

def LambdaS.QM.probability : Examples.Term₀

|ψ|²·dx is dimensionless, which is what makes the normalization integral a pure number, and what makes log of it well-typed while log |ψ|² is not.

Equations

• LambdaS.QM.probability = LambdaS.Tm.mul LambdaS.QM.density (LambdaS.Tm.ucon LambdaS.Examples.m)

Running it

eval is the evaluator of LambdaS.Dynamics (proved sound in LambdaS.Soundness and total in LambdaS.Normalization), instantiated at Float. No conversions occur here, so the conversion-factor argument is the constant 1.

def LambdaS.QM.run (e : Examples.Term₀) : Option Float

Evaluate a closed term to a magnitude.

Equations

• LambdaS.QM.run e = match LambdaS.evalC (fun (x x_1 : LambdaS.UExp LambdaS.Examples.Base 0) => 1.0) 1000 [] e with | some (LambdaS.Val.scalar x) => some x.mag | x => none

def LambdaS.QM.runMeas (e : Examples.Term₀) : Option (Val Float Examples.Base Examples.Dim)

Evaluate, keeping the unit the value carries at runtime, which unit_soundness_total guarantees equals the one the checker predicted.

Equations

• LambdaS.QM.runMeas e = LambdaS.evalC (fun (x x_1 : LambdaS.UExp LambdaS.Examples.Base 0) => 1.0) 1000 [] e

def LambdaS.QM.eV : Float

One electronvolt in joules, for reporting.

Equations

• LambdaS.QM.eV = 1602176634e-28

def LambdaS.QM.report : String

The report.

def LambdaS.QM.negBase : Examples.Term₀

(-8)^(1/3): a non-integer power of a negative argument, an undefined point of the classical operation. The Float carrier's npow is C's pow, which returns NaN there; the ℝ semantics reads through Real.rpow, whose conventional value there is 1, not a root. The two carriers part ways at this point as they do at division by zero, and no theorem reaches the compiled number (LambdaS.Num). The check pins the loud answer: the evaluator does not get stuck (the term is well typed and pow is total), and what it returns is NaN.

Equations

• LambdaS.QM.negBase = LambdaS.Tm.pow (1 / 3) (LambdaS.Tm.lit (-8))

A two-state system

The particle in a box is closed-form scalars. This exercises the other half of the calculus: spaces, linear maps, and the rank-one condition that makes their units cheap.

The system is a symmetric two-level system (an ammonia molecule, a spin in a transverse field, a qubit) with Hamiltonian

H = [ 0  -A ]        A = 10⁻⁴ eV
    [ -A  0 ]

Amplitudes are dimensionless, so the state space is [1, 1]; the Hamiltonian maps it to [J, J], and by LambdaS.Map's rank-one condition its entries carry J / 1 = J. Applying it to a state therefore yields energies, and ⟨ψ|H|ψ⟩ : Q J; the physics statement is the type.

@[reducible, inline]

abbrev LambdaS.QM.St : Sp Examples.Base 0

Dimensionless amplitudes.

Equations

• LambdaS.QM.St = [1, 1]

@[reducible, inline]

abbrev LambdaS.QM.En : Sp Examples.Base 0

Energies.

Equations

• LambdaS.QM.En = [LambdaS.QM.joule, LambdaS.QM.joule]

@[reducible, inline]

abbrev LambdaS.QM.qmCtx : Ctx Examples.Base Examples.Dim 0 0

The context: a Hamiltonian and a state, supplied as data.

Matrices and state vectors arrive through the environment for the same reason unit constants do (LambdaS.Fundamental): a program that could name its data would not be scale-invariant. A numeric program takes its operators as input.

Equations

• LambdaS.QM.qmCtx = [LambdaS.Ty.lin LambdaS.QM.St LambdaS.QM.En, LambdaS.Ty.vec LambdaS.QM.St]

@[reducible, inline]

abbrev LambdaS.QM.ket (i : ℕ) : Examples.Term₀

(H|ψ⟩)ᵢ: an energy.

Equations

• LambdaS.QM.ket i = ((LambdaS.Tm.var 0).mapp (LambdaS.Tm.var 1)).idx i

def LambdaS.QM.expectH : Examples.Term₀

⟨ψ|H|ψ⟩, summed over the two basis states. Real amplitudes, so no conjugation is needed; see the note on carriers in LambdaS.Num.

Equations

• One or more equations did not get rendered due to their size.

The data

def LambdaS.QM.splitJ : Float

The inversion splitting, 10⁻⁴ eV in joules.

Equations

• LambdaS.QM.splitJ = 1602176634e-32

def LambdaS.QM.hamiltonian : Val Float Examples.Base Examples.Dim

H = [[0, −A], [−A, 0]], a linear map St ⊸ En.

Equations

• LambdaS.QM.hamiltonian = LambdaS.Val.matrix [[0.0, -LambdaS.QM.splitJ], [-LambdaS.QM.splitJ, 0.0]] LambdaS.QM.St LambdaS.QM.En

def LambdaS.QM.statePlus : Val Float Examples.Base Examples.Dim

The symmetric eigenstate (|1⟩ + |2⟩)/√2, eigenvalue −A.

Equations

• LambdaS.QM.statePlus = LambdaS.Val.vector [0.7071067811865476, 0.7071067811865476] LambdaS.QM.St

def LambdaS.QM.stateMinus : Val Float Examples.Base Examples.Dim

The antisymmetric eigenstate (|1⟩ − |2⟩)/√2, eigenvalue +A.

Equations

• LambdaS.QM.stateMinus = LambdaS.Val.vector [0.7071067811865476, -0.7071067811865476] LambdaS.QM.St

Literals, and where parametricity draws its line

The introduction forms of LambdaS.Syntax let the eigenstate be written down rather than supplied: its amplitudes are dimensionless literals, so the state literal is parametric. A Hamiltonian literal is not: its entries are energies, so each is a multiple of 1_J, and writing the operator down names the joule, which is precisely the unit constant the parametric fragment excludes (LambdaS.Fundamental). That is why this file supplies H and ψ through the environment above.

@[reducible, inline]

abbrev LambdaS.QM.invSqrt2 : ℚ

1/√2, to sixteen places.

Equations

• LambdaS.QM.invSqrt2 = 7071067811865476 / 10 ^ 16

def LambdaS.QM.statePlusTm : Examples.Term₀

The symmetric eigenstate (|1⟩ + |2⟩)/√2 as a vector literal.

Equations

• LambdaS.QM.statePlusTm = (LambdaS.Tm.lit LambdaS.QM.invSqrt2).vcons ((LambdaS.Tm.lit LambdaS.QM.invSqrt2).vcons LambdaS.Tm.vnil)

def LambdaS.QM.hamiltonianTm : Examples.Term₀

H = [[0, −A], [−A, 0]] as a matrix literal, entry by entry a multiple of 1_J.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.QM.runIn (ρ : List (Val Float Examples.Base Examples.Dim)) (e : Examples.Term₀) : Option Float

Evaluate a scalar term in an environment.

Equations

• LambdaS.QM.runIn ρ e = match LambdaS.evalC (fun (x x_1 : LambdaS.UExp LambdaS.Examples.Base 0) => 1.0) 1000 ρ e with | some (LambdaS.Val.scalar x) => some x.mag | x => none

def LambdaS.QM.runFuel (n : ℕ) (ρ : List (Val Float Examples.Base Examples.Dim)) (e : Examples.Term₀) : Option Float

The same with an explicit fuel bound, so exhaustion is observable.

Equations

• LambdaS.QM.runFuel n ρ e = match LambdaS.evalC (fun (x x_1 : LambdaS.UExp LambdaS.Examples.Base 0) => 1.0) n ρ e with | some (LambdaS.Val.scalar x) => some x.mag | x => none

Dimensionless phase

Not evaluated: the point is the type. exp demands a dimensionless argument, so a phase A·t/ħ typechecks only because the units of an energy, a time and an action cancel. Get the Hamiltonian's units wrong and the program does not compile.

def LambdaS.QM.splitting : Examples.Term₀

Equations

• LambdaS.QM.splitting = LambdaS.QM.qty (1602176634 / 10 ^ 32) LambdaS.QM.joule

def LambdaS.QM.elapsed : Examples.Term₀

Equations

• LambdaS.QM.elapsed = LambdaS.QM.qty (1 / 10 ^ 11) LambdaS.Examples.sec

def LambdaS.QM.phase : Examples.Term₀

A·t/ħ. Dimensionless, and the checker says so.

Equations

• LambdaS.QM.phase = (LambdaS.Tm.mul LambdaS.QM.splitting LambdaS.QM.elapsed).div LambdaS.QM.hbar

Higher order: the expectation as a reusable function

expectH is written against two specific free variables. Abstracting it is where eval needs closures, and closure bodies are not subterms of the applications that invoke them, so evaluation carries a fuel bound. Fuel is consumed only at app, so first-order arithmetic evaluates at every bound including zero.

def LambdaS.QM.expectation : Examples.Term₀

λ(H : St ⊸ En). λ(ψ : vec St). ⟨ψ|H|ψ⟩

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.QM.applied : Examples.Term₀

Applied to the operator and state supplied in the environment.

Equations

• LambdaS.QM.applied = (LambdaS.Tm.app LambdaS.QM.expectation (LambdaS.Tm.var 0)).app (LambdaS.Tm.var 1)

def LambdaS.QM.twoStateChecks : Bool

Every numeric claim about the two-state system, checked in one place so the compiled binary can report whether they all hold.

Equations

• One or more equations did not get rendered due to their size.

Validation in the compiled binary

The box results are #guarded at build time in Lean's interpreter; the binary re-runs them on the compiled evaluator, so the C code path is validated against the same numbers. The literal check is new coverage: the expectation applied to the Hamiltonian and state written as terms, so the evaluator's vcons/mcons cases and the extern dgemv are all on the path of one closed program.

def LambdaS.QM.boxChecks : Bool

The particle-in-a-box claims, re-checked by the compiled evaluator, plus the undefined point (-8)^(1/3), which the compiled evaluator answers with NaN rather than a conventional number.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.QM.expectFromLiterals : Examples.Term₀

⟨ψ|H|ψ⟩ as one closed term: curried expectation, literal operator, literal state.

Equations

• LambdaS.QM.expectFromLiterals = (LambdaS.Tm.app LambdaS.QM.expectation LambdaS.QM.hamiltonianTm).app LambdaS.QM.statePlusTm

def LambdaS.QM.literalChecks : Bool

The literal program computes the symmetric eigenvalue −A through dgemv.

Equations

• LambdaS.QM.literalChecks = Option.any (fun (x : Float) => decide ((x - -LambdaS.QM.splitJ).abs < 1e-28)) (LambdaS.QM.runIn [] LambdaS.QM.expectFromLiterals)

def LambdaS.QM.boundaryChecks : Bool

The carrier-boundary conventions, asserted through the Num instance the evaluator actually uses, so a platform or libm change cannot shift them silently. Every undefined point of the classical operations behaves as IEEE: division by zero and log 0 give infinities, 0^q at negative q gives an infinity, and a non-integer power of a negative base gives NaN (the same point, checked through the evaluator, is negBase in boxChecks).

Equations

• LambdaS.QM.boundaryChecks = ((LambdaS.Num.div 1.0 0.0).isInf && (LambdaS.Num.nlog 0.0).isInf && (LambdaS.Num.npow (-1) 0.0).isInf && (LambdaS.Num.npow (1 / 3) (-8.0)).isNaN)

def LambdaS.QM.allChecks : Bool

Every run-time numeric check the binary performs; main exits nonzero unless this holds.

Equations

• LambdaS.QM.allChecks = (LambdaS.QM.boxChecks && LambdaS.QM.twoStateChecks && LambdaS.QM.literalChecks && LambdaS.QM.boundaryChecks)

def LambdaS.QM.checksReport : String

The validation summary the binary prints.

The native kernel on the evaluation path

Num.matVec is what eval reaches when it applies a linear map, and the Float carrier overrides it with a single dgemv, which is @[extern]. So in the compiled binary this runs in C, on a flat array of doubles, with no unit information present, because the checker has already discharged all of it.

def LambdaS.QM.twoStateReport : String