Glossary and notation

Read side by side

This guide explains 183 terms used in the collection and its finite examples. Use the first reading route, compare nearby ideas, browse a subject, or open the alphabetical index.

Find a glossary term on the reading website: search names, abbreviations, definitions and short examples, or choose a subject. Open the glossary beside a paper with Read side by side.

A word can have a more specific meaning in another paper. The paper’s definitions and hypotheses take precedence. Examples and source links provide context without changing any recorded evidence status.

Look up notation across the collection · Work through the calculations by hand · Papers, proofs, Lean, and code by topic · First software runs

A first reading

Follow these terms for a short route through the finite examples. Each definition links to a worked calculation.

1. Realization · Seed · Seed rank — Identify the system, the allowed action and the data that generate it.
2. Projector · Packet — See how an object splits into selected components.
3. Coordinates · Analysis and synthesis — Follow a representation from the object to coordinates and back.
4. Transfer block · Residual — Track an operation between components and check a reconstruction.

Compare nearby ideas

These distinctions use the glossary’s stated settings. Follow both entries for their definitions and examples.

Browse by subject

• Linear foundations — 26 terms
• Operators, seeds, and packets — 24 terms
• Coordinates and transfer — 15 terms
• Refinement and constraints — 21 terms
• Arithmetic and error — 13 terms
• Claims and evidence — 15 terms
• Series and cyclic functions — 11 terms
• Finite quantum systems — 13 terms
• Arithmetic and modules — 23 terms
• Dynamics, memory, and calibration — 13 terms
• Inference and probability — 9 terms

Linear foundations

The objects and notation used in the finite examples.

Scalar · Field · Vector · Vector space · Linear map · Matrix · Identity operator · Span · Linear independence · Basis · Dimension · Kernel · Image · Rank · Inner product · Norm · Subspace · Nullity · Rank–nullity identity · Injective map · Surjective map · Linear isomorphism · Direct sum · Quotient space · Determinant · Domain and codomain

Scalar

A number from the declared coefficient field, used to multiply vectors. The hand-worked matrix examples use real scalars and exact rational entries.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Field · Vector

Back to glossary lookup

Field

A number system with addition, subtraction, multiplication, and division by every nonzero element. The rational, real, and complex numbers are examples. A result over one field does not automatically hold over another.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Scalar

Back to glossary lookup

Vector

An element of a vector space. In the finite examples it is a column of numbers. Its coordinates depend on a chosen representation.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Vector space · Coordinates

Back to glossary lookup

Vector space

A collection of vectors closed under addition and scalar multiplication, with the usual distributive and associative laws. The space of pairs of real numbers is denoted R².

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Field · Span · Basis

Back to glossary lookup

Linear map

A map T satisfying T(au + bv) = aT(u) + bT(v) for all vectors u, v and allowed scalars a, b. A linear map preserves linear combinations.

Also called: Linear transformation.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Matrix · Kernel · Image

Back to glossary lookup

Matrix

A rectangular array representing a linear map after bases have been chosen. An m by n matrix takes n coordinates to m coordinates. Each output coordinate is a row multiplied by the input column.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Linear map · Basis · Composition

Back to glossary lookup

Identity operator

The map I that leaves every input unchanged, so Ix = x. The subscript in I₂ or I₃ specifies the dimension when needed.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Inverse · Complete packet family

Back to glossary lookup

Span

All finite linear combinations of a specified set of vectors. The span of the empty set consists only of the zero vector. With an operator action, one may first apply allowed operators and then take the span.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Seed · Basis · Linear independence

Back to glossary lookup

Linear independence

A family is linearly independent when the only linear combination giving zero has every coefficient zero. No member of a finite independent family can be formed from the others.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Span · Basis

Back to glossary lookup

Basis

A linearly independent spanning family. Every vector has a unique finite linear combination in that basis. Redundant measurements can describe a vector without forming a basis.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Span · Linear independence · Redundant coordinates

Back to glossary lookup

Dimension

The number of vectors in a basis of a finite-dimensional vector space. In these examples, R² has dimension two even when three redundant measurements are stored.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Basis · Rank · Seed rank

Back to glossary lookup

Kernel

For a linear map T, the vectors sent to zero: ker T = {x : Tx = 0}. A nonzero kernel describes directions that this map cannot distinguish from zero.

Also called: Nullspace, Null space.

In the worked example: For the sum map R(a,b) = a+b over R, the vector (1,−1)ᵀ lies in the kernel: R(1,−1) = 0. Adding this vector does not change the observed sum.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Image · Fiber · Factorization through a map

Back to glossary lookup

Image

The outputs actually attained by a map. For a linear map T, im T = {Tx : x is an allowed input} is a subspace of the target. The declared target can be larger than the image.

Also called: Range, Range of a linear map.

In the worked example: For A(a,b) = (a,b,a+b), the image consists of triples whose third coordinate is the sum of the first two. The coordinate vector (0,0,1)ᵀ lies outside it.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Kernel · Rank · Left inverse

Back to glossary lookup

Rank

For a finite linear map, the dimension of its image. A matrix has full column rank when its columns are linearly independent, so it has no nonzero input in its kernel.

Keep in mind: Matrix rank and seed rank answer different questions.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Dimension · Image · Seed rank

Back to glossary lookup

Inner product

For real vector spaces, a symmetric bilinear pairing with ⟨v,v⟩ > 0 for every nonzero v. It defines lengths and angles. Positive weights give the pairing sum_i w_i u_i v_i. Complex inner products use conjugate symmetry and conjugate linearity in one argument.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Norm · Orthogonal projector

Back to glossary lookup

Norm

A nonnegative measure of size that is zero only at the zero vector, scales by the absolute value of a scalar and satisfies the triangle inequality. The Euclidean norm is the square root of the sum of squared coordinates.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Inner product · Residual · Tolerance

Back to glossary lookup

Subspace

A subset of a vector space that contains zero and is closed under addition and scalar multiplication. Kernels and images of linear maps are subspaces.

Hand-worked example · Papers, proofs, Lean, and code · Kernel · Image

Back to glossary lookup

Nullity

The dimension of the kernel of a finite-dimensional linear map. It counts independent input directions erased by the map.

Hand-worked example · Papers, proofs, Lean, and code · Kernel · Dimension

Back to glossary lookup

Rank–nullity identity

For a linear map with finite-dimensional domain V, dim V = rank T + nullity T. The rank concerns the image, not the dimension of the entire declared target.

Hand-worked example · Papers, proofs, Lean, and code · Rank · Nullity

Back to glossary lookup

Injective map

A map that sends distinct inputs to distinct outputs. A linear map is injective exactly when its kernel contains only zero.

Also called: Injection, One-to-one map.

Hand-worked example · Papers, proofs, Lean, and code · Kernel · Left inverse

Back to glossary lookup

Surjective map

A map whose image is its entire declared target. Surjectivity depends on which target is specified.

Also called: Surjection, Onto map.

Hand-worked example · Papers, proofs, Lean, and code · Image · Rank

Back to glossary lookup

Linear isomorphism

A bijective linear map between vector spaces over the same field. Its inverse is linear. It preserves the vector-space structure, although lengths need not be preserved.

Also called: Invertible linear map.

Hand-worked example · Papers, proofs, Lean, and code · Inverse · Coordinate change

Back to glossary lookup

Direct sum

A decomposition into subspaces in which each vector has a unique sum of components. For two subspaces, uniqueness is equivalent to their intersection containing only zero.

Hand-worked example · Papers, proofs, Lean, and code · Subspace · Complete packet family

Back to glossary lookup

Quotient space

