Matrix Mortality Glossary

Orientation#

This glossary supplies the background needed to read the matrix-mortality collection. It assumes undergraduate linear algebra and discrete mathematics, but no prior knowledge of matrix semigroups, computability, correspondence problems, tag systems, weighted automata, p-adic dynamics, or Lean.

Entries are grouped by mathematical dependency. The index below is alphabetical. A term's fragment is its canonical public name in this corpus; a former name is recorded only where it prevents confusion with existing articles or formal declarations.

Problems and decidability#

Decision problem#: A yes-or-no question attached to each input in a specified class. Formally it is a predicate on encoded inputs. A statement about a decision problem must fix the input domain: integer matrices, rational matrices, and a fixed finite family are different problems.
Decidable#: A decision problem is decidable if one algorithm halts on every valid input and returns the correct yes-or-no answer. Complexity asks how many resources such an algorithm uses; decidability asks first whether any total algorithm exists.
Semidecidable#: A problem is semidecidable, or recursively enumerable, if an algorithm halts and accepts every yes-instance but may run forever on a no-instance. Matrix mortality is semidecidable: enumerate nonempty generator words by length and stop when a zero product appears.
Undecidable#: A decision problem is undecidable if no algorithm decides every valid input. This does not mean that each instance is opaque or that no useful subclasses are decidable. An undecidability proof usually transfers the impossibility of a known problem through a computable reduction.
Many-one reduction#: A computable function that maps each instance of one decision problem to one instance of another and preserves both answers. If P reduces to Q and P is undecidable, then Q is undecidable.

$x \in P ⟺ f (x) \in Q .$
Primitive-recursive reduction#: A many-one reduction whose instance map is primitive recursive, a syntactically restricted class of total computable functions closed under composition and bounded iteration. It is stronger effectivity evidence than an existence proof of a computable map. It need not be packaged as a command-line program.
Matrix mortality#: Given finitely many square matrices of one dimension, ask whether some nonempty product of the given matrices is the zero matrix. A family with such a product is mortal; otherwise it is immortal. This corpus uses integer entries unless another coefficient ring is stated.

$\exists n \geq 1, A_{i_{1}} A_{i_{2}} \dots A_{i_{n}} = 0 .$
Bounded matrix mortality M_d(k)#: The restriction of matrix mortality to at most k integer matrices of dimension d. The parameters bound the input family, not the witness length or matrix entries. Thus M₉(2) concerns two arbitrary 9 × 9 integer matrices and products of unbounded length.
Mortality witness#: A nonempty word over the generator labels whose ordered matrix product is zero. It is also called a zero word. The empty word is excluded because its product is the identity matrix, except in dimension zero.
Scalar zero reachability Z_d(k)#: Given a row λ, a column γ, and at most k dimension-d matrices, ask whether λA_wγ is zero for some nonempty word w. Only one coefficient must vanish; the whole product need not. The structured form Z̊ requires every generator to have first column e₁. Where the empty word is also allowed, the page says so and tests its coefficient λγ separately.

$\exists w : λ A_{w} γ = 0 .$
Zero-in-the-corner problem R_d(k)#: A scalar-reachability problem in which the observed row and column are fixed coordinate vectors, so the question is whether a designated entry of some nonempty product is zero. Which entry is designated matters: diagonal and off-diagonal conventions must not be identified without a reduction.
Parameter monotonicity and padding#: Undecidability at one pair (d,k) propagates to larger generator bounds by ignoring extras and to larger dimensions by embedding each matrix as a block with a zero block. A proof must preserve both mortality and immortality and, for an effective endpoint, preserve computability of the instance map.
Frontier antichain#: The Pareto-minimal undecidable parameter pairs under coordinatewise order. Each point establishes all larger cells by monotonicity, while no point in the antichain follows from another. The antichain summarizes known bounds; it is not a classification of the cells below it.

Words and machines#

