FinitePowerSeries: mathematical reading route
Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.
- A finite real power series
- The closed formula for every derivative order
- An absolute coefficient budget
- Finite power series are smooth
- The iterated derivative is the descending-factorial sum
- Signed derivative budgets on the unit interval
- A fourth-order composition budget
Samplinglib mathematical lesson
A finite real power series
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeries · def · Teaching coverage
Read this first
Mathematical statement
A finite set of natural exponents and arbitrary real coefficients define a polynomial by summing the supported monomials.
\[P(u)=\sum_{j\in S}a_j u^j\]
Lean statement · finitePowerSeries
Lean records the support, coefficient family, and evaluation point explicitly.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeries (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ
Exact module and namespace context
Proof roadmap
- 1Build the finite sum
Evaluate a_j u^j for every supported exponent and add the results. No convergence hypothesis is needed because the support is finite.
Full assumptions and notation
All objects and hypotheses
- S is finite.
- Coefficients may have any signs.
- u is real.
Construction and meaning
1. Build the finite sum
Evaluate a_j u^j for every supported exponent and add the results. No convergence hypothesis is needed because the support is finite.
\[P(u)=\sum_{j\in S}a_j u^j\]
Corresponding Lean step
The definition is a Finset.sum.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · finitePowerSeries
This is the complete construction, rather than a proof of another claim.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeries (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ :=
∑ j ∈ support, a j * u ^ j
Exact module and namespace context
Scope and omitted-condition boundaries
- No canonical support or infinite-series statement is asserted.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
The closed formula for every derivative order
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeriesDerivative · def · Teaching coverage
Read this first
Mathematical statement
The order-r derivative expression weights u^(j-r) by the descending factorial j^(r) and the original coefficient.
\[P_r(u)=\sum_{j\in S}j^{\underline r}a_j u^{j-r}\]
Lean statement · finitePowerSeriesDerivative
The order is explicit and the result is real-valued.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeriesDerivative
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ
Exact module and namespace context
Proof roadmap
- 1Differentiate each monomial formally
The r-th derivative of u^j is j falling r times u^(j-r), including the zero case j<r.
Full assumptions and notation
All objects and hypotheses
- r and j are natural numbers.
- Natural subtraction is truncated.
- When j<r, the descending factorial is zero.
Construction and meaning
1. Differentiate each monomial formally
The r-th derivative of u^j is j falling r times u^(j-r), including the zero case j<r.
\[D^r(u^j)=j^{\underline r}u^{j-r}\]
Corresponding Lean step
Nat.descFactorial handles all orders uniformly.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · finitePowerSeriesDerivative
The later theorem identifies this expression with Mathlib's actual iterated derivative.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeriesDerivative
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) : ℝ :=
∑ j ∈ support,
(j.descFactorial order : ℝ) * a j * u ^ (j - order)
Exact module and namespace context
Scope and omitted-condition boundaries
- This definition alone does not assert differentiability.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
An absolute coefficient budget
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeriesDerivativeMass · def · Teaching coverage
Read this first
Mathematical statement
Replace each coefficient by its absolute value and retain the derivative's descending-factorial weight.
\[M_r=\sum_{j\in S}j^{\underline r}|a_j|\]
Lean statement · finitePowerSeriesDerivativeMass
The mass depends on order, support, and coefficients, but not u.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeriesDerivativeMass
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) : ℝ
Exact module and namespace context
Proof roadmap
- 1Discard cancellation
Summing absolute coefficient contributions produces a point-independent majorant.
Full assumptions and notation
All objects and hypotheses
- The support is finite.
- No coefficient sign condition is used.
- Every summand is nonnegative.
Construction and meaning
1. Discard cancellation
Summing absolute coefficient contributions produces a point-independent majorant.
\[M_r=\sum_{j\in S}j^{\underline r}|a_j|\]
Corresponding Lean step
The definition is a finite sum of nonnegative real terms.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean construction · finitePowerSeriesDerivativeMass
It is designed to pair with the hypothesis |u|≤1.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
def finitePowerSeriesDerivativeMass
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) : ℝ :=
∑ j ∈ support, (j.descFactorial order : ℝ) * |a j|
Exact module and namespace context
Scope and omitted-condition boundaries
- The budget need not be sharp.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
Finite power series are smooth
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.finitePowerSeries_contDiff · theorem · Teaching coverage
Read this first
Mathematical statement
Every finite real power series is continuously differentiable to all finite orders.
\[P\in C^\infty(\mathbb R;\mathbb R)\]
Lean statement · finitePowerSeries_contDiff
The conclusion is Mathlib's `ContDiff ℝ ⊤`.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem finitePowerSeries_contDiff
(support : Finset ℕ) (a : ℕ → ℝ) :
ContDiff ℝ ⊤ (finitePowerSeries support a)
Exact module and namespace context
Proof roadmap
- 1Use closure of smooth functions
Each monomial is smooth; constant multiples and finite sums preserve smoothness.
Full assumptions and notation
All objects and hypotheses
- The exponent support is finite.
- Coefficients are arbitrary reals.
Mathematical proof
1. Use closure of smooth functions
Each monomial is smooth; constant multiples and finite sums preserve smoothness.
\[P=\sum_{j\in S}(u\mapsto a_j u^j)\in C^\infty\]
Corresponding Lean step
After unfolding the definition, fun_prop applies Mathlib's closure rules.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · finitePowerSeries_contDiff
The proof uses only standard smoothness rules.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem finitePowerSeries_contDiff
(support : Finset ℕ) (a : ℕ → ℝ) :
ContDiff ℝ ⊤ (finitePowerSeries support a) := by
unfold finitePowerSeries
fun_prop
Exact module and namespace context
Scope and omitted-condition boundaries
- No infinite-series analyticity claim is made.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
The iterated derivative is the descending-factorial sum
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.iteratedDeriv_finitePowerSeries · theorem · Teaching coverage
Read this first
Mathematical statement
For every order and point, Mathlib's iterated derivative of the finite series equals the closed polynomial derivative formula.
\[\operatorname{iteratedDeriv}_rP(u)=\sum_{j\in S}j^{\underline r}a_j u^{j-r}\]
Lean statement · iteratedDeriv_finitePowerSeries
This identifies an actual Mathlib derivative, not a merely formal polynomial.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem iteratedDeriv_finitePowerSeries
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) :
iteratedDeriv order (finitePowerSeries support a) u =
finitePowerSeriesDerivative order support a u
Exact module and namespace context
Proof roadmap
- 1Commute derivative and finite sum
Smoothness lets the iterated derivative distribute over all supported monomials.
- 2Use Mathlib's monomial formula
Each term contributes the descending factorial and lowered exponent.
Full assumptions and notation
All objects and hypotheses
- r is any natural order.
- u is any real point.
- The support is finite.
Mathematical proof
1. Commute derivative and finite sum
Smoothness lets the iterated derivative distribute over all supported monomials.
\[D^r\!\left(\sum_j a_j u^j\right)=\sum_j D^r(a_j u^j)\]
Corresponding Lean step
iteratedDeriv_fun_sum supplies the finite-sum rule.
2. Use Mathlib's monomial formula
Each term contributes the descending factorial and lowered exponent.
\[D^r(a_j u^j)=a_jj^{\underline r}u^{j-r}\]
Corresponding Lean step
iteratedDeriv_pow gives the exact monomial derivative; ring normalization matches the public definition.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · iteratedDeriv_finitePowerSeries
The proof reuses Mathlib's finite-sum and power derivative APIs.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem iteratedDeriv_finitePowerSeries
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) (u : ℝ) :
iteratedDeriv order (finitePowerSeries support a) u =
finitePowerSeriesDerivative order support a u := by
unfold finitePowerSeries finitePowerSeriesDerivative
rw [iteratedDeriv_fun_sum]
· apply Finset.sum_congr rfl
intro j hj
simp [iteratedDeriv_pow]
ring
· intro j hj
fun_prop
Exact module and namespace context
Scope and omitted-condition boundaries
- Only scalar real polynomials are covered.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
Signed derivative budgets on the unit interval
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.abs_iteratedDeriv_finitePowerSeries_le_mass · theorem · Teaching coverage
Read this first
Mathematical statement
On |u|≤1, every iterated derivative is bounded by its weighted absolute coefficient mass.
\[|u|\le1\Longrightarrow |P^{(r)}(u)|\le M_r\]
Lean statement · abs_iteratedDeriv_finitePowerSeries_le_mass
Low degrees and coefficient signs remain inside the theorem.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem abs_iteratedDeriv_finitePowerSeries_le_mass
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) {u : ℝ}
(hu : |u| ≤ 1) :
|iteratedDeriv order (finitePowerSeries support a) u| ≤
finitePowerSeriesDerivativeMass order support a
Exact module and namespace context
Proof roadmap
- 1Insert the exact derivative
Rewrite the actual derivative as the descending-factorial finite sum.
- 2Apply the triangle inequality
Discard cancellation and split absolute values across products.
- 3Use |u|≤1
Every remaining power is at most one.
Full assumptions and notation
All objects and hypotheses
- u lies in [-1,1].
- The derivative order is arbitrary.
- Coefficients may have arbitrary signs.
Mathematical proof
1. Insert the exact derivative
Rewrite the actual derivative as the descending-factorial finite sum.
\[P^{(r)}(u)=\sum_j j^{\underline r}a_j u^{j-r}\]
Corresponding Lean step
Use iteratedDeriv_finitePowerSeries.
2. Apply the triangle inequality
Discard cancellation and split absolute values across products.
\[|P^{(r)}(u)|\le\sum_j j^{\underline r}|a_j||u|^{j-r}\]
Corresponding Lean step
Finset.abs_sum_le_sum_abs proves the finite-sum bound.
3. Use |u|≤1
Every remaining power is at most one.
\[|u|^{j-r}\le1\Longrightarrow |P^{(r)}(u)|\le M_r\]
Corresponding Lean step
pow_le_one₀ completes the comparison.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · abs_iteratedDeriv_finitePowerSeries_le_mass
The proof combines the exact derivative identity with elementary absolute-value estimates.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem abs_iteratedDeriv_finitePowerSeries_le_mass
(order : ℕ) (support : Finset ℕ) (a : ℕ → ℝ) {u : ℝ}
(hu : |u| ≤ 1) :
|iteratedDeriv order (finitePowerSeries support a) u| ≤
finitePowerSeriesDerivativeMass order support a := by
rw [iteratedDeriv_finitePowerSeries]
unfold finitePowerSeriesDerivative finitePowerSeriesDerivativeMass
calc
|∑ j ∈ support,
(j.descFactorial order : ℝ) * a j * u ^ (j - order)| ≤
∑ j ∈ support,
|(j.descFactorial order : ℝ) * a j * u ^ (j - order)| :=
Finset.abs_sum_le_sum_abs _ _
_ = ∑ j ∈ support,
(j.descFactorial order : ℝ) * |a j| * |u| ^ (j - order) := by
apply Finset.sum_congr rfl
intro j hj
rw [abs_mul, abs_mul, abs_pow,
abs_of_nonneg (show 0 ≤ (j.descFactorial order : ℝ) by positivity)]
_ ≤ ∑ j ∈ support, (j.descFactorial order : ℝ) * |a j| := by
apply Finset.sum_le_sum
intro j hj
exact mul_le_of_le_one_right
(mul_nonneg (by positivity) (abs_nonneg (a j)))
(pow_le_one₀ (abs_nonneg u) hu)
Exact module and namespace context
Scope and omitted-condition boundaries
- Outside [-1,1], a radius-dependent budget is needed.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.
Samplinglib mathematical lesson
A fourth-order composition budget
AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries.fourthOrderCompositionExpression_abs_le · theorem · Teaching coverage
Read this first
Mathematical statement
Bounds on the first four outer derivatives control the exact five-term scalar fourth-order chain-rule expression.
\[|k_4u_1^4+6k_3u_1^2u_2+3k_2u_2^2+4k_2u_1u_3+k_1u_4|\le A_4|u_1|^4+6A_3|u_1|^2|u_2|+3A_2|u_2|^2+4A_2|u_1||u_3|+A_1|u_4|\]
Lean statement · fourthOrderCompositionExpression_abs_le
The numerical coefficients are explicit rather than hidden in a generic constant.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem fourthOrderCompositionExpression_abs_le
{k1 k2 k3 k4 u1 u2 u3 u4 A1 A2 A3 A4 : ℝ}
(hk1 : |k1| ≤ A1) (hk2 : |k2| ≤ A2)
(hk3 : |k3| ≤ A3) (hk4 : |k4| ≤ A4) :
|k4 * u1 ^ (4 : ℕ) +
6 * k3 * u1 ^ (2 : ℕ) * u2 +
3 * k2 * u2 ^ (2 : ℕ) +
4 * k2 * u1 * u3 + k1 * u4| ≤
A4 * |u1| ^ (4 : ℕ) +
6 * A3 * |u1| ^ (2 : ℕ) * |u2| +
3 * A2 * |u2| ^ (2 : ℕ) +
4 * A2 * |u1| * |u3| + A1 * |u4|
Exact module and namespace context
Proof roadmap
- 1Split the five terms
The coefficients 1,6,3,4,1 are the exact one-dimensional fourth-order chain-rule coefficients.
- 2Bound each term
Apply the triangle inequality and then substitute |k_i|≤A_i.
Full assumptions and notation
All objects and hypotheses
- |k_i|≤A_i for i=1,2,3,4.
- The inner derivative values are arbitrary reals.
- No sign assumption is used.
Mathematical proof
1. Split the five terms
The coefficients 1,6,3,4,1 are the exact one-dimensional fourth-order chain-rule coefficients.
\[t_1=k_4u_1^4,\ldots,t_5=k_1u_4\]
Corresponding Lean step
The proof names the five summands.
2. Bound each term
Apply the triangle inequality and then substitute |k_i|≤A_i.
\[|\sum_i t_i|\le\sum_i|t_i|\le\text{displayed majorant}\]
Corresponding Lean step
abs_add_le, abs_mul, and monotone multiplication give the result.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · fourthOrderCompositionExpression_abs_le
This is a scalar inequality; Mathlib's chain rule can identify the derivative values separately.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem fourthOrderCompositionExpression_abs_le
{k1 k2 k3 k4 u1 u2 u3 u4 A1 A2 A3 A4 : ℝ}
(hk1 : |k1| ≤ A1) (hk2 : |k2| ≤ A2)
(hk3 : |k3| ≤ A3) (hk4 : |k4| ≤ A4) :
|k4 * u1 ^ (4 : ℕ) +
6 * k3 * u1 ^ (2 : ℕ) * u2 +
3 * k2 * u2 ^ (2 : ℕ) +
4 * k2 * u1 * u3 + k1 * u4| ≤
A4 * |u1| ^ (4 : ℕ) +
6 * A3 * |u1| ^ (2 : ℕ) * |u2| +
3 * A2 * |u2| ^ (2 : ℕ) +
4 * A2 * |u1| * |u3| + A1 * |u4| := by
let t1 := k4 * u1 ^ (4 : ℕ)
let t2 := 6 * k3 * u1 ^ (2 : ℕ) * u2
let t3 := 3 * k2 * u2 ^ (2 : ℕ)
let t4 := 4 * k2 * u1 * u3
let t5 := k1 * u4
have htri : |t1 + t2 + t3 + t4 + t5| ≤
|t1| + |t2| + |t3| + |t4| + |t5| := by
calc
|t1 + t2 + t3 + t4 + t5| ≤ |t1 + t2 + t3 + t4| + |t5| :=
abs_add_le _ _
_ ≤ (|t1 + t2 + t3| + |t4|) + |t5| := by
gcongr
exact abs_add_le _ _
_ ≤ ((|t1 + t2| + |t3|) + |t4|) + |t5| := by
gcongr
exact abs_add_le _ _
_ ≤ (((|t1| + |t2|) + |t3|) + |t4|) + |t5| := by
gcongr
exact abs_add_le _ _
have ht1 : |t1| ≤ A4 * |u1| ^ (4 : ℕ) := by
dsimp [t1]
rw [abs_mul, abs_pow]
exact mul_le_mul_of_nonneg_right hk4 (by positivity)
have ht2 : |t2| ≤ 6 * A3 * |u1| ^ (2 : ℕ) * |u2| := by
dsimp [t2]
rw [abs_mul, abs_mul, abs_mul, abs_pow]
norm_num
gcongr
have ht3 : |t3| ≤ 3 * A2 * |u2| ^ (2 : ℕ) := by
dsimp [t3]
rw [abs_mul, abs_mul, abs_pow]
norm_num
gcongr
have ht4 : |t4| ≤ 4 * A2 * |u1| * |u3| := by
dsimp [t4]
rw [abs_mul, abs_mul, abs_mul]
norm_num
gcongr
have ht5 : |t5| ≤ A1 * |u4| := by
dsimp [t5]
rw [abs_mul]
exact mul_le_mul_of_nonneg_right hk1 (abs_nonneg _)
dsimp [t1, t2, t3, t4, t5] at htri
linarith
end AutoSamplingTheory.TechnicalLemmas.Analysis.FinitePowerSeries
Exact module and namespace context
Scope and omitted-condition boundaries
- It does not itself prove differentiability of a particular composition.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.