The vector space V/W obtained by identifying vectors whose difference lies in a subspace W. A coset x+W records the equivalence class of x.

Hand-worked example · Papers, proofs, Lean, and code · Subspace · Fiber

Back to glossary lookup

Determinant

A scalar attached to a square matrix. For [[a,b],[c,d]] it is ad − bc. Over a field, a square matrix is invertible exactly when its determinant is nonzero.

Hand-worked example · Papers, proofs, Lean, and code · Inverse · Field

Back to glossary lookup

Domain and codomain

The declared input and target spaces of a map. The codomain includes all permitted outputs, while the image consists of outputs actually attained.

Hand-worked example · Papers, proofs, Lean, and code · Image · Surjective map · Typed system

Back to glossary lookup

Operators, seeds, and packets

How an allowed action generates, selects, and decomposes objects.

Realization · Seed · Address · Projector · Packet · Typed system · Operator algebra · Seed rank · Cyclic vector · Orthogonal projector · Complete packet family · Mutual annihilation · Invariant subspace · Eigenvector · Eigenvalue · Eigenspace · Diagonalizable operator · Polynomial in an operator · Minimal polynomial · Spectral projector · Commutator · Typed path · Operator relation · Nilpotent operator

Realization

A way to represent a declared system using concrete spaces and operations while respecting its required relations. A finite matrix realization assigns a space to each type and a matrix to each permitted arrow.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Typed system · Operator algebra · Compatibility

Back to glossary lookup

Seed

Initial generating data from which the allowed operator action produces further elements. Whether a seed is sufficient depends on both the object and the declared action.

In the worked example: On R², let N(a,b) = (b,0) and v = (0,1). Then Nv = (1,0), so v and its image generate every vector by linear combinations.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Span · Seed rank · Cyclic vector

Back to glossary lookup

Address

A label for a legal operator path or a packet coordinate. Examples include signal phases, residue classes, and positions in a packet tree. An address identifies a location in a representation, not necessarily a physical location.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Typed system · Packet · Residue class

Back to glossary lookup

Projector

A linear operator P satisfying P² = P. Applying it twice has the same effect as applying it once. This algebraic definition does not require orthogonality.

Also called: Projection, Idempotent linear operator.

In the worked example: On R², P₁(a,b) = (a,0). Applying P₁ again still gives (a,0), so P₁² = P₁.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Orthogonal projector · Packet · Redundant coordinates

Back to glossary lookup

Packet

In the finite projector example, a selected component Pᵢx or the subspace in which it lies, according to context. Signal, algebraic and arithmetic works may assign the word more specific meanings.

In the worked example: For x = (2,3)ᵀ, the coordinate projectors give packets P₁x = (2,0)ᵀ and P₂x = (0,3)ᵀ. Their sum recovers x.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Projector · Complete packet family · Address

Back to glossary lookup

Typed system

A system that records which objects an operation accepts and returns. A path of operations is legal only when consecutive input and output types agree. Types are part of the mathematical specification.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Linear map · Composition · Realization

Back to glossary lookup

Operator algebra

In the finite linear setting, a collection of linear operators closed under sums, scalar multiples, and composition. When a unital algebra is intended, the identity operator is included.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Composition · Seed · Invariant subspace

Back to glossary lookup

Seed rank

In the finite linear example, the least number of seeds whose operator-generated span is the whole space. More general definitions can involve modules, dense generation, and cardinalities. Read the definition in the chosen work.

In the worked example: For N(a,b) = (b,0) on R², one seed v = (0,1) suffices. With only the zero operator and the identity, two seeds are needed on the same space.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Seed · Span · Rank

Back to glossary lookup

Cyclic vector

For a single linear operator T, a vector v is cyclic when v, Tv, T²v and further iterates span the space under consideration. One cyclic vector is enough to generate that operator module.

Also called: Cyclic seed.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Seed · Span

Back to glossary lookup

Orthogonal projector

A projector onto a subspace whose residual x − Px is perpendicular to that subspace in the specified inner product. In ordinary real Euclidean coordinates its matrix is symmetric as well as idempotent.

Keep in mind: Orthogonality depends on the inner product. Weighted averaging need not have a symmetric matrix in ordinary coordinates.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Projector · Inner product

Back to glossary lookup

Complete packet family

In these finite examples, projectors Pᵢ with PᵢPⱼ = 0 for distinct indices and sum_i Pᵢ = I. These identities decompose every vector as x = sum_i Pᵢx.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Projector · Mutual annihilation · Reconstruction

Back to glossary lookup

Mutual annihilation

The relation PᵢPⱼ = 0 whenever i and j differ. Applying one selection after a different selection gives zero. For a pair of projectors, both orders must be checked.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Projector · Complete packet family

Back to glossary lookup

Invariant subspace

A subspace W preserved by an operator T, meaning T(W) is contained in W. Preservation does not require T to act as the identity on W.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Span · Operator algebra

Back to glossary lookup

Eigenvector

A nonzero vector v for which Tv = λv. The scalar λ is the associated eigenvalue. Zero is excluded from the definition of eigenvector.

Hand-worked example · Papers, proofs, Lean, and code · Eigenvalue · Invariant subspace

Back to glossary lookup

Eigenvalue

A scalar λ such that Tv = λv for some nonzero v over the specified field. A real matrix may have no real eigenvalue even though it has eigenvalues over the complex numbers.

Hand-worked example · Papers, proofs, Lean, and code · Eigenvector · Field

Back to glossary lookup

Eigenspace

For an operator T and scalar λ, the kernel of T − λI. It includes zero and all eigenvectors with eigenvalue λ.

Hand-worked example · Papers, proofs, Lean, and code · Kernel · Eigenvector

Back to glossary lookup

Diagonalizable operator

An operator that has a basis of eigenvectors over the stated field. Equivalently, its matrix becomes diagonal after an invertible change of basis.

Hand-worked example · Papers, proofs, Lean, and code · Basis · Eigenvector · Coordinate change

Back to glossary lookup

Polynomial in an operator

Substitute T into p(t) = a₀ + a₁t + ⋯ + aₙtⁿ to obtain p(T) = a₀I + a₁T + ⋯ + aₙTⁿ. The constant term acts through the identity operator.

Hand-worked example · Papers, proofs, Lean, and code · Operator algebra · Identity operator

Back to glossary lookup

Minimal polynomial

For a linear operator on a nonzero finite-dimensional space over a field, the monic polynomial of least degree with m(T) = 0. It records an exact operator relation.

Hand-worked example · Papers, proofs, Lean, and code · Polynomial in an operator · Operator relation

Back to glossary lookup

Spectral projector

In the diagonalizable finite example, the projector onto one eigenspace along the sum of the others. Distinct eigenvalues allow a polynomial interpolation formula for these projectors.

Hand-worked example · Papers, proofs, Lean, and code · Projector · Eigenspace · Diagonalizable operator

Back to glossary lookup

Commutator

For operators on the same space, [A,B] = AB − BA. A zero commutator means the two orders of composition agree.

Hand-worked example · Papers, proofs, Lean, and code · Composition · Operator algebra

Back to glossary lookup

Typed path

A sequence of arrows in which each output type matches the next input type. Its realization is the corresponding ordered composition. An empty path at a type acts as its identity.

Hand-worked example · Papers, proofs, Lean, and code · Typed system · Composition · Identity operator

Back to glossary lookup

Operator relation

A required equality between legal operator expressions, such as T² = 0. In a typed system, both sides must have the same input and output types.

Hand-worked example · Papers, proofs, Lean, and code · Typed path · Realization · Minimal polynomial

Back to glossary lookup

Nilpotent operator