Alphabet and word#: An alphabet is a set of symbols. A word is a finite ordered list of symbols from one alphabet; its length is |w|. The empty word ε has length zero. Concatenation joins words and is generally noncommutative.
Free monoid and free semigroup#: The free monoid Σ* consists of all finite words over Σ, including ε, with concatenation. The free semigroup Σ+ contains only nonempty words. Matrix mortality quantifies over Σ+; word morphisms are usually defined on Σ*.
Word product and product order#: A labelled matrix family assigns a matrix A_a to each letter a. The product of w = w₁…w_n is taken in the displayed left-to-right order. Reversing this convention reverses words and can silently invalidate a reduction if only one side changes.

$A_{w} = A_{w_{1}} \dots A_{w_{n}} .$
Word morphism#: A map between free monoids determined by the image of each letter and extended by concatenation. Thus h(uv) = h(u)h(v) and h(ε) = ε. PCP and GPCP compare two such morphisms.
Prefix code#: A set of codewords in which no codeword is a proper prefix of another. It is complete when every infinite input stream begins with some codeword, equivalently when its prefix tree has no missing infinite branch. Prefix codes permit deterministic left-to-right decoding without a delimiter.
Decoder and transducer#: A decoder reads encoded letters and recovers source symbols. A finite-state transducer additionally carries a finite control state and may emit output while reading. Matrix compilers realize such machines by block matrices: block position stores control state, and block values store the accumulated matrix product.
Post correspondence problem (PCP)#: Given pairs of words (u_i,v_i), ask whether some nonempty index word produces equal concatenations on the two sides. The same sequence of tile indices must be used above and below.
Generalized Post correspondence problem (GPCP)#: PCP with fixed boundary words around the variable morphic images. A common convention asks whether αu(w)β = γv(w)δ for some nonempty w. Generator counts refer to the variable tiles unless a paper explicitly counts boundary pairs.
Fixed-boundary match#: An equality of two word morphisms after prescribed left or right boundary words are attached. A terminal match is the one-sided specialization used in this corpus, such as U(w)M = V(w). It is not ordinary PCP until the boundary has been compiled into tiles or matrices.
Tile and tile word#: A tile is one pair (u_i,v_i) in a correspondence instance. A tile word is the chosen sequence of tile labels. “Rule tile” and “deletion tile” name semantic roles in the synchronized tag construction, not additional boundary tiles.
Tag system#: A queue-rewriting machine specified by a finite alphabet, a positive deletion width β, and one appendant for each letter. A step reads the first letter, deletes the first β letters, and appends the word assigned to the letter read. If fewer than β letters remain, the ordinary execution halts.
Deletion width#: The fixed number β of queue symbols removed by each tag step. It is a machine parameter, not the length of an appendant. Width two is universal over sufficiently rich alphabets, while binary width two is decidable; these facts cannot be conflated.
Appendant#: The complete word appended after a tag letter is read. In the restricted binary system used here, the appendants are b and Bb. An appendant may contain a variable body, but the two nouns are not synonyms.
Neary body#: The binary word B forming the variable prefix of the c-appendant in the restricted system: tagOutput B b = b and tagOutput B c = B ++ [b]. Earlier pages used q for the same object; B is canonical to avoid collision with quotient and prime-power variables.
Tag execution and halting#: An execution is the finite or infinite sequence of queues obtained by repeated tag steps. Halting may mean that the queue becomes too short or that a distinguished symbol is encountered, depending on the encoded source theorem. A reduction must state which convention it preserves.
Cyclic and restricted binary tag systems#: A cyclic tag system cycles through a fixed list of appendants and conditionally appends the current one. A restricted binary tag system has alphabet {b,c} and a constrained pair of appendants. They are intermediate machine models in the checked halting reduction, not alternate names for an ordinary tag system.
Word taxonomy#: A tile word indexes correspondence pairs; a role word records rule or deletion roles; a control word uses compressed data and toggle controls; a binary word encodes another alphabet; a physical word indexes the actual matrix generators. These words may correspond under a compiler, but they inhabit different alphabets and should not be identified.

