Executable declaration checks at the semantic boundaries

These examples run DeclSolver.check, DeclSolver.solve, and DeclSolver.conversionExact on small unit systems chosen to separate consistency from global completeness and to exercise exact irrational output. Each namespace sets up its own UnitSys:

• Length: feet and meters with no declaration are consistent but rejected as incomplete, and foot = 0.3048 meter (link) makes the system pass, as in Section 3 of our paper; a redundant reciprocal is accepted and a conflicting factor is rejected.
• Root: the dimensionless equation u = 2/u forces the factor √2, returned as radicand 2 and degree 2.
• Unsound: a solvable declaration that equates independent dimensions is rejected.
• Empty and DependentDimensions: an empty unit system, and dimension rows that coincide.
• RadicalChain: a radical factor derived through a compound right-hand side; in an incomplete system, a determined factor is still extracted and an undetermined one is refused.
• Nanometer: the paper's wavefunction-amplitude example (exactAmplitude).

Each check is a #guard, and allChecks and report run the same computations in the native executable, which exits nonzero on failure. Length.linkedFactor_returned and Root.rootFactor_returned prove what the solver returns; Length.linkedFactor_correct and Root.rootFactor_correct prove the returned factor equal to the conversion factor in every satisfying real valuation, independently of the solver's chosen free magnitudes.

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.Length.instUnitSysFinOfNatNat : UnitSys (Fin 2) (Fin 1)

Equations

• LambdaS.DeclarationSolverExamples.Length.instUnitSysFinOfNatNat = { dim := fun (x : Fin 2) => LambdaS.Term.ofBase 0 }

def LambdaS.DeclarationSolverExamples.Length.foot : UExp (Fin 2) 0

Equations

• LambdaS.DeclarationSolverExamples.Length.foot = LambdaS.Term.ofBase 0

def LambdaS.DeclarationSolverExamples.Length.meter : UExp (Fin 2) 0

Equations

• LambdaS.DeclarationSolverExamples.Length.meter = LambdaS.Term.ofBase 1

def LambdaS.DeclarationSolverExamples.Length.link : Decl (Fin 2)

unit foot = 0.3048 meter.

Equations

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

def LambdaS.DeclarationSolverExamples.Length.reciprocal : Decl (Fin 2)

unit meter = (1250/381) foot: redundant with link, and consistent.

Equations

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

def LambdaS.DeclarationSolverExamples.Length.conflict : Decl (Fin 2)

unit foot = (1/3) meter: conflicts with link.

Equations

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

def LambdaS.DeclarationSolverExamples.Length.noDeclarations : Fin 0 → Decl (Fin 2)

Equations

• LambdaS.DeclarationSolverExamples.Length.noDeclarations = Fin.elim0

def LambdaS.DeclarationSolverExamples.Length.disconnectedConsistent : Bool

Equations

• LambdaS.DeclarationSolverExamples.Length.disconnectedConsistent = (LambdaS.DeclSolver.solve (Equiv.refl (Fin 2)) LambdaS.DeclarationSolverExamples.Length.noDeclarations).isSome

def LambdaS.DeclarationSolverExamples.Length.disconnectedRejected : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Length.disconnectedFactorRejected : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Length.linkedAccepted : Bool

Equations

• LambdaS.DeclarationSolverExamples.Length.linkedAccepted = (LambdaS.DeclSolver.check (Equiv.refl (Fin 2)) (Equiv.refl (Fin 1)) ![LambdaS.DeclarationSolverExamples.Length.link]).isSome

def LambdaS.DeclarationSolverExamples.Length.reciprocalAccepted : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Length.conflictRejected : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Length.exactLink : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Length.linkedFactor : DeclSolver.ExactFactor

Equations

• LambdaS.DeclarationSolverExamples.Length.linkedFactor = LambdaS.DeclSolver.exactFactor ![LambdaS.DeclarationSolverExamples.Length.link] ![1]

theorem LambdaS.DeclarationSolverExamples.Length.linkedFactor_returned : DeclSolver.conversionExact (Equiv.refl (Fin 2)) ![link] foot meter = some linkedFactor

conversionExact from foot to meter returns linkedFactor, the exact factor built from the coefficient witness ![1].

theorem LambdaS.DeclarationSolverExamples.Length.linkedFactor_correct (V : Scaling (Fin 2) 0) (hV : Decl.Satisfies V link) : linkedFactor.value = conv V foot meter