An operator N for which Nᵏ = 0 for some positive integer k. It can be nonzero. The smallest such k on a nonzero space is its nilpotency index.

Also called: Nilpotent linear map.

Hand-worked example · Papers, proofs, Lean, and code · Operator algebra · Minimal polynomial

Back to glossary lookup

Coordinates and transfer

How descriptions change and operations move between components.

Coordinates · Analysis and synthesis · Transfer block · Coordinate change · Inverse · Left inverse · Redundant coordinates · Composition · Operator conjugation · Intertwiner · Block matrix · Schur complement · Elimination · Orthogonal matrix · Normalization

Coordinates

Values describing an object relative to a chosen representation. Coordinates can be unique basis coefficients or redundant measurements, depending on the setup.

In the worked example: The coordinate change C(a,b) = (a + b/2,b) sends x = (2,3)ᵀ to y = (7/2,3)ᵀ. These describe the same object in two coordinate systems.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Basis · Coordinate change · Redundant coordinates

Back to glossary lookup

Analysis and synthesis

Analysis sends an object to coordinates. Synthesis returns an object from coordinates. In the finite model, A analyzes and S synthesizes, and exact reconstruction is the identity SA = I.

In the worked example: The analysis A(a,b) = (a,b,a+b) sends (2,3)ᵀ to (2,3,5)ᵀ. The example’s synthesis S returns (2,3)ᵀ, with SA = I₂.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Left inverse · Coordinates · Reconstruction

Back to glossary lookup

Transfer block

The part of an operation connecting a source component to a target component. With source projector Pᵢ, target projector Qⱼ and operator T, the block is QⱼTPᵢ. Complete source and target families allow the blocks to reconstruct T.

In the worked example: For T = [[1,2],[3,4]], the coordinate block P₁TP₂ sends (2,3)ᵀ to (6,0)ᵀ. It carries source coordinate 2 into target coordinate 1.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Projector · Composition · Reconstruction

Back to glossary lookup

Coordinate change

A transformation between descriptions of the same object. In the invertible linear example the convention is y = Cx, so x = C⁻¹y. Keeping track of the direction prevents inverse formulas from being swapped.

Also called: Change of coordinates.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Coordinates · Inverse · Operator conjugation

Back to glossary lookup

Inverse

A map that undoes another map in both directions. For a square invertible matrix C, the inverse satisfies C⁻¹C = CC⁻¹ = I.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Identity operator · Left inverse

Back to glossary lookup

Left inverse

For A mapping an input space to a coordinate space, S is a left inverse when SA = I on the input space. This gives exact reconstruction of analyzed inputs. It does not imply AS = I on the entire coordinate space.

In the worked example: The redundant-coordinate example has SA = I₂ but AS ≠ I₃. S recovers every original vector even though it does not invert every three-coordinate input.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Inverse · Analysis and synthesis · Image

Back to glossary lookup

Redundant coordinates

A representation containing more coordinate entries than are needed for a basis description. Valid coordinate lists can satisfy relations, such as a third measurement being the sum of the first two.

Also called: Redundant representation.

Keep in mind: The reconstruction components SEᵢA can sum to the identity without being projectors.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Basis · Analysis and synthesis · Projector

Back to glossary lookup

Composition

Applying one map after another. In a matrix product UT, T acts first and U acts second. The intermediate dimensions or types must agree.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Typed system · Matrix · Transfer block

Back to glossary lookup

Operator conjugation

The change in an operator matrix under an invertible coordinate change. With y = Cx and original operator T, the new matrix is CTC⁻¹. This usage is distinct from complex conjugation.

Also called: Similarity transformation.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Coordinate change · Intertwiner

Back to glossary lookup

Intertwiner

A linear map C connecting operators T and U by CT = UC. Applying T and then C agrees with applying C and then U. An intertwiner need not be invertible.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Operator conjugation · Commuting diagram

Back to glossary lookup

Block matrix

A matrix grouped into rectangular submatrices according to decompositions of its input and output coordinates. Block products require the inner dimensions to agree.

Hand-worked example · Papers, proofs, Lean, and code · Matrix · Transfer block

Back to glossary lookup

Schur complement

For the block matrix [[A,B],[C,D]] with invertible A, the Schur complement of A is D − CA⁻¹B. It is the remaining operator after eliminating the first block of unknowns.

Hand-worked example · Papers, proofs, Lean, and code · Block matrix · Elimination · Inverse

Back to glossary lookup

Elimination

Removing selected unknowns by solving part of a system and substituting into the remaining equations. The substitution requires its stated invertibility or solvability assumptions.

Hand-worked example · Papers, proofs, Lean, and code · Schur complement · Reconstruction

Back to glossary lookup

Orthogonal matrix

A real square matrix Q with QᵀQ = QQᵀ = I. It preserves the Euclidean inner product and norm. A transform with orthogonal rows can still need normalization to satisfy this identity.

Hand-worked example · Papers, proofs, Lean, and code · Inner product · Norm · Normalization

Back to glossary lookup

Normalization

A declared scaling convention. For a Haar pair, dividing sums and differences by two gives averages, while dividing by √2 gives a Euclidean norm-preserving transform.

Hand-worked example · Papers, proofs, Lean, and code · Haar pair · Orthogonal matrix

Back to glossary lookup

Refinement and constraints

How descriptions become finer, discard information or meet a compatibility condition.

Refinement · Obstruction · Coarsening · Polyphase decomposition · Residue class · Compatibility · Commuting diagram · Reconstruction · Fiber · Factorization through a map · Lift · Finite conditional expectation · Completion · Haar pair · Detail coefficient · Repair direction · Free linear repair · Finite repair menu · Repair selection cost · Feasibility · Linear obstruction witness

Refinement

A compatible move from a coarser description to a finer one. In finite packet refinement, each fine packet has a coarse parent and each coarse projector is the sum of its children.

In the worked example: The zero-based even indices split into residue classes 0 and 2 modulo 4. Their selectors satisfy P₀ = F₀ + F₂.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Coarsening · Compatibility · Residue class

Back to glossary lookup

Obstruction

An identified reason a requested construction cannot meet its stated conditions. In the recovery example, two inputs have the same coarse value but require different answers, so no recovery function from that value alone exists.

In the worked example: The inputs (1,0) and (0,1) have the same sum but different first coordinates. No function of their sum alone can return the first coordinate for every real input.

Keep in mind: A nonzero numerical residual is not automatically a proof that every possible construction fails.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Fiber · Factorization through a map · Residual

Back to glossary lookup

Coarsening

Passing to a description that groups or forgets distinctions. Combining fine packets can recover a coarse packet, while discarding the fine values can prevent later reconstruction.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Refinement · Obstruction · Fiber

Back to glossary lookup

Polyphase decomposition

For a sequence x and a positive integer m, the phase r collects samples x_(mk+r), with 0 ≤ r < m. Interleaving all phases reconstructs the indexed sequence. Filtering requires additional boundary and convention choices.

Also called: Polyphase splitting.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Address · Residue class · Reconstruction

Back to glossary lookup

Residue class

Integers with the same remainder modulo a positive integer m. Two integers belong to the same class when their difference is a multiple of m. Even and odd indices are the two classes modulo two.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Polyphase decomposition · Address

Back to glossary lookup

Compatibility

Agreement between specified maps, operations or levels of a construction. The relevant equality must be stated, such as a coarse projector equaling the sum of its fine children.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Commuting diagram · Refinement · Completion

Back to glossary lookup

Commuting diagram

A diagram in which the declared routes between the same starting and ending objects give the same map. In Example 3 the equality is D_y C = C D.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Composition · Compatibility · Intertwiner