Linear representations#

Semiring#: A system of scalars with associative addition and multiplication, additive zero, multiplicative identity, distributivity, and absorbing zero; addition is commutative. Subtraction and division need not exist. A commutative semiring also has commutative multiplication. The examples ℕ, ℤ and ℚ suffice for the interface theorem, whose proof uses no division.
Matrix semigroup#: The set of all nonempty products generated by a family of matrices. If the identity, corresponding to the empty product, is included, the object is a matrix monoid. Mortality asks whether the zero matrix belongs to the generated semigroup.
Singular and nonsingular matrices#: A square matrix is singular when it is not invertible, equivalently when its determinant is zero over a field. “Nonsingular” means invertible. A mortal family must contain or generate singular matrices, but its individual generators need not all be singular.
Rank, kernel, and image#: The kernel of a linear map is the subspace sent to zero; its image is the subspace attained; its rank is the image dimension. Rank refers to a map or matrix. It must not be used as a synonym for the dimension of the ambient realization.
Rank profile#: The list of generator ranks in a fixed ordering, or its unordered multiset when labels are immaterial. Splitting a mortality problem by rank profile isolates invertible, zero, and singular strata. It is a classification coordinate, not a reduction or a claim that the strata are equivalent.
Invariant subspace and quotient#: A subspace W is invariant under a matrix family if every generator maps W into itself. The family then induces maps on W and on the quotient space V/W. Quotienting can remove behavior invisible to the observed scalar, but it may create false zeros unless the converse is proved.
Direct sum and block matrix#: A direct sum combines independent vector spaces; in coordinates its maps are block diagonal. Block matrices also encode transitions between components. The zero-padding map A ↦ A ⊕ 0 preserves zero products because a word product becomes A_w ⊕ 0.
Outer product and rank-one separator#: The outer product uv^T has rank at most one. Used as a separator C around a product A_w, it converts one scalar coefficient into a whole zero matrix. A nonzero rank-one separator has both boundary vectors nonzero.

$C A_{w} C = u (v^{T} A_{w} u) v^{T} .$
Boundary data and scalar coefficient#: A boundary row λ and boundary column γ select the scalar λA_wγ from a matrix product. They encode fixed left and right words or initial and terminal linear states. Boundary data belong to scalar reachability; a rank-one separator is the matrix constructed from them.
Word series#: A function from words to scalars. A linear representation has the form s(w) = λμ(w)γ, where μ is a matrix-valued word morphism. Unlike an ordinary sequence, a word series branches over every letter at each length.
Paired scalar series#: The project’s four-dimensional word series for fixed-boundary correspondence. Two data controls and one phase toggle carry the two encoded words; the boundary coefficient vanishes exactly when they agree. The reusable scalar interface states this contract; the coordinate formula supplies its matrices.
Zero language#: The set of words at which a scalar- or matrix-valued word series vanishes. A reduction to mortality often needs only this language, not the exact nonzero values. The empty word must be handled separately when the target problem requires a nonempty witness.
Zero-language equivalence#: Pointwise agreement about which words vanish: f(w) = 0 if and only if g(w) = 0 for every word in the stated domain. The formal code sometimes calls this “same-zero.” It is weaker than equality of series and therefore can admit smaller realizations.
Existential zero transport#: Preserving whether a nonempty zero word exists, while allowing a witness to be replaced by a different word. This is weaker than pointwise zero-language equivalence. In M₈(2), prepending a toggle replaces each source zero rejected by the changed separator.
Asymmetric separator#: The rank-one separator used in the eight-dimensional construction. Its row assigns different slopes to the rule and erase phases: erase-phase zeros are exactly word equalities, while the rule phase never vanishes on the source image. A leading toggle restores any discarded witness. It preserves existence of a zero, not the full zero language. See the construction and scope.
Linear representation#: A finite-dimensional factorization of a word series into an initial row, a matrix morphism, and a terminal column. “Realization” denotes the same mathematical structure when emphasizing its state-space construction. Exact representations preserve every value; zero-language representations need only preserve zeros.
Realization dimension#: The dimension of the vector space on which a linear representation acts. This corpus says “nine-dimensional realization,” not “nine-state realization,” because state is reserved for automata and dynamical systems. “Rank nine” is used only when an actual matrix or Hankel form has rank nine.
Ternary word value#: Recode the binary symbols 0 and 1 as the ternary digits 1 and 2. Read the resulting string as a base-three integer, denoted σ, with the empty string assigned zero. For example, the binary word 01 becomes the ternary numeral 12, of value five. No leading zero is allowed, so distinct words, including words of different lengths, have distinct values. Appending a word shifts the old digits left by its length:

$σ (uv) = σ (u) 3^{| v |} + σ (v) .$
Periodic ternary value#: For a nonempty block w, the rational value of the infinite ternary fraction repeating its recoded digits is $\frac{σ (w)}{3^{| w |} - 1}$ . Different finite blocks can have the same periodic value. Equality is equivalent to commutation of the blocks, by cross multiplication and finite ternary-code injectivity.
Word commutation#: Two words commute when their concatenations agree in either order: $uv = vu$ . For example, 01 and 0101 commute; 01 and 10 do not. This finite identity allows prefix comparisons between competing periods without constructing infinite words. See its use in the wrong-phase exclusion.
Word-pair representation#: A matrix morphism that encodes a pair of words so multiplication represents pairwise concatenation. The three-dimensional construction stores powers of three and ternary word values, turning equality of encoded words into vanishing of one matrix entry.
Agreement subspace#: A subspace on which two linear actions agree. In paired-role compression, equal upper words give an agreement plane for each rule/deletion pair. Identifying this plane across the two phase copies saves two dimensions. The induced control maps must be well-defined on the quotient and preserve the observed coefficient for every word.
Change of basis and conjugation#: Replacing every generator A by P⁻¹AP expresses the same linear action in another basis and preserves mortality. If P and P⁻¹ have integer entries, P is unimodular and integrality is preserved. Rational changes of basis may require later denominator clearing.
Hankel matrix and Hankel rank#: The Hankel matrix of a word series has rows and columns indexed by words and entry H_u,v = s(uv). Over a field, its rank is the minimum dimension of an exact linear representation. This lower bound does not automatically apply to a different series with the same zero language.

Compilers and return systems#

Compiler#: An explicit, structure-preserving transformation between problem presentations, usually assembled from smaller encodings and equipped with forward and converse theorems. A compiler becomes a decision-problem reduction only after its instance map is effective and its yes/no equivalence is proved for every input.
Paired-role compression#: The project construction that identifies an agreement subspace across rule and deletion phases, replacing four semantic roles by three controls: two data controls and one phase toggle. The quotient must preserve the boundary coefficient for every control word, not only correctly phased executions.
Binary compiler#: A compiler replacing a finite generator alphabet by two generators. It uses a binary code and stores the unfinished codeword in a finite-dimensional decoder. Correctness must cover complete codewords, incomplete suffixes, and words beginning from every reachable decoder state.
Common-image restriction#: A dimension reduction in which all relevant generators map into one common invariant image, allowing the representation to be restricted to that image. The easy direction projects zero products. The converse needs a synchronizing or appended letter that turns any new restricted zero into a zero of the original family.
Transition matrix#: An actual generator designated to occupy the blocks between cuts. In a one-transition return system it is the matrix A whose powers encode waiting or internal evolution. “Transition” names a role in the physical family; earlier prose also called it the ambient matrix or ambient action.
Input and output maps#: Linear maps U into a transition space and O back to an interface space. They expose the return OAⁿU after n transition steps. Full-rank hypotheses allow cancellation in the split construction, but singular-return compression does not need them.
Interface space#: A vector space S through which a cut matrix factors. Input maps send S into the physical transition space; output maps return to S. Its dimension may exceed the rank of the cut, so “interface dimension” and “cut rank” are not aliases.
Interface bridge#: For cuts indexed by i and j and a transition word w, the bridge from i to j is O_iA_wU_j. Consecutive cuts in a physical word multiply as a path of such maps on the interface space.
Interface compression#: The exact reduction of mortality for transitions and factored cuts to two cases: a transition-only zero word or a zero product along a nonempty path of interface bridges. The proof retains transitions before the first cut and after the last. Rank-one separators and singular-return compression are specializations.
Return matrix and return family#: The return matrix at wait n is M_n = OAⁿU. The return family is the infinite labelled family of all M_n. A physical word with several cuts becomes a product of returns whose labels are its intervening wait lengths.