The returned factor equals the foot-to-meter conversion factor in every valuation satisfying link.

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.Root.instUnitSysFinOfNatNat : UnitSys (Fin 1) (Fin 0)

Equations

• LambdaS.DeclarationSolverExamples.Root.instUnitSysFinOfNatNat = { dim := fun (x : Fin 1) => LambdaS.Term.one }

def LambdaS.DeclarationSolverExamples.Root.unit : UExp (Fin 1) 0

Equations

• LambdaS.DeclarationSolverExamples.Root.unit = LambdaS.Term.ofBase 0

def LambdaS.DeclarationSolverExamples.Root.selfDecl : Decl (Fin 1)

A dimensionless generator satisfying u = 2/u has magnitude sqrt(2).

Equations

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

def LambdaS.DeclarationSolverExamples.Root.accepted : Bool

Equations

• LambdaS.DeclarationSolverExamples.Root.accepted = (LambdaS.DeclSolver.check (Equiv.refl (Fin 1)) (Equiv.refl (Fin 0)) ![LambdaS.DeclarationSolverExamples.Root.selfDecl]).isSome

def LambdaS.DeclarationSolverExamples.Root.exactRoot : Bool

Equations

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

def LambdaS.DeclarationSolverExamples.Root.rootFactor : DeclSolver.ExactFactor

Equations

• LambdaS.DeclarationSolverExamples.Root.rootFactor = LambdaS.DeclSolver.exactFactor ![LambdaS.DeclarationSolverExamples.Root.selfDecl] ![1 / 2]

theorem LambdaS.DeclarationSolverExamples.Root.rootFactor_returned : DeclSolver.conversionExact (Equiv.refl (Fin 1)) ![selfDecl] unit Term.one = some rootFactor

conversionExact from unit to the dimensionless unit returns rootFactor, the exact factor built from the coefficient witness ![1/2].

theorem LambdaS.DeclarationSolverExamples.Root.rootFactor_correct (V : Scaling (Fin 1) 0) (hV : Decl.Satisfies V selfDecl) : rootFactor.value = conv V unit Term.one

The returned factor equals the conversion factor from unit to 1 in every valuation satisfying selfDecl.

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.Unsound.instUnitSysFinOfNatNat : UnitSys (Fin 2) (Fin 2)

Equations

• LambdaS.DeclarationSolverExamples.Unsound.instUnitSysFinOfNatNat = { dim := fun (b : Fin 2) => LambdaS.Term.ofBase b }

def LambdaS.DeclarationSolverExamples.Unsound.rejected : Bool

The equations have a solution, but equating independent dimensions is illegal.

Equations

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

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.Empty.instUnitSysFinOfNatNat : UnitSys (Fin 0) (Fin 0)

Equations

• LambdaS.DeclarationSolverExamples.Empty.instUnitSysFinOfNatNat = { dim := Fin.elim0 }

def LambdaS.DeclarationSolverExamples.Empty.accepted : Bool

Equations

• LambdaS.DeclarationSolverExamples.Empty.accepted = (LambdaS.DeclSolver.check (Equiv.refl (Fin 0)) (Equiv.refl (Fin 0)) fun (i : Fin 0) => i.elim0).isSome

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.DependentDimensions.instUnitSysFinOfNatNat : UnitSys (Fin 2) (Fin 2)

Equations

• LambdaS.DeclarationSolverExamples.DependentDimensions.instUnitSysFinOfNatNat = { dim := fun (x : Fin 2) => (LambdaS.Term.ofBase 0).mul (LambdaS.Term.ofBase 1) }

def LambdaS.DeclarationSolverExamples.DependentDimensions.accepted : Bool

Both dimension rows coincide; a declaration still fixes the only unit ratio.

Equations

• LambdaS.DeclarationSolverExamples.DependentDimensions.accepted = (LambdaS.DeclSolver.check (Equiv.refl (Fin 2)) (Equiv.refl (Fin 2)) ![LambdaS.DeclarationSolverExamples.Length.link]).isSome

Three length units linked through a compound rational-power right-hand side, so that the radical a conversion needs is derived rather than declared.

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.RadicalChain.instUnitSysFinOfNatNat : UnitSys (Fin 3) (Fin 1)

Equations

• LambdaS.DeclarationSolverExamples.RadicalChain.instUnitSysFinOfNatNat = { dim := fun (x : Fin 3) => LambdaS.Term.ofBase 0 }