Back to glossary lookup

Reconstruction

Recovering an object from its representation under the stated identities. Exact reconstruction may use all packet components or a synthesis map. Dropping components generally introduces a residual.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Analysis and synthesis · Residual · Complete packet family

Back to glossary lookup

Fiber

For a map R and an output s, the set of all inputs with R(x) = s. A proposed observation can be recovered from R(x) alone only if it is constant on each fiber.

Also called: Fibre, Preimage of a point.

In the worked example: For R(a,b) = a+b on R², the fiber over 1 consists of all (t,1−t) with real t. It contains both (1,0) and (0,1).

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Kernel · Factorization through a map

Back to glossary lookup

Factorization through a map

Writing one map F as G composed with another map R, so F(x) = G(R(x)). This means the intermediate value R(x) contains enough information for the requested output F(x).

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Fiber · Obstruction · Composition

Back to glossary lookup

Lift

An object at a finer or richer level that maps to a specified object at a coarser level. Existence, uniqueness and compatibility of lifts are separate questions.

Further reading · Refinement · Compatibility · Obstruction

Back to glossary lookup

Finite conditional expectation

For positive weights and a finite partition, replace each value by its group’s weighted mean. The resulting map fixes group-constant vectors and is an orthogonal projector in the corresponding weighted inner product.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Orthogonal projector · Inner product · Coarsening

Back to glossary lookup

Completion

A construction that adds or realizes limits or missing structure under a specified mathematical definition. There is no single universal completion operation across the collection. A finite compatible tower does not by itself construct an infinite limit.

Keep in mind: Mathematical completion and the editorial completion stage of a paper are different uses of the word.

Further reading · Compatibility · Lift

Back to glossary lookup

Haar pair

A two-sample transform that separates an average and a difference. The tutorial uses a = (u+v)/2 and d = (u−v)/2, with inverse (u,v) = (a+d,a−d). Other Haar normalizations use square roots.

Hand-worked example · Papers, proofs, Lean, and code · Detail coefficient · Normalization · Refinement

Back to glossary lookup

Detail coefficient

In the Haar pair example, the signed half-difference d = (u−v)/2. It records the information lost when the pair is replaced by its repeated average.

Hand-worked example · Papers, proofs, Lean, and code · Haar pair · Residual

Back to glossary lookup

Repair direction

An allowed vector added to the span of the original image so that a required target can become reachable. Both the target equation and the permitted coefficient system must remain specified.

Hand-worked example · Papers, proofs, Lean, and code · Image · Span · Finite repair menu

Back to glossary lookup

Free linear repair

A repair problem allowing freely chosen added directions over the declared field. In the rational finite-dimensional setting, the minimum added dimension is the dimension of the span of the target residual classes in the original cokernel.

Hand-worked example · Papers, proofs, Lean, and code · Repair direction · Cokernel · Dimension

Back to glossary lookup

Finite repair menu

A supplied finite list of candidate directions, with costs and any selection restrictions. Feasibility and optimality are judged using this list and the original target equation.

Hand-worked example · Papers, proofs, Lean, and code · Repair direction · Repair selection cost · Feasibility

Back to glossary lookup

Repair selection cost

The declared cost of the selected repair choices. In the tutorial it is the sum of their selection costs, paid once per choice, independently of the rational coefficients used to combine them.

Hand-worked example · Papers, proofs, Lean, and code · Finite repair menu · Free linear repair

Back to glossary lookup

Feasibility

Existence of a solution satisfying the stated equations and admissibility conditions. Failure of one candidate or exhaustion of a search budget does not by itself show infeasibility.

Hand-worked example · Papers, proofs, Lean, and code · Hypothesis · Obstruction · Certificate

Back to glossary lookup

Linear obstruction witness

A linear functional that annihilates every allowed direction but has a nonzero value on the required target. It proves that this target lies outside their span under the stated linear problem.

Hand-worked example · Papers, proofs, Lean, and code · Linear map · Kernel · Obstruction · Feasibility

Back to glossary lookup

Arithmetic and error

How exact values, stored approximations, and error measures differ.

Residual · Exact · Numerical · Precision · Dyadic rational · Rounding · ULP · Numerical ternary · Tolerance · Integer congruence · Coprime integers · Modular inverse · Chinese remainder theorem

Residual

A discrepancy computed for a specified identity or reconstruction. In Example 5 it is r = x − x̂. Other operations may use a different sign or norm, so the definition belongs with the reported number.

In the worked example: Dropping residue class 2 modulo 4 from (1,2,3,4,5,6,7,8) gives r = (0,0,3,0,0,0,7,0). Its squared Euclidean norm is 58.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Norm · Tolerance · Obstruction

Back to glossary lookup

Exact

Computed or stated in exact algebra or arithmetic under the declared hypotheses. Exact rational arithmetic avoids rounding of those rational values. It does not establish an unchecked modeling assumption.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Numerical · Hypothesis · Dyadic rational

Back to glossary lookup

Numerical

Computed with finite-precision arithmetic and interpreted using a stated error or residual rule. A zero observed floating-point residual does not turn the whole computation into an exact-arithmetic proof.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Exact · Residual · Tolerance

Back to glossary lookup

Precision

The capacity of a numerical representation. For the binary model here it is the number of significant binary digits, including the leading bit. More precision does not alone prove that an algorithm or its input is accurate.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Rounding · ULP · Numerical

Back to glossary lookup

Dyadic rational

A rational number expressible as an integer divided by a power of two. These are precisely the rational numbers with a finite binary expansion, apart from representation range limits.

Also called: Binary rational.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Exact · Rounding

Back to glossary lookup

Rounding

Choosing a representable stored value for an exact value according to a specified rule. Nearest, ties to even chooses the closer value and resolves an exact midpoint by the parity of the last retained significand bit.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Precision · ULP · Numerical ternary

Back to glossary lookup

ULP

A unit in the last retained place at a specified precision and exponent. In the three-bit example the spacing in [1, 2) is 1/4, while the spacing in [2, 4) is 1/2. It is not one fixed absolute distance.

Also called: Unit in the last place.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Precision · Rounding

Back to glossary lookup

Numerical ternary

A numerical return whose sign compares the stored result with the exact value under the operation’s contract. Zero means exact, negative means below and positive means above. An error sentinel is not a numerical direction.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Rounding · Exact

Back to glossary lookup

Tolerance

A declared threshold used by a numerical acceptance rule. Its units, scaling and comparison must match the residual being checked. A residual below tolerance is evidence within that rule, not exact equality in general.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Residual · Norm · Numerical

Back to glossary lookup

Integer congruence

The relation a ≡ b modulo m means m divides a − b, with m a positive integer. It compares residue classes, not the ordinary sizes of a and b.

Hand-worked example · Papers, proofs, Lean, and code · Residue class · Modular inverse

Back to glossary lookup

Coprime integers

Integers with greatest common divisor one. Pairwise coprime moduli give independent residue coordinates in the ordinary Chinese remainder theorem.

Also called: Relatively prime integers.

Hand-worked example · Papers, proofs, Lean, and code · Chinese remainder theorem · Integer congruence

Back to glossary lookup

Modular inverse

An integer b with ab ≡ 1 modulo m. For m greater than one, it exists exactly when a and m are coprime. The inverse is a residue class modulo m.

Hand-worked example · Papers, proofs, Lean, and code · Integer congruence · Coprime integers

Back to glossary lookup

Chinese remainder theorem

For pairwise coprime positive moduli, a tuple of residues specifies exactly one residue class modulo their product. Selecting an integer representative requires an additional convention.

Also called: CRT.