$M_{n} = O A^{n} U .$
Return realization#: The triple (A,U,O), together with its transition and interface spaces, that realizes a prescribed return sequence. Earlier M₉(2) prose called the explicit construction a return chart. “Realization” states the mathematical object; coordinates and charts are presentations of it.
Cut matrix#: An actual generator designated as a boundary between transition blocks. When C = UO, each occurrence forces the ambient product through the interface space. “Cut” names an analytic role, not an added matrix or a restriction on allowed words. Its rank is at most the interface dimension and need not be one.
Factored cut#: A cut generator presented as C_j = U_jO_j through a common interface space. The factorization supplies the endpoints of interface bridges; it need not be a minimal-rank factorization.
Physical family#: The finite matrix family supplied to the actual target problem, as opposed to an infinite return family or an intermediate semantic alphabet. For two-generator return compression the physical family is {A,UO}. A physical word is an unrestricted nonempty word over these matrices.
Split-return normal form#: A return construction in which the cut factors through an interface with full-rank input and output maps and the transition is invertible. These hypotheses give the physical/return mortality equivalence by cancellation. They are stronger assumptions than those needed by singular-return compression, not a stronger conclusion. See the rank-two example.
Singular-return compression#: The single-transition, single-cut specialization of interface compression: mortality of {A,UO} is equivalent to mortality of {OAⁿU : n ≥ 0}, assuming only that no pure power Aⁿ is zero. Sandwiching a cut-containing physical zero retains its exterior waits; wrapping a zero return product in cuts gives the converse.

$A^{p_{0}} U O \dots U O A^{p_{r}} = 0 \Rightarrow \prod (O A^{p_{j}} U) = 0 .$
Exterior wait and pure transition word#: In a physical word, transitions before the first cut or after the last cut are exterior waits. A word containing no cut is a pure transition word Aⁿ. Both cases must be controlled; proving only the grammar of transitions between cuts does not prove unrestricted mortality.
Moment sequence and geometric tail#: The sequence OAⁿU of returns is the moment sequence of a realization. An exceptional moment is one of finitely many prescribed initial values. A geometric tail has the form s^n−NR after a cutoff N, so one eigenmode carries every later return.
Nilpotent block, Jordan block, and eigenline#: A nilpotent block dies after finitely many powers and can carry exceptional moments. A Jordan block is a standard indecomposable block for one eigenvalue. An eigenline is a one-dimensional invariant subspace; a nonzero eigenvalue on it proves that no power of the whole transition matrix is zero.
Denominator clearing#: Multiplying each rational generator by a nonzero common denominator produces integer generators. A word product is multiplied by the product of its generators' nonzero scalars, so zero is preserved and reflected. “Integerization” names this passage; effectivity additionally requires the denominators and entries to be computable.

Arithmetic dynamics#