def LambdaS.DeclarationSolverExamples.RadicalChain.a : UExp (Fin 3) 0

Equations

• LambdaS.DeclarationSolverExamples.RadicalChain.a = LambdaS.Term.ofBase 0

def LambdaS.DeclarationSolverExamples.RadicalChain.b : UExp (Fin 3) 0

Equations

• LambdaS.DeclarationSolverExamples.RadicalChain.b = LambdaS.Term.ofBase 1

def LambdaS.DeclarationSolverExamples.RadicalChain.c : UExp (Fin 3) 0

Equations

• LambdaS.DeclarationSolverExamples.RadicalChain.c = LambdaS.Term.ofBase 2

def LambdaS.DeclarationSolverExamples.RadicalChain.meanBC : UExp (Fin 3) 0

The geometric mean of b and c.

Equations

• LambdaS.DeclarationSolverExamples.RadicalChain.meanBC = (LambdaS.Term.mul LambdaS.DeclarationSolverExamples.RadicalChain.b LambdaS.DeclarationSolverExamples.RadicalChain.c).rpow (1 / 2)

def LambdaS.DeclarationSolverExamples.RadicalChain.viaMean : Decl (Fin 3)

a = 2 · (b·c)^(1/2).

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.bToC : Decl (Fin 3)

b = 2 · c.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.conflict : Decl (Fin 3)

a = 3 · c, which contradicts the other two: they force a/c = 2^(3/2).

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.chainAccepted : Bool

Both declared ratios together span the kernel of dim.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.exactAC : Bool

log(a/c) = (3/2) log 2, cleared to log 8 / 2.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.exactAB : Bool

log(a/b) = (1/2) log 2.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.conflictRejected : Bool

The contradiction is decided exactly: 2 log 3 − log 8 = log (9/8) ≠ 0.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.incompleteRejected : Bool

With viaMean alone, b/c is undetermined, so the global check rejects the system.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.determinedInIncomplete : Bool

With viaMean alone, the factor from a to meanBC, which that declaration fixes, is still extracted exactly: radicand 2, degree 1.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.undeterminedInIncomplete : Bool

With viaMean alone, the undetermined factor from a to c is refused rather than assigned the solver's free choice.

Equations

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

def LambdaS.DeclarationSolverExamples.RadicalChain.allChecks : Bool

Equations

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

A one-dimensional wavefunction amplitude carries a half-power of inverse length. A rational declared factor between nanometer and meter then yields a radical factor between the amplitude units. Section 3 of our paper cites exactAmplitude.

@[instance_reducible]

def LambdaS.DeclarationSolverExamples.Nanometer.instUnitSysFinOfNatNat : UnitSys (Fin 2) (Fin 1)

Equations

• LambdaS.DeclarationSolverExamples.Nanometer.instUnitSysFinOfNatNat = { dim := fun (x : Fin 2) => LambdaS.Term.ofBase 0 }

def LambdaS.DeclarationSolverExamples.Nanometer.nm : UExp (Fin 2) 0

Equations

• LambdaS.DeclarationSolverExamples.Nanometer.nm = LambdaS.Term.ofBase 0

def LambdaS.DeclarationSolverExamples.Nanometer.meter : UExp (Fin 2) 0

Equations

• LambdaS.DeclarationSolverExamples.Nanometer.meter = LambdaS.Term.ofBase 1

def LambdaS.DeclarationSolverExamples.Nanometer.nmDecl : Decl (Fin 2)

nm = 10^(-9) m.

Equations

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

def LambdaS.DeclarationSolverExamples.Nanometer.accepted : Bool

Equations

• LambdaS.DeclarationSolverExamples.Nanometer.accepted = (LambdaS.DeclSolver.check (Equiv.refl (Fin 2)) (Equiv.refl (Fin 1)) ![LambdaS.DeclarationSolverExamples.Nanometer.nmDecl]).isSome

def LambdaS.DeclarationSolverExamples.Nanometer.exactAmplitude : Bool

nm^(-1/2) to m^(-1/2) multiplies by 10^(9/2): radicand 10^9, degree 2.

Equations

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

def LambdaS.DeclarationSolverExamples.allChecks : Bool

All declaration regressions, also evaluated by the native artifact executable.

Equations

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

def LambdaS.DeclarationSolverExamples.report : String

A compact runtime reading identifying the declaration checks.