Hand-worked example · Papers, proofs, Lean, and code · Residue class · Coprime integers · Reconstruction

Back to glossary lookup

Claims and evidence

How to read assumptions, proofs, formal links, and computation records.

Certificate · Conditional · Lean correspondence · Hypothesis · Theorem · Proof · Heuristic · Finite check · Finite proof field · Admissible leaf · Recorded inference rule · Verification closure · Inclusion-minimal certificate · Least certificate · Minimum-cost certificate

Certificate

A structured report describing a particular check, with its evidence class, residuals, and assumptions. The producer determines what was checked. A saved certificate describes a past calculation and needs revalidation for a new one.

Further reading · How to inspect a proof · Exact · Numerical · Conditional

Back to glossary lookup

Conditional

A result that retains explicitly listed assumptions. In a computation record, some of those assumptions may not have been established by the computation. Passing its checks does not discharge them.

Further reading · How to inspect a proof · Hypothesis · Certificate · Completion

Back to glossary lookup

Lean correspondence

A recorded connection between a written claim and a formal Lean statement. Compare hypotheses, the full formal type, source edition, and execution record. A similar declaration name or a working link alone does not establish the correspondence.

Further reading · How to inspect a proof · Proof · Theorem · Certificate

Back to glossary lookup

Hypothesis

An assumption required by a statement or construction. It may describe the space, arithmetic, domain, regularity or supplied data. A conclusion applies only where its hypotheses hold.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Conditional · Theorem · Certificate

Back to glossary lookup

Theorem

A mathematical statement established by a proof from its specified assumptions. A theorem may be conditional on explicit hypotheses, even when the implication itself is fully proved.

Further reading · How to inspect a proof · Hypothesis · Proof · Conditional

Back to glossary lookup

Proof

An argument establishing a statement from its hypotheses and accepted prior results. A worked input illustrates a statement. A general identity or argument is needed to establish a claim about every allowed input.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Theorem · Finite check · Lean correspondence

Back to glossary lookup

Heuristic

A method for discovery, search or estimation without a complete guarantee for the claimed outcome. Its suggestions can lead to later proofs or checks, but the suggestions alone do not establish them.

Further reading · How to inspect a proof · Proof · Finite check

Back to glossary lookup

Finite check

A check over specified, finitely many inputs or cases. Exhaustive checking can prove a claim about that finite domain. Sampling a larger domain does not establish the universal claim without an additional argument.

Hand-worked example · Further reading · Papers, proofs, Lean, and code · Proof · Certificate · Hypothesis

Back to glossary lookup

Finite proof field

A declared finite collection of claim nodes, admissible leaves, and recorded inference rules. Certificate validity is relative to this supplied system.

Hand-worked example · Papers, proofs, Lean, and code · Recorded inference rule · Admissible leaf · Certificate

Back to glossary lookup

Admissible leaf

A node allowed as a starting point under the declared proof-field contract. Selecting such a leaf does not require deriving it again inside that certificate.

Hand-worked example · Papers, proofs, Lean, and code · Finite proof field · Hypothesis

Back to glossary lookup

Recorded inference rule

A specified set of premise nodes together with a conclusion node. The certificate can use the rule only when the required premises have been derived and its recorded certification permits it.

Hand-worked example · Papers, proofs, Lean, and code · Finite proof field · Verification closure

Back to glossary lookup

Verification closure

The nodes obtainable by admitting selected admissible leaves and repeatedly applying the retained certified rules whose premises are available.

Hand-worked example · Papers, proofs, Lean, and code · Admissible leaf · Recorded inference rule · Certificate

Back to glossary lookup

Inclusion-minimal certificate

A valid node-and-rule certificate with no valid strictly smaller subcertificate under componentwise inclusion. Several incomparable minimal certificates can exist.

Hand-worked example · Papers, proofs, Lean, and code · Certificate · Least certificate · Minimum-cost certificate

Back to glossary lookup

Least certificate

A certificate contained componentwise in every certificate for the same request and rule system. This is stronger than being inclusion-minimal or having minimum numerical cost.

Hand-worked example · Papers, proofs, Lean, and code · Inclusion-minimal certificate · Minimum-cost certificate

Back to glossary lookup

Minimum-cost certificate

A valid certificate attaining the lowest declared total cost among the permitted certificates. Costs count selected items according to the supplied rule, so a shared premise need not be charged each time it is used.

Hand-worked example · Papers, proofs, Lean, and code · Certificate · Least certificate · Finite proof field

Back to glossary lookup

Series and cyclic functions

Coefficient operations and the distinction between a finite truncation and an infinite series.

Coefficient · Power series · Truncation · Formal reciprocal · Coefficient convolution · Root of unity · Derivative in the series example · Differential equation · Initial condition · Contracted argument · Coefficient recurrence

Coefficient

The scalar multiplying a specified basis term. In f(z) = sum aₙzⁿ, aₙ is the coefficient of zⁿ.

Hand-worked example · Papers, proofs, Lean, and code · Scalar · Basis

Back to glossary lookup

Power series

An expression sum aₙzⁿ with infinitely many coefficient positions. A formal power series is manipulated through its coefficients. Evaluating it at a number additionally requires convergence.

Hand-worked example · Papers, proofs, Lean, and code · Coefficient · Truncation

Back to glossary lookup

Truncation

Keeping only specified degrees or levels. Equality modulo zᴺ means the coefficients of degrees below N agree. It need not be equality of the full functions or series.

Hand-worked example · Papers, proofs, Lean, and code · Power series · Residual

Back to glossary lookup

Formal reciprocal

For a power series over a field with nonzero constant coefficient, the unique series whose product with it is one. Its coefficients are determined recursively. A finite truncation only verifies the corresponding finite set of coefficient identities.

Also called: Multiplicative inverse of a formal series.

Hand-worked example · Papers, proofs, Lean, and code · Power series · Coefficient convolution · Field

Back to glossary lookup

Coefficient convolution

The multiplication rule cₙ = sum from k=0 to n of aₖbₙ₋ₖ for ordinary power series. Each output coefficient is a finite sum, even when the series are infinite.

Hand-worked example · Papers, proofs, Lean, and code · Coefficient · Power series

Back to glossary lookup

Root of unity

A complex number ω with ωᴺ = 1 for a positive integer N. It is primitive when N is its least positive such exponent. A weighted average over the powers of a primitive Nth root selects coefficients in one residue class modulo N.

Hand-worked example · Papers, proofs, Lean, and code · Residue class · Packet

Back to glossary lookup

Derivative in the series example

For n≥1, differentiating a power-series term aₙzⁿ gives n aₙzⁿ⁻¹. Constant terms differentiate to zero. Formal differentiation acts on coefficients. An analytic interpretation uses the function’s convergence and differentiability conditions.

Hand-worked example · Papers, proofs, Lean, and code · Coefficient · Power series

Back to glossary lookup

Differential equation

An equation relating an unknown function to one or more of its derivatives. The example also evaluates the same function at contracted arguments qz and rz.

Hand-worked example · Papers, proofs, Lean, and code · Derivative in the series example · Initial condition · Contracted argument

Back to glossary lookup

Initial condition

A specified value, or collection of derivative values, used with a differential equation. The feedback example fixes T(0)=0, and the equation then forces T′(0)=1.

Hand-worked example · Papers, proofs, Lean, and code · Differential equation · Derivative in the series example

Back to glossary lookup

Contracted argument

Evaluation at qz with 0<q<1 in the feedback example. A term cₙzⁿ becomes cₙqⁿzⁿ after this substitution. The scaling is inside the defining equation.

Hand-worked example · Papers, proofs, Lean, and code · Coefficient · Differential equation