Projective line and projective point#: The projective line over a field is the set of one-dimensional subspaces of a two-dimensional vector space. A nonzero pair (x,y) represents the point [x:y]; multiplying both coordinates by a nonzero scalar leaves the point unchanged. The affine coordinate is x/y when y ≠ 0.
Projectivization#: Passing from a nonzero vector or rank-one image to its projective point, thereby forgetting common scalar content. This often reduces a two-coordinate return recurrence to a one-variable rational map. It loses information needed for integrality or height arguments, so primitive representatives may later be restored.
Möbius transformation#: The projective action of an invertible 2 × 2 matrix. In an affine chart it is a fractional-linear map; the denominator-zero point is sent to infinity. Composition corresponds to matrix multiplication up to nonzero scalar.

$z \mapsto \frac{a z + b}{c z + d} .$
Projective incidence#: Ask whether a product of invertible rational 2 × 2 matrices sends a nonzero source column into the kernel of a nonzero target row. Equivalently, the scalar r^TM_wc must vanish. Multiplying generators by nonzero scalars preserves the answer. GPI₂ is the two-generator restriction with the two explicit generic-chart normalizations, not a name for every incidence instance.
Shortcut-Collatz map and reachability#: The integer map sending even n to n/2 and odd n to (3n+1)/2. Shortcut-Collatz reachability asks, for one supplied integer, whether some finite iterate equals 1. It is a pointwise decision problem, distinct from the universal Collatz conjecture.
p-adic valuation#: For a prime p and nonzero rational x, ν_p(x) is the exponent of p in the reduced factorization of x. It is positive for divisibility in the numerator, negative for powers in the denominator, and additive under multiplication. Conventionally ν_p(0) = ∞.
p-adic unit#: A nonzero rational with p-adic valuation zero. For an integer, this means not divisible by p. Unit conditions prevent cancellation from changing a chosen valuation and are frequently the local hypotheses behind wait-forcing arguments.
Ultrametric law#: The p-adic valuation satisfies ν_p(x + y) ≥ min{ν_p(x),ν_p(y)}. If the two input valuations differ, equality holds. Thus terms of unequal valuation cannot cancel, the rigidity used by valuation guards and walls.
Orbit and partial map#: An orbit is the sequence obtained by iterating a map from an initial point. A partial map is defined only on a stated domain; an illegal input may be sent to a rejecting sink when one wants a total transition system. Reachability asks whether the orbit ever meets a target set.
Live region and trap#: A live region contains the nonterminal states not yet excluded by an invariant. Membership does not guarantee eventual success. A trap is a forward-invariant set excluding the target: once entered, it cannot be escaped to reach the target. The valuation guard uses these regions to reject incorrect waits.
Valuation guard#: The project construction in which a return can stay live only when its chosen wait equals a p-adic valuation, thereby turning an arbitrary word choice into deterministic arithmetic evolution. “Guard” names the enforcement mechanism, not an extra generator or an algorithm deciding all resulting orbits.
Ready point and legal wait#: In the valuation guard, a live point has a unique candidate wait: its positive p-adic valuation. It is ready only if it also satisfies the exact carry-depth equation. Readiness is necessary for that wait to avoid the trap, not sufficient for eventual success. A ready orbit may continue forever.
Reset, target, and tail coordinate#: The reset is the distinguished initial projective point; the target is the point killed by the terminal separator. A tail coordinate is a rational affine coordinate chosen so the legal return has a simple recurrence. These roles are semantic and may be represented by different homogeneous vectors after normalization.
Valuation wall#: A proved p-adic invariant separating the reset orbit from the target. Typically a strict ball around reset is preserved by every positive legal branch while the target lies outside it. A wall is a sufficient immortality certificate for the parameter chamber satisfying its inequalities, not a global decision procedure.
Reset-defect numerator#: For integral parameters with α = A/L and drift δ = D/L, the integer A + D − L = L(α + δ − 1). It measures the reset's affine displacement from the terminal target after denominators are cleared. Earlier prose and formal names called it the “reset resultant”; it is not a polynomial resultant.
Primitive pair and content#: A nonzero integer pair is primitive when its two coordinates are coprime. Dividing both coordinates by their greatest common divisor removes its content without changing the represented projective point. A signed content also records a simultaneous sign change. The terminal-centered coordinates use such pairs to track divisibility that projectivization alone forgets.
Resultant and cross-resultant#: The resultant of two polynomials is an elimination invariant that vanishes when they have a common root over an algebraic closure. For two affine pencils, the cross-resultant is the corresponding 2 × 2 determinant of coefficients. This standard noun is reserved for elimination; it does not name the reset-defect numerator.
Smith normal form and Smith split#: Smith normal form diagonalizes an integer matrix using unimodular row and column operations, exposing divisibility invariants. A Smith split in the return-guard analysis factors primitive endpoint content according to those invariants. It is a derived arithmetic coordinate system, not another dynamical state space.
Exact-order prime and primitive divisor#: A prime ℓ has exact multiplicative order n for base p when pⁿ ≡ 1 mod ℓ and no smaller positive exponent works. A primitive prime divisor of pⁿ − 1 divides no p^m − 1 with 0 < m < n; therefore p has exact order n modulo ℓ. Such primes isolate a chosen wait length.

