Executable declaration solving

This module is the declaration checker of Section 3 of our paper. It decides, in exact rational arithmetic, the conditions that LambdaS.Declare (consistency), LambdaS.Determinacy (which factors are fixed), and LambdaS.DeclarationComplete (whether every legal conversion is fixed) state semantically, and proves each decision sound and complete.

Three entry points, in the order a caller wants them.

• check accepts a complete certified system: the declarations are dimensionally sound, some valuation satisfies them all, and every same-dimension conversion has the same factor in every satisfying valuation. Acceptance returns the proofs as a Checked certificate, and check_isSome_iff (Theorem 3.2) proves acceptance equivalent to these three conditions.
• solve answers the weaker question of consistency alone, whether any valuation satisfies the declarations (solve_isSome_iff).
• conversionExact returns a factor as an ExactFactor, a positive rational radicand and a positive integer root degree, proved equal to V u / V v under every satisfying valuation (conversionExact_correct). For a consistent set it succeeds exactly when that factor is determined (factorCoefficients_iff_determined), and in a checked system it succeeds for every same-dimension pair (Checked.conversionExact_isSome).

DeclarationSolverExamples runs all three: disconnected feet and meters are rejected, adding foot = 0.3048 meter makes the system pass, and the dimensionless self-equation u = 2/u forces the magnitude √2, returned as radicand 2 and degree 2.

The mechanics: the solver works over explicit enumerations of the finite base-unit and base-dimension universes (enum, dims), supplied as input data rather than as a noncomputable choice of order, and reduces each declaration to one linear equation in the logarithms of the magnitudes (satisfies_valuation_iff). RationalSolver performs the elimination, and LogFactor carries the exact arithmetic that keeps it decidable.

def LambdaS.DeclSolver.matrix {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) : Matrix (Fin n) (Fin m) ℚ

The rational coefficient matrix of declaration equations.

Equations

• LambdaS.DeclSolver.matrix enum ds = Matrix.of fun (i : Fin n) (j : Fin m) => (ds i).ratio.base (enum j)

def LambdaS.DeclSolver.valuation {B : Type} {m : ℕ} (enum : Fin m ≃ B) (x : Fin m → ℝ) : Scaling B 0

The valuation whose log-magnitudes are x, indexed in the base-unit order enum supplies.

Equations

• LambdaS.DeclSolver.valuation enum x = { base := fun (b : B) => x (enum.symm b), vars := Fin.elim0 }

theorem LambdaS.DeclSolver.logScale_valuation {B : Type} [Fintype B] {m : ℕ} (enum : Fin m ≃ B) (x : Fin m → ℝ) (u : UExp B 0) : (valuation enum x).logScale u = ∑ j : Fin m, ↑(u.base (enum j)) * x j

Reindexing changes neither the unit nor its magnitude.