Back to glossary lookup

Coefficient recurrence

A rule determining successive series coefficients from earlier ones. It gives exact finite calculations at each degree. Analytic convergence and bounds for a discarded tail require additional arguments.

Also called: Recurrence for coefficients.

Hand-worked example · Papers, proofs, Lean, and code · Coefficient · Truncation · Coefficient convolution

Back to glossary lookup

Finite quantum systems

States, measurement and channels on finite complex vector spaces.

Complex conjugate · Adjoint matrix · Unitary matrix · Quantum amplitude · Density matrix · Matrix trace · Born probability · Purity of a density matrix · Dephasing · Kraus operators · Hermitian matrix · Positive semidefinite matrix · Coherence in a chosen basis

Complex conjugate

For real a and b, the conjugate of a+bi is a−bi. The squared modulus is (a+bi)(a−bi) = a²+b².

Hand-worked example · Papers, proofs, Lean, and code · Inner product · Scalar

Back to glossary lookup

Adjoint matrix

For a complex matrix in orthonormal bases, the adjoint A* is its conjugate transpose. In real orthonormal bases this is the ordinary transpose.

Also called: Conjugate transpose, Hermitian transpose.

Hand-worked example · Papers, proofs, Lean, and code · Complex conjugate · Inner product

Back to glossary lookup

Unitary matrix

A complex square matrix U with UU = UU = I. It preserves the complex inner product and therefore vector norms.

Hand-worked example · Papers, proofs, Lean, and code · Adjoint matrix · Norm · Orthogonal matrix

Back to glossary lookup

Quantum amplitude

A complex coordinate of a normalized state vector in a chosen orthonormal basis. Its squared modulus gives that basis outcome’s probability. Relative phases can affect measurements in other bases.

Hand-worked example · Papers, proofs, Lean, and code · Complex conjugate · Born probability · Coordinates

Back to glossary lookup

Density matrix

A positive semidefinite Hermitian matrix with trace one. A normalized vector ψ gives the pure-state matrix ρ = ψψ*. Different vectors that differ only by an overall complex phase give the same density matrix.

Hand-worked example · Papers, proofs, Lean, and code · Adjoint matrix · Matrix trace · Purity of a density matrix

Back to glossary lookup

Matrix trace

The sum of diagonal entries of a square matrix. It is unchanged by an invertible change of basis. Field trace is a related arithmetic construction with its own definition.

Hand-worked example · Papers, proofs, Lean, and code · Matrix · Field trace

Back to glossary lookup

Born probability

For a density matrix ρ and an orthogonal measurement projector P, the outcome probability is tr(Pρ). A complete orthogonal projector family gives probabilities summing to one.

Hand-worked example · Papers, proofs, Lean, and code · Density matrix · Matrix trace · Orthogonal projector

Back to glossary lookup

Purity of a density matrix

The number tr(ρ²). For a finite density matrix it equals one exactly for a pure state and is smaller for a mixed state.

Hand-worked example · Papers, proofs, Lean, and code · Density matrix · Matrix trace

Back to glossary lookup

Dephasing

For a specified complete orthogonal family Pᵢ, the channel ρ ↦ sum PᵢρPᵢ removes coherence between different selected subspaces. Its effect depends on the chosen decomposition.

Hand-worked example · Papers, proofs, Lean, and code · Density matrix · Projector · Kraus operators

Back to glossary lookup

Kraus operators

Matrices Kᵢ describing a finite quantum channel by Φ(ρ) = sum KᵢρKᵢ. The condition sum KᵢKᵢ = I makes this map trace preserving.

Also called: Kraus representation.

Hand-worked example · Papers, proofs, Lean, and code · Adjoint matrix · Density matrix · Matrix trace

Back to glossary lookup

Hermitian matrix

A complex square matrix A with A* = A. Its diagonal entries are real and opposite off-diagonal entries are complex conjugates. This condition alone does not imply positivity.

Also called: Self-adjoint matrix.

Hand-worked example · Papers, proofs, Lean, and code · Adjoint matrix · Positive semidefinite matrix

Back to glossary lookup

Positive semidefinite matrix

A Hermitian matrix A for which v*Av is nonnegative for every vector v. Zero eigenvalues are allowed.

Also called: PSD, PSD matrix.

Hand-worked example · Papers, proofs, Lean, and code · Hermitian matrix · Eigenvalue · Density matrix

Back to glossary lookup

Coherence in a chosen basis

Off-diagonal density-matrix entries that encode relations between different basis components. They can contribute to probabilities after a change of measurement basis.

Hand-worked example · Papers, proofs, Lean, and code · Density matrix · Dephasing · Quantum amplitude

Back to glossary lookup

Arithmetic and modules

Finite fields, lift branches, and the module data behind support.

Prime power · Modular reduction · Lift branch · Compatible tower · p-adic integer · Survival to a finite level · Prime field · Extension field · Finite-field Frobenius · Field trace · Field norm · Irreducible polynomial · Commutative ring with identity · Module · Module presentation · Cokernel · Module annihilator · Module support · Zeroth Fitting ideal · Multiplicity in the module example · Ideal · Prime ideal · Localization at a prime

Prime power

An integer pⁿ with p prime and n a nonnegative integer. Successive positive powers give the moduli in the lift-branch example.

Hand-worked example · Papers, proofs, Lean, and code · Integer congruence · Prime field

Back to glossary lookup

Modular reduction

Passing from a residue class modulo pⁿ⁺¹ to its class modulo pⁿ. This map forgets the highest retained base-p digit.

Hand-worked example · Papers, proofs, Lean, and code · Prime power · Residue class · Coarsening

Back to glossary lookup

Lift branch

A sequence of solutions at successive levels whose reductions agree. A node at one finite level can have several children or no child.

Hand-worked example · Papers, proofs, Lean, and code · Lift · Modular reduction · Compatible tower

Back to glossary lookup

Compatible tower

A collection of objects with specified maps between levels and stated compatibility identities. For modular solutions, the next residue must reduce to the preceding one.

Hand-worked example · Papers, proofs, Lean, and code · Compatibility · Modular reduction · Completion

Back to glossary lookup

p-adic integer

For a prime p, an element of the inverse limit of the residue rings modulo pⁿ. It specifies a compatible residue at every positive level. A finite list of residues is only a truncation of that data.

Hand-worked example · Papers, proofs, Lean, and code · Compatible tower · Prime power · Truncation

Back to glossary lookup

Survival to a finite level

A branch reaches the chosen last level without losing compatibility or the required equations. Survival to that level alone says nothing about the next one.

Hand-worked example · Papers, proofs, Lean, and code · Lift branch · Finite check

Back to glossary lookup

Prime field

The smallest subfield of a field. In characteristic p it consists of the p scalar classes and is isomorphic to Fₚ. In characteristic zero it is isomorphic to the rational numbers.

Hand-worked example · Papers, proofs, Lean, and code · Field · Integer congruence

Back to glossary lookup

Extension field

A field containing a specified smaller field. The extension degree is its vector-space dimension over that smaller field.

Hand-worked example · Papers, proofs, Lean, and code · Field · Dimension · Prime field

Back to glossary lookup

Finite-field Frobenius

In a finite field of characteristic p, the map x ↦ xᵖ is an automorphism. Over F_q, the relative Frobenius is x ↦ x^q. The example uses q = p = 5.

Hand-worked example · Papers, proofs, Lean, and code · Extension field · Linear isomorphism

Back to glossary lookup

Field trace

For a finite field extension L/K, the trace of the K-linear map that multiplies L by an element a. In F₂₅/F₅ it is a+a⁵.