Verification and evidence#

Formalization#: A mathematical development expressed in a proof assistant's formal language. Formalization includes definitions and theorem statements as well as proofs. Its value depends on statement fidelity: a flawless proof of a weakened or misencoded proposition does not establish the intended theorem.
Machine-checked theorem#: A theorem whose proof term has been accepted by a small trusted kernel. In this repository, “Lean proves” means the declaration is in the checked dependency chain and passes the strict build. It does not mean that the prose statement, literature claim, or external source theorem was automatically audited.
Transitive axiom set#: The axioms on which a theorem depends after following every referenced declaration. Auditing only the theorem's source file can miss an admitted result upstream. This project snapshots the complete transitive set for publication-facing declarations and rejects project-specific axioms and proof escapes.
Trust boundary#: The components that must be trusted rather than proved within the artifact. For a Lean theorem this normally includes the kernel, compiler/runtime assumptions, the pinned library, and the fidelity of definitions to the informal problem. External universality or literature theorems enlarge the boundary unless they are reconstructed formally.
Symbolic cross-check#: A separate exact calculation, often in a computer algebra system, that reconstructs identities using rational or polynomial arithmetic. It is auxiliary when Lean already proves the identity: useful for discovery, regression diagnosis, and independent formula transcription, but not an additional premise of the theorem.
Finite falsifier#: A bounded exhaustive search designed to refute an overstrong universal claim by finding a counterexample. Passing the search excludes counterexamples only within its bound. It becomes a proof only when a proved finite reduction shows that every possible counterexample lies inside the searched domain.
Computational evidence#: Exact or numerical observations not yet connected to the target by a complete proof. Exact arithmetic prevents rounding error but does not turn a sampled or bounded experiment into a universal theorem. A formal-scope statement must distinguish such evidence from proved results.
Obstruction and no-go theorem#: An obstruction proves that a stated architecture, parameter chamber, or invariant cannot achieve its intended target. A no-go theorem is useful only with its quantifiers and scope intact. It does not rule out unrelated compilers, a changed zero language, or the original open problem unless it explicitly quantifies over them.
Formal scope#: The exact boundary between claims proved in the assistant and claims supported by prose, computation, or literature. A page's formal-scope statement should name the final declarations, imported assumptions, and remaining external seams. Formal scope is narrower than rhetorical confidence and broader than a list of filenames.

Sources#

Standard mortality and bounded-reduction terminology follows Cassaigne, Halava, Harju, and Nicolas; bounded GPCP terminology follows Nicolas; the restricted tag vocabulary follows Neary; and the Hankel-rank convention follows weighted-automata literature. Project-specific terms are defined by the linked expositions and Lean modules.

Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014.
François Nicolas, (Generalized) Post Correspondence Problem and Semi-Thue Systems, 2008.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015.
Stefan Kiefer, Notes on Equivalence and Minimization of Weighted Automata, 2020.
Formal Verification, theorem map and trust boundary for this corpus.