theorem LambdaS.DeclSolver.satisfies_valuation_iff {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (x : Fin m → ℝ) : (∀ (i : Fin n), Decl.Satisfies (valuation enum x) (ds i)) ↔ ∀ (i : Fin n), ∑ j : Fin m, matrix enum ds i j • x j = Real.log ↑(ds i).factor

Declaration satisfaction is exactly the linear system in logarithms.

theorem LambdaS.DeclSolver.valuation_coordinates {B : Type} {m : ℕ} (enum : Fin m ≃ B) (V : Scaling B 0) : (valuation enum fun (j : Fin m) => V.base (enum j)) = V

Every supplied valuation has coordinates in the explicit enumeration.

def LambdaS.DeclSolver.factorCoefficients {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (r : UExp B 0) : Option (Fin n → ℚ)

Compute rational witnesses expressing a queried ratio through declarations. Failure means the ratio is not in the ℚ-span of the declared ratios. For a consistent set that is exactly the semantic statement that the declarations leave the factor undetermined (Decl.determined_iff_coefficients); for an inconsistent set no valuation satisfies the declarations at all, so the semantic notion is vacuous and only the span statement applies.

Equations

• LambdaS.DeclSolver.factorCoefficients enum ds r = LambdaS.RationalSolver.solve (Matrix.of fun (j : Fin m) (i : Fin n) => (ds i).ratio.base (enum j)) fun (j : Fin m) => r.base (enum j)

theorem LambdaS.DeclSolver.factorCoefficients_sound {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (r : UExp B 0) {c : Fin n → ℚ} (h : factorCoefficients enum ds r = some c) (b : B) : ∑ i : Fin n, c i * (ds i).ratio.base b = r.base b

Successful factor lookup supplies an exact dependency witness.

theorem LambdaS.DeclSolver.factorCoefficients_isSome_iff {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (r : UExp B 0) : (factorCoefficients enum ds r).isSome = true ↔ ∃ (c : Fin n → ℚ), ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = r.base b

Lookup decides span membership, including failure, using exact rationals.

def LambdaS.DeclSolver.solve {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) : Option (Fin m → LogFactor)

Solve declaration equations in exact logarithmic numbers. A solution fixes free log-magnitudes to zero, but its particular choices do not determine a conversion unless the separate factor-witness check succeeds.

Equations

• LambdaS.DeclSolver.solve enum ds = LambdaS.RationalSolver.solve (LambdaS.DeclSolver.matrix enum ds) fun (i : Fin n) => LambdaS.LogFactor.ofRat (ds i).factor ⋯

theorem LambdaS.DeclSolver.solve_sound {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) {x : Fin m → LogFactor} (h : solve enum ds = some x) (i : Fin n) : Decl.Satisfies (valuation enum fun (j : Fin m) => LogFactor.interpret (x j)) (ds i)

Every returned exact solution denotes a valuation satisfying every declaration.

theorem LambdaS.DeclSolver.solve_isSome_iff {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) : (solve enum ds).isSome = true ↔ ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)

Executable solving decides existence of a real satisfying valuation. No assumption that the magnitudes or their logarithms are rational is needed.

def LambdaS.DeclSolver.factorLog {B : Type} {n : ℕ} (ds : Fin n → Decl B) (c : Fin n → ℚ) : LogFactor

Interpret the factor witness without choosing magnitudes for unconstrained units.

Equations

• LambdaS.DeclSolver.factorLog ds c = ∑ i : Fin n, c i • LambdaS.LogFactor.ofRat (ds i).factor ⋯

theorem LambdaS.DeclSolver.factorLog_correct {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} (ds : Fin n → Decl B) (r : UExp B 0) (c : Fin n → ℚ) (hc : ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = r.base b) (V : Scaling B 0) (hV : ∀ (i : Fin n), Decl.Satisfies V (ds i)) : LogFactor.interpret (factorLog ds c) = V.logScale r

A linear combination of declaration ratios fixes the same combination of log-factors.

def LambdaS.DeclSolver.conversion {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (u v : UExp B 0) : Option LogFactor

Exact conversion lookup. An unresolved ratio returns none, even if an arbitrary satisfying valuation could assign it a numerical value.

Equations

• LambdaS.DeclSolver.conversion enum ds u v = Option.map (LambdaS.DeclSolver.factorLog ds) (LambdaS.DeclSolver.factorCoefficients enum ds (LambdaS.Term.div u v))

theorem LambdaS.DeclSolver.conversion_correct {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (u v : UExp B 0) {q : LogFactor} (h : conversion enum ds u v = some q) (V : Scaling B 0) (hV : ∀ (i : Fin n), Decl.Satisfies V (ds i)) : Real.exp (LogFactor.interpret q) = conv V u v

The returned exact logarithm gives the conversion factor in every satisfying valuation.

theorem LambdaS.DeclSolver.factorCoefficients_iff_determined {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (hc : ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)) (r : UExp B 0) : (factorCoefficients enum ds r).isSome = true ↔ Decl.Determined ds r

The executable factor test is exactly semantic determinacy on consistent declarations.

theorem LambdaS.DeclSolver.conversion_isSome_iff {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (hc : ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)) (u v : UExp B 0) : (conversion enum ds u v).isSome = true ↔ Decl.Determined ds (Term.div u v)

For a consistent declaration set, conversion lookup succeeds exactly when the factor of u / v is determined, so success decides determinacy rather than producing a guess.

structure LambdaS.DeclSolver.ExactFactor : Type

An inspectable exact positive factor: the positive degree-th root of radicand.

• radicand : ℚ

  The positive rational under the root.

• degree : ℕ

  The root degree, a positive natural number.

• radicand_pos : 0 < self.radicand
• degree_pos : 0 < self.degree

@[instance_reducible]

instance LambdaS.DeclSolver.instReprExactFactor : Repr ExactFactor

Equations

• LambdaS.DeclSolver.instReprExactFactor = { reprPrec := LambdaS.DeclSolver.instReprExactFactor.repr }

def LambdaS.DeclSolver.instReprExactFactor.repr : ExactFactor → ℕ → Std.Format

Equations

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

noncomputable def LambdaS.DeclSolver.ExactFactor.value (q : ExactFactor) : ℝ

The real number the factor denotes, radicand ^ (1 / degree), written as exp (log radicand / degree). Noncomputable; constructing and comparing ExactFactor values is executable.

Equations

• q.value = Real.exp (Real.log ↑q.radicand / ↑q.degree)

def LambdaS.DeclSolver.factorExpr {B : Type} {n : ℕ} (ds : Fin n → Decl B) (c : Fin n → ℚ) : LogFactor.Expr

Preserve a finite expression so its radical representation can be inspected.

Equations

• LambdaS.DeclSolver.factorExpr ds c = List.ofFn fun (i : Fin n) => (c i, ⟨(ds i).factor, ⋯⟩)

theorem LambdaS.DeclSolver.factorExpr_eval {B : Type} {n : ℕ} (ds : Fin n → Decl B) (c : Fin n → ℚ) : LogFactor.eval (factorExpr ds c) = LogFactor.interpret (factorLog ds c)

def LambdaS.DeclSolver.exactFactor {B : Type} {n : ℕ} (ds : Fin n → Decl B) (c : Fin n → ℚ) : ExactFactor

Denominator clearing constructs a positive rational radicand and positive degree.

Equations

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

theorem LambdaS.DeclSolver.exactFactor_value {B : Type} {n : ℕ} (ds : Fin n → Decl B) (c : Fin n → ℚ) : (exactFactor ds c).value = Real.exp (LogFactor.interpret (factorLog ds c))

def LambdaS.DeclSolver.conversionExact {B : Type} [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (u v : UExp B 0) : Option ExactFactor

Return an inspectable exact radical for a determined conversion.

Equations

• LambdaS.DeclSolver.conversionExact enum ds u v = Option.map (LambdaS.DeclSolver.exactFactor ds) (LambdaS.DeclSolver.factorCoefficients enum ds (LambdaS.Term.div u v))

theorem LambdaS.DeclSolver.conversionExact_correct {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} (enum : Fin m ≃ B) (ds : Fin n → Decl B) (u v : UExp B 0) {q : ExactFactor} (h : conversionExact enum ds u v = some q) (V : Scaling B 0) (hV : ∀ (i : Fin n), Decl.Satisfies V (ds i)) : q.value = conv V u v

The extracted radical is the conversion factor in every satisfying valuation.

structure LambdaS.DeclSolver.Checked {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [UnitSys B D] {d : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) : Type

A checked unit system carries its computed solution and evidence that its declarations are sound, consistent, and determine every legal conversion.

• magnitudes : Fin m → LogFactor

  Exact log-magnitudes, in enum order, of one satisfying valuation. Free coordinates are 0; they never supply a factor.

• sound (i : Fin n) : (ds i).Sound

  Every declaration relates units of one dimension.

• solution : solve enum ds = some self.magnitudes

  magnitudes is what solve returned, so it satisfies every declaration (solve_sound).

• complete : DeclarationComplete.check enum dims ds = true

  The declared ratios and dimension rows span the unit space.

def LambdaS.DeclSolver.check {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [Fintype D] [DecidableEq D] [UnitSys B D] {d : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) : Option (Checked enum dims ds)

The declaration checker. Accepts, returning a Checked certificate, when every declaration is Decl.Sound, solve finds a solution, and DeclarationComplete.check confirms that the declared ratios and dimension rows span the unit space; returns none otherwise. check_isSome_iff characterizes acceptance.

Equations

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

theorem LambdaS.DeclSolver.Checked.consistent {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [UnitSys B D] {d : ℕ} {enum : Fin m ≃ B} {dims : Fin d ≃ D} {ds : Fin n → Decl B} (cert : Checked enum dims ds) : ∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)

Every checked system supplies a genuine satisfying valuation.

theorem LambdaS.DeclSolver.Checked.determined {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [UnitSys B D] {d : ℕ} {enum : Fin m ≃ B} {dims : Fin d ≃ D} {ds : Fin n → Decl B} (cert : Checked enum dims ds) (u v : UExp B 0) (h : SameDim (DCtx.nil D) u v) : Decl.Determined ds (Term.div u v)

Every same-dimension conversion in a checked system is determined.

theorem LambdaS.DeclSolver.check_isSome_iff {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [Fintype D] [DecidableEq D] [UnitSys B D] {d : ℕ} (enum : Fin m ≃ B) (dims : Fin d ≃ D) (ds : Fin n → Decl B) : (check enum dims ds).isSome = true ↔ (∀ (i : Fin n), (ds i).Sound) ∧ (∃ (V : Scaling B 0), ∀ (i : Fin n), Decl.Satisfies V (ds i)) ∧ ∀ (u v : UExp B 0), SameDim (DCtx.nil D) u v → Decl.Determined ds (Term.div u v)

Executable declaration checking (Theorem 3.2 of our paper). check accepts exactly when every declaration is dimensionally sound, some valuation satisfies them all, and every same-dimension pair has the same factor in every satisfying valuation. So an accepted system has these properties, and a system that has them is never rejected.

theorem LambdaS.DeclSolver.Checked.conversionExact_isSome {B : Type} [Fintype B] [DecidableEq B] {m n : ℕ} {D : Type} [UnitSys B D] {d : ℕ} {enum : Fin m ≃ B} {dims : Fin d ≃ D} {ds : Fin n → Decl B} (cert : Checked enum dims ds) (u v : UExp B 0) (h : SameDim (DCtx.nil D) u v) : (conversionExact enum ds u v).isSome = true

Factor extraction cannot fail for a legal conversion in a checked system.