Hand-worked example · Papers, proofs, Lean, and code · Matrix trace · Extension field · Finite-field Frobenius

Back to glossary lookup

Field norm

For a finite field extension L/K, the determinant of multiplication by an element a as a K-linear map. In F₂₅/F₅ it is a·a⁵. This norm is algebraic and is not a vector length.

Hand-worked example · Papers, proofs, Lean, and code · Determinant · Extension field · Norm

Back to glossary lookup

Irreducible polynomial

A nonconstant polynomial over a field that cannot be factored into two polynomials of positive degree over that field. For degree two, irreducibility is equivalent to having no root in the field.

Hand-worked example · Papers, proofs, Lean, and code · Field · Extension field

Back to glossary lookup

Commutative ring with identity

A system with addition, subtraction and commutative multiplication satisfying the ring laws and having a multiplicative identity. A nonzero element need not have a multiplicative inverse.

Hand-worked example · Papers, proofs, Lean, and code · Field · Module

Back to glossary lookup

Module

An abelian additive group with a scalar action by a ring satisfying the usual distributive, associative, and identity laws. For a module over Q[t], multiplication by t can be specified by a Q-linear operator.

Hand-worked example · Papers, proofs, Lean, and code · Commutative ring with identity · Operator algebra

Back to glossary lookup

Module presentation

A description of a module by generators and relations. A finite matrix A: Rᵐ → Rⁿ presents the quotient Rⁿ/im A.

Hand-worked example · Papers, proofs, Lean, and code · Module · Cokernel · Image

Back to glossary lookup

Cokernel

For a linear map or module map A: U → V, the quotient V/im A. It records target classes modulo those already reached by A.

Hand-worked example · Papers, proofs, Lean, and code · Quotient space · Image · Module

Back to glossary lookup

Module annihilator

The ideal of ring elements that act as zero on every element of a module. For Q[t]/(tᵏ), the annihilator is the ideal (tᵏ).

Hand-worked example · Papers, proofs, Lean, and code · Module · Nilpotent operator · Commutative ring with identity

Back to glossary lookup

Module support

The prime ideals at which a module’s localization is nonzero. In the example Q[t]/(tᵏ), the support is the single prime ideal (t). The underlying support set does not determine k or the module.

Hand-worked example · Papers, proofs, Lean, and code · Module · Module annihilator · Multiplicity in the module example

Back to glossary lookup

Zeroth Fitting ideal

For a finite presentation Rᵐ → Rⁿ → M → 0 over a commutative ring, the ideal generated by the n by n minors of the presentation matrix. In the one-generator example with relation tᵏ, it is (tᵏ).

Hand-worked example · Papers, proofs, Lean, and code · Module presentation · Determinant · Module support

Back to glossary lookup

Multiplicity in the module example

For Q[t]/(tᵏ) supported at t=0, the integer k records the module’s length and its Q-vector-space dimension. This is additional data beyond the one-point support set. Other works use multiplicity with their own specified objects.

Hand-worked example · Papers, proofs, Lean, and code · Dimension · Module support · Nilpotent operator

Back to glossary lookup

Ideal

An additive subgroup of a commutative ring closed under multiplication by every element of the ring. The principal ideal (f) consists of all multiples of f.

Hand-worked example · Papers, proofs, Lean, and code · Commutative ring with identity · Module annihilator

Back to glossary lookup

Prime ideal

A proper ideal P such that ab in P implies a in P or b in P. The ideal (t) in Q[t] is prime because the quotient is the field Q.

Hand-worked example · Papers, proofs, Lean, and code · Ideal · Commutative ring with identity · Field

Back to glossary lookup

Localization at a prime

A construction that makes ring elements outside a chosen prime ideal invertible, and carries a module along with that scalar change. The prime lies in the module’s support exactly when the localized module is nonzero.

Hand-worked example · Papers, proofs, Lean, and code · Prime ideal · Module support · Module

Back to glossary lookup

Dynamics, memory, and calibration

What a retained state predicts and what exact observations determine.

Visible state · Hidden state · Prepared hidden initialization · Discrete memory maps · Autonomous dynamics of a summary · State augmentation · Semigroup law for evolution maps · Exact operator calibration · Calibration span · Compatible model · Linear extension · Reusable calibrated core · Identifiability relative to a model class

Visible state

The state coordinates or summary retained for a specified prediction task. A visible value need not contain enough information to determine its own next value.

Hand-worked example · Papers, proofs, Lean, and code · Hidden state · Autonomous dynamics of a summary · Coarsening

Back to glossary lookup

Hidden state

The part of the declared full state omitted by the current observation or summary. It can influence later visible outputs even when it does not affect the current output.

Hand-worked example · Papers, proofs, Lean, and code · Visible state · Discrete memory maps

Back to glossary lookup

Prepared hidden initialization

An initialization that fixes the hidden coordinates by a specified rule. The example uses R(y)=(y,0). Results for this preparation need not hold for arbitrary hidden starting values.

Hand-worked example · Papers, proofs, Lean, and code · Hidden state · Reconstruction · Autonomous dynamics of a summary

Back to glossary lookup

Discrete memory maps

For the block update (y,z) ↦ (Ay+Bz,Gy+Dz), the maps Mₖ=BDᵏG describe a visible-to-hidden entry, k hidden transitions, and a return. The first effect of Mₖ on prepared visible evolution occurs after k+2 full steps.

Hand-worked example · Papers, proofs, Lean, and code · Block matrix · Hidden state · Prepared hidden initialization

Back to glossary lookup

Autonomous dynamics of a summary

A transition rule determined by the retained current state, under the declared controls and initialization contract. For deterministic maps, full states with the same summary must have the same next summary.

Hand-worked example · Papers, proofs, Lean, and code · Visible state · Fiber · Factorization through a map

Back to glossary lookup

State augmentation

Enlarging a retained state with additional coordinates or history needed for future prediction. The hidden-memory example retains the previous visible value along with the current one.

Hand-worked example · Papers, proofs, Lean, and code · Visible state · Hidden state · Autonomous dynamics of a summary

Back to glossary lookup

Semigroup law for evolution maps

The identity Eₘ₊ₙ=EₘEₙ for nonnegative step counts, with E₀ the identity. It expresses agreement between uninterrupted evolution and successive uses of the same state-level evolution maps.

Hand-worked example · Papers, proofs, Lean, and code · Composition · Identity operator · Prepared hidden initialization

Back to glossary lookup

Exact operator calibration

Supplied input-output pairs for an unknown operation. For a linear operation, every linear relation among calibrated inputs must be respected by the supplied outputs.

Hand-worked example · Papers, proofs, Lean, and code · Linear map · Calibration span · Compatible model

Back to glossary lookup

Calibration span

The span of the calibrated input vectors. Consistent exact linear calibration determines the operation on this span. Its outputs can leave that span.

Hand-worked example · Papers, proofs, Lean, and code · Exact operator calibration · Span · Reusable calibrated core

Back to glossary lookup

Compatible model

A model satisfying all supplied data and every declared structural assumption. In the calibration example, all linear extensions of the known restriction are allowed, and each model stays fixed through a trajectory.

Hand-worked example · Papers, proofs, Lean, and code · Exact operator calibration · Linear extension · Identifiability relative to a model class

Back to glossary lookup

Linear extension

A linear map on a larger vector space that agrees with a given map on its original subspace. Values on an added basis can vary unless further conditions are imposed.

Hand-worked example · Papers, proofs, Lean, and code · Linear map · Subspace · Basis

Back to glossary lookup

Reusable calibrated core

