Which conversion factors declarations determine

Consistency (LambdaS.Declare) asks whether some valuation satisfies the declarations. Execution needs to know which conversion factors are the same in every satisfying valuation; such a ratio is Determined.

The answer is linear algebra over ℚ. ratioSpan ds is the ℚ-span of the declared ratios' exponent vectors. A ratio in the span is determined, because log-magnitude is linear in the exponent vector and every satisfying valuation agrees on the declared ratios (determined_of_mem_ratioSpan). For a consistent set the converse holds too: outside the span, a rational linear functional that vanishes on the span but not on the ratio can be added to a satisfying valuation, changing the ratio's factor while keeping every declaration satisfied (determined_iff_mem_span). determined_iff_coefficients restates span membership as a finite rational linear system; Section 3 of our paper cites it, and DeclSolver.factorCoefficients solves it.

The Completeness section proves the linear algebra behind the global check in LambdaS.DeclarationComplete. When the declared vectors are annihilated by the dimension rows, they span the rows' common kernel exactly when they and the rows together span the whole unit space (span_sup_rows_eq_top_iff, combined_span_eq_top_iff). Spanning the whole space is decided one standard basis vector at a time (span_eq_top_iff_basis_coefficients).

def LambdaS.Decl.Determined {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} (ds : Fin n → Decl B) (r : UExp B 0) : Prop

A ratio is determined when every satisfying valuation gives it the same factor.

Equations

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

def LambdaS.Decl.ratioSpan {B : Type} [DecidableEq B] {n : ℕ} (ds : Fin n → Decl B) : Submodule ℚ (B → ℚ)

The ℚ-span of the declared ratios' exponent vectors, a subspace of B → ℚ. For a consistent set, its members are exactly the ratios whose factors the declarations determine (determined_iff_mem_span).

Equations

• LambdaS.Decl.ratioSpan ds = Submodule.span ℚ (Set.range fun (i : Fin n) => (ds i).ratio.base)

theorem LambdaS.Decl.mem_ratioSpan_iff_coefficients {B : Type} [DecidableEq B] {n : ℕ} (ds : Fin n → Decl B) (r : UExp B 0) : r.base ∈ ratioSpan ds ↔ ∃ (c : Fin n → ℚ), ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = r.base b

Membership in the declared span is a finite system of rational equations.

theorem LambdaS.Decl.determined_of_mem_ratioSpan {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} {r : UExp B 0} (hr : r.base ∈ ratioSpan ds) : Determined ds r

Span membership suffices. If a ratio's exponent vector lies in ratioSpan ds, every satisfying valuation gives it the same factor: log-magnitude is linear in the exponent vector, and satisfying valuations agree on each declared ratio. No consistency hypothesis is needed.

theorem LambdaS.Decl.determined_iff_mem_span {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} (hconsistent : ∃ (V : Scaling B 0), ∀ (i : Fin n), Satisfies V (ds i)) (r : UExp B 0) : Determined ds r ↔ r.base ∈ ratioSpan ds

Determinacy is span membership. For a consistent declaration set, a ratio is Determined exactly when its exponent vector lies in ratioSpan ds. Outside the span, a rational linear functional that vanishes on the span but not on the ratio is added to a satisfying valuation; every declaration stays satisfied and the ratio's factor changes. The consistency hypothesis is needed for this direction: with no satisfying valuation, every ratio is Determined vacuously.

theorem LambdaS.Decl.determined_iff_coefficients {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {ds : Fin n → Decl B} (hconsistent : ∃ (V : Scaling B 0), ∀ (i : Fin n), Satisfies V (ds i)) (r : UExp B 0) : Determined ds r ↔ ∃ (c : Fin n → ℚ), ∀ (b : B), ∑ i : Fin n, c i * (ds i).ratio.base b = r.base b

Determinacy as a rational linear system. For a consistent declaration set, a ratio is Determined exactly when rational coefficients c express its exponent vector as a combination of the declared ratios. This is the system DeclSolver.factorCoefficients solves; Section 3 of our paper cites this theorem.

theorem LambdaS.Decl.span_sup_rows_eq_top_iff {B : Type} [Fintype B] [DecidableEq B] {D : Type} (S : Submodule ℚ (B → ℚ)) (rows : D → B → ℚ) (hsound : ∀ x ∈ S, ∀ (d : D), ∑ b : B, rows d b * x b = 0) : S ⊔ Submodule.span ℚ (Set.range rows) = ⊤ ↔ ∀ (x : B → ℚ), (∀ (d : D), ∑ b : B, rows d b * x b = 0) → x ∈ S

A kernel-basis-free completeness test. If every vector of the subspace S is annihilated by all dimension rows, then S is the whole common kernel of those rows exactly when S together with the rows spans the whole unit space.

theorem LambdaS.Decl.span_eq_top_iff_basis_coefficients {B : Type} [Fintype B] [DecidableEq B] {ι : Type} [Fintype ι] (vectors : ι → B → ℚ) : Submodule.span ℚ (Set.range vectors) = ⊤ ↔ ∀ (b : B), ∃ (c : ι → ℚ), ∀ (a : B), ∑ i : ι, c i * vectors i a = Pi.single b 1 a

Spanning the whole unit space is equivalent to solving for each standard basis vector. This is a finite family of ordinary rational linear systems.

theorem LambdaS.Decl.combined_span_eq_top_iff {B : Type} [Fintype B] [DecidableEq B] {n : ℕ} {D : Type} (vectors : Fin n → B → ℚ) (rows : D → B → ℚ) (hsound : ∀ (i : Fin n) (d : D), ∑ b : B, rows d b * vectors i b = 0) : Submodule.span ℚ (Set.range (Sum.elim vectors rows)) = ⊤ ↔ ∀ (x : B → ℚ), (∀ (d : D), ∑ b : B, rows d b * x b = 0) → x ∈ Submodule.span ℚ (Set.range vectors)

The concrete combined-column completeness criterion. Soundness says that every declaration vector is annihilated by every dimension row.