For the tutorial’s unrestricted linear extension class and full-state output, the largest subspace inside the calibration span preserved by every calibrated operation. All finite operation sequences from this subspace are determined by the calibration.

Hand-worked example · Papers, proofs, Lean, and code · Calibration span · Invariant subspace · Compatible model

Back to glossary lookup

Identifiability relative to a model class

A requested quantity is identifiable from the supplied data when every compatible model gives the same value. Identifying a particular output can require less information than identifying the whole model.

Hand-worked example · Papers, proofs, Lean, and code · Compatible model · Exact operator calibration · Obstruction

Back to glossary lookup

Inference and probability

The model, observation and Gaussian calculations used in the inference example.

Finite-dimensional Gaussian model · Prior distribution · Likelihood · Posterior distribution · Covariance matrix · Precision matrix · Observation innovation · Exact Gaussian gain · Joseph covariance

Finite-dimensional Gaussian model

A model with a Gaussian state and specified linear observations with Gaussian noise. The tutorial supplies an independent noise variable, a prior mean and covariance, an observation matrix and a positive noise variance.

Hand-worked example · Papers, proofs, Lean, and code · Prior distribution · Likelihood · Covariance matrix

Back to glossary lookup

Prior distribution

The state distribution specified before conditioning on the observation under the declared model. A Gaussian prior is described by its mean and covariance.

Also called: Prior.

Hand-worked example · Papers, proofs, Lean, and code · Finite-dimensional Gaussian model · Posterior distribution · Covariance matrix

Back to glossary lookup

Likelihood

For a fixed observed value, the observation density viewed as a function of the proposed state or parameter. It is combined with the prior and normalized to obtain a posterior density when that density formula applies.

Hand-worked example · Papers, proofs, Lean, and code · Prior distribution · Posterior distribution · Finite-dimensional Gaussian model

Back to glossary lookup

Posterior distribution

The state distribution conditional on the observed data under the supplied prior and observation model. The tutorial computes the usual explicit Gaussian conditional density by completing the square.

Also called: Posterior.

Hand-worked example · Papers, proofs, Lean, and code · Prior distribution · Likelihood · Exact Gaussian gain

Back to glossary lookup

Covariance matrix

For a random vector X with mean m and finite second moments, the matrix E[(X−m)(X−m)ᵀ]. Its diagonal entries are variances. For a unit direction u, uᵀCu is the variance in that direction.

Hand-worked example · Papers, proofs, Lean, and code · Positive semidefinite matrix · Finite-dimensional Gaussian model · Precision matrix

Back to glossary lookup

Precision matrix

The inverse covariance when the covariance is invertible. In a nonsingular Gaussian density it appears in the quadratic exponent. This use of precision is distinct from the number of bits in stored arithmetic.

Also called: Inverse covariance matrix.

Hand-worked example · Papers, proofs, Lean, and code · Covariance matrix · Inverse · Precision

Back to glossary lookup

Observation innovation

The difference d=y−Hm between an observation and its predicted mean in the linear model. Its covariance is S=HPHᵀ+R when the state covariance is P and the independent noise covariance is R.

Also called: Observation residual.

Hand-worked example · Papers, proofs, Lean, and code · Finite-dimensional Gaussian model · Covariance matrix · Exact Gaussian gain

Back to glossary lookup

Exact Gaussian gain

For the declared linear Gaussian model, K=PHᵀ(HPHᵀ+R)⁻¹. Multiplying the innovation by K gives the posterior mean correction. Positive noise covariance makes the displayed observation-space inverse exist.

Hand-worked example · Papers, proofs, Lean, and code · Observation innovation · Posterior distribution · Joseph covariance

Back to glossary lookup

Joseph covariance

For a gain B, the matrix (I−BH)P(I−BH)ᵀ+BRBᵀ. It is positive semidefinite for valid prior and noise covariances. At the exact gain it equals the posterior covariance. A general gain still needs its own accuracy check.

Hand-worked example · Papers, proofs, Lean, and code · Covariance matrix · Exact Gaussian gain · Positive semidefinite matrix

Back to glossary lookup

Symbols in the introductory example

The examples use the following notation. The reading column spells out symbols for readers who are unfamiliar with them.

Symbols are local to their definitions. In another paper, the same letter can denote a different object.

Alphabetical index

A · B · C · D · E · F · H · I · J · K · L · M · N · O · P · Q · R · S · T · U · V · Z

A

Address · Adjoint matrix · Admissible leaf · Analysis and synthesis · Autonomous dynamics of a summary

B

Basis · Block matrix · Born probability

C

Calibration span · Certificate · Chinese remainder theorem · Coarsening · Coefficient · Coefficient convolution · Coefficient recurrence · Coherence in a chosen basis · Cokernel · Commutative ring with identity · Commutator · Commuting diagram · Compatibility · Compatible model · Compatible tower · Complete packet family · Completion · Complex conjugate · Composition · Conditional · Contracted argument · Coordinate change · Coordinates · Coprime integers · Covariance matrix · Cyclic vector

D

Density matrix · Dephasing · Derivative in the series example · Detail coefficient · Determinant · Diagonalizable operator · Differential equation · Dimension · Direct sum · Discrete memory maps · Domain and codomain · Dyadic rational

E

Eigenspace · Eigenvalue · Eigenvector · Elimination · Exact · Exact Gaussian gain · Exact operator calibration · Extension field

F

Factorization through a map · Feasibility · Fiber · Field · Field norm · Field trace · Finite check · Finite conditional expectation · Finite proof field · Finite repair menu · Finite-dimensional Gaussian model · Finite-field Frobenius · Formal reciprocal · Free linear repair

H

Haar pair · Hermitian matrix · Heuristic · Hidden state · Hypothesis

I

Ideal · Identifiability relative to a model class · Identity operator · Image · Inclusion-minimal certificate · Initial condition · Injective map · Inner product · Integer congruence · Intertwiner · Invariant subspace · Inverse · Irreducible polynomial

J

Joseph covariance

K

Kernel · Kraus operators

L

Lean correspondence · Least certificate · Left inverse · Lift · Lift branch · Likelihood · Linear extension · Linear independence · Linear isomorphism · Linear map · Linear obstruction witness · Localization at a prime

M

Matrix · Matrix trace · Minimal polynomial · Minimum-cost certificate · Modular inverse · Modular reduction · Module · Module annihilator · Module presentation · Module support · Multiplicity in the module example · Mutual annihilation

N

Nilpotent operator · Norm · Normalization · Nullity · Numerical · Numerical ternary

O

Observation innovation · Obstruction · Operator algebra · Operator conjugation · Operator relation · Orthogonal matrix · Orthogonal projector

P

p-adic integer · Packet · Polynomial in an operator · Polyphase decomposition · Positive semidefinite matrix · Posterior distribution · Power series · Precision · Precision matrix · Prepared hidden initialization · Prime field · Prime ideal · Prime power · Prior distribution · Projector · Proof · Purity of a density matrix

Q

Quantum amplitude · Quotient space

R

Rank · Rank–nullity identity · Realization · Reconstruction · Recorded inference rule · Redundant coordinates · Refinement · Repair direction · Repair selection cost · Residual · Residue class · Reusable calibrated core · Root of unity · Rounding

S

Scalar · Schur complement · Seed · Seed rank · Semigroup law for evolution maps · Span · Spectral projector · State augmentation · Subspace · Surjective map · Survival to a finite level

T

Theorem · Tolerance · Transfer block · Truncation · Typed path · Typed system

U

ULP · Unitary matrix

V

Vector · Vector space · Verification closure · Visible state

Z

Zeroth Fitting ideal

Reading routes · Hand-worked examples · First runs · Browse works