Reference
Glossary
Definitions for the mathematics, software, and research described on this site. Open a term for an explanation, examples, and its use in Plectis.
About these definitions
How to read definitions. A word can have different meanings in different subjects. Each card explains the relevant meaning and any more specific use in Plectis. A system-local specialization is a narrower use of an established term; a system-coined term is a name created for this system. These local meanings apply here, without redefining the word for everyone else. For example, a paper is a written account of a question, argument, or result, published here as a PDF and web page. A paper module is an internal guide to part of the system; it is not itself a research paper or proof.
Legacy name note. Microcosm is a compatibility identifier for Plectis, not a second product. Search this page for the card. It still appears in lineage, legacy URLs, old source paths, and migration records. For the rename and old-route behavior, read Lineage & legacy and the legacy route manifest.
No terms match that filter.
PlectisProject identityPlectis is this project's public name, covering its mathematical research, formal proofs, and supporting software.
componentSystem-local specializationA component is a distinct part of a system with a defined job and interfaces to other parts.
scope limitSystem-local specializationA scope limit states where a claim, permission, or piece of evidence stops applying.
evidence classSystem-coined termAn evidence class identifies how a claim is supported, such as by a proof, test run, calculation, or citation.
recordSystem-local specializationA record is stored information about an object, event, decision, or result.
substrateSystem-local specializationHere, substrate means the underlying files, stored state, and tools on which the system operates.
source authoritySystem-local specializationSource authority identifies which record or implementation controls a particular fact when other views disagree.
organ (source identifier)Compatibility identifierOrgan is the source-code term for a bounded unit that the public site usually calls a component.
check resultSystem-local specializationA mathematical witness is an object showing that an existence claim holds; in Plectis's software records, the word can also mean evidence of a check.
2-kernelGeneral or domain usageThe 2-kernel of a sequence a(n) is the family of subsequences n↦a(2ᵉn+r), for all e≥0 and 0≤r<2ᵉ.
a microcosmGeneral or domain usageA microcosm is a small example that reflects features of a larger system or situation.
above and beyondSystem-local specializationIn Plectis, “above and beyond” means doing the useful follow-through that makes a completed task easy to find, check, and continue.
absolute convergenceGeneral or domain usageA series converges absolutely if the sum of the absolute values of its terms is finite.
absolute valueGeneral or domain usageA number's nonnegative size, ignoring sign; for complex numbers it is distance from zero.
accessibilityGeneral or domain usageAccessibility is the extent to which people, including disabled people, can perceive, understand, navigate, and use information or a system.
accountability layerSystem-local specializationThe accountability layer is the evidence and source links that let someone check what the system says it did.
actor axesSystem-coined termActor axes are separate descriptions of an agent's access, abilities, tools, and role in a task.
admitted proof stepGeneral or domain usageAn admitted proof step is a gap temporarily accepted as an assumption instead of supplied with a proof.
affine functionGeneral or domain usageA linear function followed by a translation, such as x↦ax+b.
affordance rowSystem-coined termAn affordance row is a navigation entry that explains what an item is and what opening it lets you do.
agentGeneral or domain usageAn AI agent is software that uses a model and tools to carry out steps towards a task.
agent reliability and safetyGeneral or domain usageAgent reliability is how consistently an AI agent completes its intended task under the conditions in which it is used.
agent seedSystem-coined termAn agent seed is a saved record of an agent's observations and interpretations, with its author and sources identified.
agent traceGeneral or domain usageAn agent trace is a recorded sequence of events from an agent session, such as tool calls, outputs, and file operations.
AI-nativeGeneral or domain usageAI-native describes a system designed from the outset for AI to take part in its normal operation.
algebraic fieldGeneral or domain usageAn algebraic field supports addition, subtraction, multiplication, and division by nonzero elements under the usual commutative arithmetic laws.
algebraic numberGeneral or domain usageA complex number satisfying some nonzero polynomial equation with integer coefficients.
algorithmGeneral or domain usageAn algorithm is an explicit procedure for turning permitted inputs into outputs or decisions.
analytic continuationGeneral or domain usageAnalytic continuation extends a holomorphic function beyond its initial domain while agreeing with the original function wherever both are defined.
analytic functionGeneral or domain usageA function that near every point is represented by a convergent power series; over the complex numbers this is equivalent to being holomorphic.
annexSystem-local specializationAn annex is Plectis's source-linked account of ideas or techniques drawn from an outside project.
annulusGeneral or domain usageAn annulus is the region between two concentric circles, usually written {z: r<|z-a|<R} with 0≤r<R.
anti-principleSystem-local specializationAn anti-principle names a recurring shortcut or failure pattern that the system is meant to avoid.
Apache-2.0Externally anchoredApache-2.0 is an open-source licence allowing use, modification, and redistribution, including commercial use, subject to its conditions.
APIGeneral or domain usageAn API is a defined interface through which software requests operations or data from another software component.
appeal lifecycleSystem-coined termAn appeal lifecycle is the process for challenging a system decision and recording how the challenge was resolved.
applySystem-local specializationIn Plectis, apply is the step that makes a specified change to a file or record.
architectureGeneral or domain usageArchitecture is the high-level arrangement of a system’s parts, responsibilities, boundaries, constraints, and connections.
arithmetic progressionGeneral or domain usageA sequence obtained by repeatedly adding one fixed difference.
artifactGeneral or domain usageAn artifact is a stored item that someone can inspect or use, such as a file, report, dataset, or generated page.
artifact kindSystem-coined termAn artifact kind is a category of stored object, such as a standard, paper module, component, or result record.
assimilationSystem-coined termAssimilation is the process of incorporating a useful result into the system so later work can use it.
assistive technologyGeneral or domain usageAssistive technology is hardware or software that helps a disabled person perceive, operate, understand, or communicate with a system.
asymptotic boundGeneral or domain usageAn asymptotic bound compares the sizes of functions once their input is sufficiently large or approaches a specified limit.
asymptotic densityGeneral or domain usageThe limiting proportion of positive integers up to N that belong to a set.
asymptotic equivalenceGeneral or domain usageTwo functions are asymptotically equivalent at a specified limit if their ratio tends to one.
AtlasSystem-local specializationThe Atlas is Plectis's navigable map of the system's parts and their relationships.
Atom feedExternally anchoredAn Atom feed is an XML document for syndicating entries such as articles or updates, with identifying and descriptive metadata.
auditGeneral or domain usageAn audit is a systematic examination of records against stated requirements; here it often checks whether an agent's report matches its actions.
authenticationGeneral or domain usageAuthentication is the process of checking a claim about who or what an actor is.
authorityGeneral or domain usageAuthority is the recognised basis for settling a particular question or permitting an action.
authorizationGeneral or domain usageAuthorization determines which actions a person, program, or role is permitted to perform on specified resources.
axiomSystem-local specializationAn axiom is a starting assumption of a mathematical theory; Plectis also uses the word for a fundamental system rule.
backendGeneral or domain usageA backend is the processing, storage, and service layer behind a user-facing interface or another client.
bandSystem-local specializationA band is a named level of detail in a description, such as a brief label, a short summary, or a full explanation.
barrierGeneral or domain usageA mathematical barrier is an obstruction showing why a specified approach cannot establish its intended result under stated conditions.
baseGeneral or domain usageThe base of a power is the number being raised to an exponent. In a positional numeral system, powers of the base also determine place values.
basisGeneral or domain usageIn linear algebra, a basis gives unique vector coordinates; in an argument, its basis is the assumptions or evidence supporting it.
benchmarkGeneral or domain usageA benchmark is a specified workload and measurement procedure used to compare performance against a baseline or other systems.
big-o notationGeneral or domain usageBig-O notation bounds the magnitude of one quantity by a fixed constant times another near a specified limit.
bijectionGeneral or domain usageA bijection is a function that reaches every element of its codomain exactly once.
binary expansionGeneral or domain usageA binary expansion writes a number with digits 0 and 1, using powers of two as place values.
Boolean selectorGeneral or domain usageA Boolean selector is a sequence or function taking values 0 and 1 that records which objects are included.
boundGeneral or domain usageA bound is a value that a quantity is proved to stay above or below under stated conditions.
branch pointGeneral or domain usageA branch point is a location around which continuing a multivalued function can lead from one branch to another.
bridgeSystem-local specializationA bridge is Plectis's mechanism for sending a bounded task to an outside worker and returning its response.
bundleGeneral or domain usageA bundle is a group of related files packaged together for inspection or use.
cacheGeneral or domain usageA cache stores a reusable copy of data or a computed result so later access can avoid repeated work.
calibrationGeneral or domain usageCalibration compares measurements with a reference standard or compares stated forecast probabilities with observed event frequencies.
callbackGeneral or domain usageA callback is a function supplied to other code so that code can call it when a specified event or stage occurs.
canonicalisationExternally anchoredCanonicalisation is the process of putting something into a standard, representative form.
cardinalityGeneral or domain usageCardinality measures how many elements a set has, extending finite counting to infinite sets through bijections.
careSystem-local specializationCare means attending to the people, correctness, and future maintenance affected by a piece of work.
catalogSystem-local specializationA catalog is an organised inventory; on Plectis's architecture page it lists patterns available for use in the system.
cauchy–schwarz inequalityGeneral or domain usageThe absolute inner product of two vectors is at most the product of their lengths.
certificateGeneral or domain usageA certificate is data that a specified checker can use to verify a particular claim.
Challenge/Solution pairSystem-coined termA Challenge/Solution pair packages a precise Lean problem with a proposed solution that can be checked against it.
changelogGeneral or domain usageA changelog is a reader-facing record of notable changes between versions.
Chebotarev density theoremGeneral or domain usageThe Chebotarev density theorem says that primes with any prescribed Frobenius conjugacy class occur with a predictable positive density in a finite Galois extension.
checkGeneral or domain usageA check is an examination of whether something satisfies a stated condition.
checkerGeneral or domain usageA checker is a program or procedure that evaluates an input against specified rules.
Chinese remainder theoremGeneral or domain usageThe Chinese remainder theorem solves simultaneous congruences with pairwise coprime positive moduli.
circuit-breakGeneral or domain usageTo circuit-break a process is to interrupt a loop that would otherwise keep running or reinforcing itself.
claimGeneral or domain usageA claim is an assertion that can be examined for truth or support.
claim registrySystem-local specializationA claim registry is a structured list of assertions and the evidence, scope, and status attached to each.
clearing denominatorsGeneral or domain usageClearing denominators multiplies an equation or expression by a suitable nonzero common denominator to remove its fractions.
clientGeneral or domain usageA client is a program or device that requests data or a service from a server.
cloneGeneral or domain usageTo clone a repository is to create a local copy of its files and Git history, with options to limit what is downloaded.
closed routeSystem-local specializationA closed route is a recorded approach that has been ruled out within a stated set of assumptions or methods.
closed setGeneral or domain usageA set containing all of its limit points; equivalently, its complement is open.
closeoutSystem-local specializationA closeout is the final record of a unit of work: what changed, what was checked, and what remains unresolved.
closure of a setGeneral or domain usageThe smallest closed set containing a given set.
coarea formulaGeneral or domain usageThe coarea formula rewrites an integral over a region as integrals over level sets of a function, with a gradient factor accounting for how the levels are spaced.
Code MapSystem-coined termCode Map is a generated view of the code's parts and their dependencies.
coding agentGeneral or domain usageA coding agent is an AI agent equipped to work with source files and development tools.
codomainGeneral or domain usageThe codomain is the set in which a function's outputs are declared to lie.
coefficientGeneral or domain usageA number multiplying a variable, power, basis element, or series term.
coefficient sequenceGeneral or domain usageA coefficient sequence is the indexed list of coefficients in a series or expansion, including any zero coefficients.
cofinalGeneral or domain usageA subset of an ordered set is cofinal if it reaches at least as far as every element of that set.
cold agentSystem-coined termA cold agent starts a task without the earlier conversation or session context.
cold cloneSystem-local specializationA cold clone is a fresh repository checkout used to test whether someone new can follow the published instructions.
collaborationGeneral or domain usageCollaboration is people working together on a shared task or result.
combinatoricsGeneral or domain usageCombinatorics studies how discrete objects can be selected, arranged, counted, and related.
command shellGeneral or domain usageA command shell interprets commands and coordinates the programs, files, and data streams they act on.
command-line interfaceGeneral or domain usageA command-line interface lets someone control software through textual commands, usually with arguments and options.
commitGeneral or domain usageA Git commit records a complete repository-tree snapshot, parent link or links, and identifying metadata.
common senseSystem-local specializationIn Plectis, common sense means choosing a proportionate action using the task, available evidence, and relevant constraints.
compactGeneral or domain usageCompact means concise in the software descriptions, while mathematical compactness requires every open cover to have a finite subcover.
compactnessGeneral or domain usageA space is compact if every collection of open sets covering it has a finite subcollection that still covers it.
ComparatorGeneral or domain usageComparator is a Lean tool for checking a submitted solution against a separately specified challenge.
compatibility routeSystem-coined termA compatibility route keeps an old address or identifier usable after an item has moved or been renamed.
compiled binaryGeneral or domain usageA compiled binary is machine-readable output from compilation, such as an object file, library, bytecode module, firmware image, or executable.
compilerGeneral or domain usageA compiler translates one structured representation into another under defined transformation and checking rules.
complex numberGeneral or domain usageA number a+bi with real a,b and i²=-1.
complex planeGeneral or domain usageThe complex plane represents every complex number a+bi by the point with Cartesian coordinates (a,b).
compressionSystem-local specializationCompression reduces the amount of information needed to store, transmit, or read something.
compression profileSystem-coined termA compression profile specifies how one kind of material should be presented at different levels of detail.
computer scienceGeneral or domain usageComputer science is the study of computation, algorithms, information, and the systems that process them.
conceptSystem-local specializationA concept is an idea or category used to understand and organise a subject.
concurrencyGeneral or domain usageConcurrency is the organization of multiple tasks whose execution or waiting periods overlap.
conditional reductionGeneral or domain usageA conditional reduction proves that a target statement follows if a specified further condition holds.
conditional theoremGeneral or domain usageA conditional theorem proves a conclusion under stated hypotheses.
configurationGeneral or domain usageConfiguration is the set of selected values and options that determines how a program or system operates in a particular environment.
conformal mapGeneral or domain usageA conformal map preserves angles locally; in planar complex analysis, it is a holomorphic map with nonzero derivative.
congruenceGeneral or domain usageTwo integers are congruent modulo m if their difference is divisible by m.
conjectureGeneral or domain usageA conjecture is a precise mathematical claim proposed as true but not yet established by proof.
conjugacy classGeneral or domain usageThe conjugacy class of a group element g is the set {hgh⁻¹ : h in the group}.
connected componentGeneral or domain usageA connected component is a connected subset that cannot be enlarged while remaining connected within the surrounding space.
connected setGeneral or domain usageA set that cannot be split into two disjoint nonempty open pieces relative to that set.
context packetSystem-coined termA context packet is a selected collection of information supplied for a particular task.
context windowGeneral or domain usageA context window is the bounded sequence of tokens a language model can use during a generation.
continuous integrationGeneral or domain usageContinuous integration is the practice of frequently combining code changes and automatically checking that they work together.
contradictionGeneral or domain usageA contradiction is an impossibility obtained from assumptions, such as a statement and its negation both being true.
contrapositiveGeneral or domain usageIn classical logic, the contrapositive of “if P, then Q” is the equivalent statement “if not Q, then not P”.
contributeGeneral or domain usageTo contribute is to supply work that helps a shared project advance or correct itself.
contributor creditSystem-local specializationContributor credit records who supplied a piece of work and what that contribution was.
convergenceGeneral or domain usageConvergence means approaching a specified limit; for an infinite series, it means that its partial sums approach a finite value.
convex combinationGeneral or domain usageA weighted sum whose weights are nonnegative and add to one.
convex envelopeGeneral or domain usageThe convex envelope of a function is the greatest convex function that lies everywhere at or below the original function.
convex hullGeneral or domain usageThe convex hull of a set is the smallest convex set containing it, equivalently all finite weighted averages of its points with nonnegative weights summing to one.
convexityGeneral or domain usageA set is convex when it contains every line segment between its points; a function is convex when its graph lies at or below each chord joining two graph points.
coprimeGeneral or domain usageTwo integers are coprime if their greatest common divisor is 1.
corpusGeneral or domain usageA corpus is a collection of material studied or managed as a body of work.
counterexampleGeneral or domain usageA counterexample is a case that satisfies a claim's assumptions but makes its conclusion false.
coverageGeneral or domain usageCoverage is the measured portion of a declared population, requirement set, behavior space, or source surface that has been examined or represented.
covering mapGeneral or domain usageA covering map is a continuous surjection for which every target point has a neighbourhood whose preimage is a disjoint union of pieces, each mapped homeomorphically onto that neighbourhood.
credentialGeneral or domain usageA credential is evidence used to support a claim about identity, qualification, role, or authority.
critic postureSystem-coined termCritic posture is a deliberate way of examining an idea for weaknesses before relying on it.
critical pointGeneral or domain usageA critical point of a differentiable real or complex function is an input where its derivative vanishes; in several real variables, all first partial derivatives vanish there.
critical valueGeneral or domain usageA critical value is the output of a function at one of its critical points.
CSSGeneral or domain usageCSS is a language for describing how structured documents are presented.
curve parametrisationGeneral or domain usageA function from a parameter interval into a space whose image traces a curve.
cyclotomic polynomialGeneral or domain usageThe nth cyclotomic polynomial is the monic integer polynomial whose roots are exactly the primitive nth roots of unity.
data fieldGeneral or domain usageA data field is a named part of a structured record that holds a value with an expected meaning and form.
databaseGeneral or domain usageA database is an organized collection of data maintained so it can be accessed, queried, and updated.
datasetGeneral or domain usageA dataset is an organized collection of observations or records intended to be considered together.
declarationGeneral or domain usageA declaration introduces a named item in a programming or proof language, such as a definition, theorem, or structure.
definite integralGeneral or domain usageA definite integral accumulates a function’s values over a specified region using a rule for measuring that region.
degree of a polynomialGeneral or domain usageThe degree of a nonzero polynomial is the highest exponent with a nonzero coefficient.
Demo TakeSystem-coined termDemo Take is the system's recording tool for capturing a demonstration and its accompanying material.
denominatorGeneral or domain usageThe denominator is the divisor in a fraction: the b in a/b, where b is nonzero.
dense subsetGeneral or domain usageA subset whose closure is the whole surrounding space.
dependencyGeneral or domain usageA dependency is an object, service, fact, or earlier result that another component or conclusion requires.
deploymentGeneral or domain usageDeployment places a software version or configuration into an environment where it can run or serve users.
derivationGeneral or domain usageA derivation is a sequence of justified steps leading from stated starting points to a result.
derivation certificateSystem-coined termA derivation certificate is an inspectable record that lets a checker verify how a particular claim follows from its stated basis.
derivativeGeneral or domain usageA derivative is the linear map that approximates a function's change to first order near a point.
determinantGeneral or domain usageA determinant is a scalar computed from a square matrix; over a field, it is nonzero exactly when the matrix is invertible.
deterministicGeneral or domain usageA deterministic process produces the same output whenever all relevant inputs and operating conditions are the same.
Diebold-Mariano testGeneral or domain usageThe Diebold–Mariano test assesses whether two forecasting methods have equal expected loss under a chosen measure of error.
differentiable functionGeneral or domain usageA function with a linear first-order approximation at each point under discussion.
digestGeneral or domain usageA cryptographic digest is a fixed-size value computed from data, used to detect whether the data has changed.
digestionExternally anchoredMathematical digestion is the process of understanding a result well enough to place it in the field and use it in further work.
dimensionGeneral or domain usageA vector space has dimension equal to the size of a basis; geometric notions such as Hausdorff dimension use different definitions.
dirichlet convolutionGeneral or domain usageThe arithmetic-function product (f*g)(n)=Σ_{d|n}f(d)g(n/d).
Dirichlet energyGeneral or domain usageThe Dirichlet energy of a sufficiently regular function u on a region is the integral of |∇u|²; for complex maps it measures the total squared stretching.
dirichlet's theorem on primes in arithmetic progressionsGeneral or domain usageDirichlet’s theorem says that every residue class a modulo a positive integer q with gcd(a,q) = 1 contains infinitely many primes.
discrete mathematicsGeneral or domain usageDiscrete mathematics studies objects with separate elements, such as integers, graphs, and finite arrangements.
discriminantGeneral or domain usageA discriminant detects repeated roots or arithmetic degeneracy: a polynomial’s discriminant vanishes exactly when it has a repeated root, while a number field’s discriminant records how its integral arithmetic behaves modulo primes.
distanceGeneral or domain usageA distance assigns zero to identical points, positive values to distinct points, and obeys symmetry and the triangle inequality.
divergenceGeneral or domain usageA sequence or series diverges when it does not converge in the sense being considered.
divisibilityGeneral or domain usageDivisibility is the relation in which one integer is an exact integer multiple of another.
divisorGeneral or domain usageAn integer d is a divisor of an integer n when n = d·k for some integer k.
divisor transformGeneral or domain usageThe divisor transform sends an arithmetic function a to b(n)=Σ_{d|n}a(d), summing its values over every positive divisor of n.
doctrineSystem-local specializationIn Plectis, doctrine is the organised set of ideas and rules explaining how the system is intended to work.
Document Object ModelGeneral or domain usageThe Document Object Model, or DOM, represents a document as a tree of objects and provides an interface for reading and changing it.
DOIExternally anchoredA DOI is a persistent identifier for an object such as a paper, dataset, or software release.
domain expertGeneral or domain usageA domain expert is someone with substantial knowledge and judgement in a particular field.
driftSystem-local specializationDrift is a mismatch that develops between things expected to agree, such as a generated page and its source.
drilldownGeneral or domain usageA drilldown opens a more detailed view of something shown in a summary.
dyadicGeneral or domain usageDyadic means related to powers of two, often fractions or intervals built from them.
dyadic sectionGeneral or domain usageA dyadic section of a sequence a(n) is a subsequence a(2ᵉn+r) obtained by fixing the index modulo a power of two.
empirical distributionGeneral or domain usageAn empirical distribution puts equal weight on each observation in a finite sample, adding weights when values repeat.
endogenousGeneral or domain usageEndogenous means originating within the system or process being discussed.
endpointGeneral or domain usageAn endpoint is a defined end of a connection, process, path, or investigation; its exact meaning depends on context.
engine roomSystem-local specialization“Engine room” is the site's informal label for components that operate and maintain the system itself.
entrySystem-local specializationIn the navigation descriptions, an entry is either a starting route or an individual item in a collection.
environmentGeneral or domain usageAn environment is the surrounding technical, physical, and procedural conditions under which work runs or an observation is made.
epistemic control planeSystem-coined termThe epistemic control plane is a proposed system layer that uses evidence and uncertainty to govern which actions may proceed.
equalityGeneral or domain usageAn equality states that two expressions represent the same value or mathematical object.
equationGeneral or domain usageAn equation is a mathematical statement that two expressions are equal.
equidistributionGeneral or domain usageA sequence is equidistributed in a region when the long-run proportion of its terms in each suitable subregion equals that subregion’s relative size.
equivalenceGeneral or domain usageTwo statements are logically equivalent when each implies the other under the same assumptions.
Paul ErdősExternally anchoredPaul Erdős was a mathematician known for work in number theory, combinatorics, probability, and related fields.
Erdős problemExternally anchoredAn Erdős problem is a mathematical question associated with Paul Erdős; this site uses the numbering of the Erdős Problems database.
euler productGeneral or domain usageAn Euler product expresses a quantity as a product of factors associated with individual primes.
Euler's theorem (modular arithmetic)General or domain usageEuler's theorem says that if a is coprime to a positive integer n, then a raised to φ(n) is congruent to 1 modulo n.
evaluatorGeneral or domain usageAn evaluator is a tool or procedure that assesses something against chosen criteria.
event listenerGeneral or domain usageAn event listener is code registered to receive notification when a specified event occurs.
eventual propertyGeneral or domain usageAn eventual property holds at every index after some finite threshold.
evidenceGeneral or domain usageEvidence is information that supports or challenges a particular claim.
evidence bandSystem-local specializationAn evidence band labels the kind of support attached to a statement in a mathematical working record.
exact rational arithmeticGeneral or domain usageExact rational arithmetic calculates with integer numerators and denominators instead of rounded decimal values.
executable cross-sectionSystem-coined termAn executable cross-section is a selected part of a larger system that can be run and inspected on its own.
executionGeneral or domain usageExecution is the running of instructions or the actual performance of a planned operation.
existential quantifierGeneral or domain usageAn existential quantifier states that at least one element of a specified domain satisfies a property.
exit codeGeneral or domain usageAn exit code is the small numeric status a process returns when it finishes.
exogenousGeneral or domain usageExogenous means originating outside the system or process under discussion.
exogenous truthGeneral or domain usage“Exogenous truth” is this project's phrase for judgement brought in from outside the process being judged.
exponentGeneral or domain usageAn exponent specifies a power: in bⁿ, b is the base and n is the exponent.
exponential backoffGeneral or domain usageExponential backoff is a retry schedule that increases the delay after each consecutive failure, usually by multiplying it by a fixed factor.
exponential growthGeneral or domain usageExact exponential growth multiplies a positive quantity by the same factor greater than one at each step.
exponential sumGeneral or domain usageAn exponential sum is a finite sum of complex phases, commonly Σ a_n exp(2πi f(n)), used to measure cancellation or arithmetic regularity.
expositionExternally anchoredMathematical exposition explains a result, its proof, and why the argument works for its intended readers.
factorGeneral or domain usageA factor is one of the quantities multiplied together to make a product.
factorialGeneral or domain usageThe factorial of a nonnegative integer n is the product of the integers from 1 through n, with the value at zero defined as 1.
factorisationGeneral or domain usageFactorisation writes a number or algebraic expression as a product of simpler factors.
fail-closedSystem-coined termFail-closed means withholding an action when a required condition cannot be established.
failure class propagationSystem-coined termFailure-class propagation checks whether a discovered fault also affects other cases for the same reason.
failure modesGeneral or domain usageFailure modes are the distinct ways something can fail to meet its intended purpose.
fallbackGeneral or domain usageA fallback is an alternative behavior used when a preferred route is unavailable, unsuitable, or fails.
falsifiableGeneral or domain usageA claim is falsifiable when some possible evidence could count against it under stated assumptions.
Farey sequenceGeneral or domain usageThe Farey sequence of order N lists all reduced fractions between 0 and 1 whose positive denominators are at most N.
feedback loopGeneral or domain usageA feedback loop occurs when a process's output influences its later behaviour.
field extensionGeneral or domain usageA field extension L/K is a larger field L containing a copy of a field K and using the same addition and multiplication on K.
field of fractionsGeneral or domain usageThe field of fractions Frac(A) of an integral domain A consists of ratios a/b with a,b∈A and b≠0, identifying ratios that represent the same value.
finiteGeneral or domain usageA set is finite if its elements can be counted by a nonnegative integer.
finite computationGeneral or domain usageA finite computation is a calculation that completes after finitely many steps.
finite truncationGeneral or domain usageA finite truncation keeps a specified finite part of an otherwise longer or infinite object.
fixtureGeneral or domain usageA test fixture supplies the inputs, state, or environment used for a test.
floor functionGeneral or domain usageThe floor of a real number x, written ⌊x⌋, is the greatest integer less than or equal to x.
focus managementGeneral or domain usageFocus management is the deliberate control of which interactive element receives keyboard input and where focus moves after an interface changes.
forecastingGeneral or domain usageForecasting produces claims about unknown future outcomes, often with probabilities or ranges.
formalGeneral or domain usageFormal means expressed within explicitly specified rules; in mathematics, it usually concerns a precise logical language and inference system.
formal mathematicsGeneral or domain usageFormal mathematics expresses definitions, statements, and proofs in a language governed by explicit logical rules.
formal proofGeneral or domain usageA formal proof is a derivation expressed precisely enough to be checked against a formal system's inference rules.
formal verificationGeneral or domain usageFormal verification uses mathematical methods to establish that a system or proof satisfies a precise specification.
formalisationGeneral or domain usageFormalisation expresses definitions, statements, or arguments in a language with explicit rules for their meaning and use.
forward-invariant setGeneral or domain usageA set is forward invariant when trajectories starting in it remain there for as long as their forward evolution is defined.
fractionGeneral or domain usageA fraction writes a quotient as a/b; for a rational number, a and b are integers and b is nonzero.
fractional partGeneral or domain usageFor a real number x, its fractional part is x minus the greatest integer at most x, so it lies in [0,1).
freshnessSystem-local specializationFreshness describes whether stored information still reflects the source or state it is meant to represent.
Frobenius automorphismGeneral or domain usageIn characteristic p, Frobenius sends x to x^p; it is an automorphism when this power map is onto, as it always is for a finite field.
Frobenius elementGeneral or domain usageA Frobenius element is a field symmetry attached to an unramified prime in a finite Galois extension of number fields; it describes a power map after reduction modulo a chosen prime above it.
frontendGeneral or domain usageA front end is the part of a software system through which a user interacts with it.
frontierSystem-local specializationHere, the mathematical frontier is the stated boundary between established results and unresolved questions for a problem.
functionGeneral or domain usageA mathematical function assigns one output to each allowed input; a software function is a callable piece of code.
function compositionGeneral or domain usageFunction composition applies one function to the output of another.
function domainGeneral or domain usageThe domain of a function is the set of inputs on which that function is defined.
Galois extensionGeneral or domain usageA Galois extension L/K is an algebraic field extension that is normal, so it contains every conjugate root required by its equations over K, and separable, so those roots are distinct.
Galois groupGeneral or domain usageThe Galois group Gal(L/K) is the group of field automorphisms of L that fix every element of K.
gateGeneral or domain usageA gate is a checkpoint that permits an action only when specified conditions are satisfied.
Gaussian binomial coefficientGeneral or domain usageA Gaussian binomial coefficient is the q-analogue of an ordinary binomial coefficient, written [n choose k]_q and defined by a product of q-power differences.
generalise-up-propagateSystem-coined termGeneralise-up-propagate means turning a supported local lesson into guidance that future relevant work will actually encounter.
geometric majorantGeneral or domain usageA geometric majorant bounds terms or their magnitudes by a geometric sequence with a fixed ratio.
geometric seriesGeneral or domain usageA geometric series adds terms formed by repeatedly multiplying an initial value by a fixed number.
GitExternally anchoredGit is a version-control system that records snapshots of files and the history connecting them.
Git branchGeneral or domain usageA Git branch is a movable name that points to a commit and normally advances along one line of repository history.
GitHubExternally anchoredGitHub is a service for hosting Git repositories and tools for collaboration around them.
governGeneral or domain usageTo govern a process is to define how its decisions are made, authorised, and checked.
gradientGeneral or domain usageFor a differentiable real-valued function in Euclidean coordinates, the gradient is the vector of its first partial derivatives.
Gram matrixGeneral or domain usageThe Gram matrix of vectors v₁,…,vₙ has entries Gᵢⱼ=⟨vᵢ,vⱼ⟩, recording every pairwise inner product.
graphGeneral or domain usageA graph can mean vertices joined by edges, or the set of input–output pairs of a function.
graph edgeGeneral or domain usageA graph edge connects vertices according to the graph’s declared relation.
graph nodeGeneral or domain usageA graph node, also called a vertex, is one of the objects that a graph’s edges can connect.
greatest common divisorGeneral or domain usageFor integers not all zero, the greatest common divisor is the largest positive integer dividing every one of them.
groundingGeneral or domain usageGrounding connects a statement or decision to the information that gives it meaning and support.
guinea pigGeneral or domain usage“Guinea pig” is an informal term for a person or case on which an experimental method is tried.
hard-codedGeneral or domain usageHard-coded means a value or choice is written directly into code or content instead of being supplied through configuration, input, or a separate source.
harmonic extensionGeneral or domain usageA harmonic extension fills boundary data into a domain by a harmonic function that takes those boundary values, when the relevant Dirichlet problem is solvable.
harmonic functionGeneral or domain usageA harmonic function has continuous second derivatives and a zero Laplacian, the sum of its pure second partial derivatives.
harnessGeneral or domain usageA test harness is the code and setup that runs a test and captures its result.
hausdorff measureGeneral or domain usageA size measure built from arbitrarily fine coverings, extending length, area, and fractal dimension ideas.
hessian matrixGeneral or domain usageThe square matrix of second partial derivatives of a scalar-valued function.
heuristicGeneral or domain usageA heuristic is a practical rule or method that often finds a useful answer without guaranteeing the best or correct answer.
hologramSystem-local specializationIn Plectis, “hologram” means a structured, compressed view that preserves routes into the material it summarises.
holomorphic functionGeneral or domain usageA complex-valued function having a complex derivative at every point of an open region.
HTMLExternally anchoredHTML is the markup language used to describe the structure and meaning of web-page content.
HTTP and HTTPSGeneral or domain usageHTTP is the web protocol for exchanging requests and responses; HTTPS is HTTP carried through an authenticated encrypted connection.
hyperbolic distanceGeneral or domain usageIn the unit-disc model, hyperbolic distance is the shortest path length measured with increasing stretching near the boundary.
hypothesisGeneral or domain usageA mathematical hypothesis is an assumption under which a statement is being considered or proved.
IDEGeneral or domain usageAn IDE, or integrated development environment, is an application combining tools for working on software.
idempotencyGeneral or domain usageIdempotency is the property that repeating an operation with the same intended input has the same effect as performing it once.
identifierGeneral or domain usageAn identifier is a name or code used to distinguish one object from others within a stated system.
image of a functionGeneral or domain usageThe set of output values a function actually attains.
immutableGeneral or domain usageImmutable describes a value or record that cannot be changed after it is created.
implementationGeneral or domain usageAn implementation is a concrete realization of a design, specification, algorithm, interface, or policy.
implicationGeneral or domain usageAn implication says that if one statement holds, another follows.
indexGeneral or domain usageAn index identifies a member of an indexed family or provides a lookup structure for locating information.
inequalityGeneral or domain usageAn inequality compares quantities using an order relation such as <, ≤, >, or ≥.
infimumGeneral or domain usageThe largest number less than or equal to every member of a set.
infiniteGeneral or domain usageAn infinite set has more elements than any finite set; no finite count exhausts it.
injective mapGeneral or domain usageA function that never sends two different inputs to the same output.
inner productGeneral or domain usageAn inner product pairs two vectors to measure their lengths and relative directions through an algebraic operation.
inspectionSystem-local specializationInspection means examining the actual material closely enough to assess a specific question about it.
integerGeneral or domain usageAn integer is one of the numbers …, −2, −1, 0, 1, 2, … .
integral basisGeneral or domain usageAn integral basis is a basis over the integers: every element of the relevant free abelian group has a unique finite integer linear combination of the basis vectors.
integral curveGeneral or domain usageAn integral curve of a vector field is a parametrised curve whose velocity agrees with that field at every point.
intelligentGeneral or domain usageIntelligent ordinarily describes an ability to learn, reason, understand, or adapt to a task.
interfaceGeneral or domain usageAn interface is a defined boundary through which a person, program, or component interacts with another system.
invariantGeneral or domain usageAn invariant is a quantity or property preserved by specified transformations or steps of a process.
inverse branchGeneral or domain usageA single-valued local choice of inverse for a map that may have several preimages globally.
inverse functionGeneral or domain usageAn inverse function undoes a function, returning each output to the unique input that produced it.
irrationalGeneral or domain usageA real number is irrational if it cannot equal a/b for any integers a and nonzero b.
irrationality criterionGeneral or domain usageAn irrationality criterion is a proved condition that can be used to establish that a number is irrational.
irrationality exponentGeneral or domain usageThe irrationality exponent is the supremum of the approximation powers achieved infinitely often by rational approximations to an irrational number.
jacobian matrixGeneral or domain usageThe matrix of all first partial derivatives of a map between finite-dimensional coordinate spaces.
JavaScriptGeneral or domain usageJavaScript is a programming language used in web browsers and many server and tooling environments.
jitterGeneral or domain usageJitter is variation in timing. In a retry schedule, deliberate random variation spreads requests out so clients do not all retry together.
jordan domainGeneral or domain usageA Jordan domain is the bounded open region enclosed by a simple closed curve in the plane.
JSONExternally anchoredJSON is a text format for representing structured values as objects, arrays, strings, numbers, booleans, and null.
kernelSystem-local specializationA kernel is a system's central core; this site uses the word for both Lean's proof checker and Plectis's command router.
Koebe distortion theoremGeneral or domain usageThe Koebe distortion theorem gives explicit bounds on the size and derivative of a normalized univalent holomorphic function inside the unit disc.
laboratorySystem-local specializationIn Plectis, a laboratory is a controlled setting for trying a proposed mechanism before relying on it in live work.
Lambert seriesGeneral or domain usageA Lambert series has the form ∑ aₙxⁿ/(1 − xⁿ), usually summed over positive integers n where it converges.
large language modelGeneral or domain usageA large language model is a statistical model trained to predict and generate sequences of tokens from context.
latencyGeneral or domain usageLatency is the elapsed time between the start of an action or request and a defined response or completion point.
LaTeXExternally anchoredLaTeX is a system for writing structured documents that a typesetting engine turns into formatted output, usually a PDF.
latticeSystem-local specializationIn Plectis, the lattice is the network of relationships between rules, skills, concepts, code, and evidence.
lattice transpositionSystem-coined termLattice transposition moves a reusable lesson into the kind of system record that can apply it to future work.
launch-scope decisionSystem-local specializationA launch-scope decision determines what is ready and authorised to be published or made available.
lay personSystem-local specializationA lay person is someone who is not a specialist in the subject being discussed.
LeanGeneral or domain usageLean is a programming language and proof assistant used to state mathematics and check formal proofs.
Lean kernelGeneral or domain usageThe Lean kernel is the core that checks whether a formal proof object has the type claimed for it.
Lean's standard axiomsGeneral or domain usageLean's usual mathematical foundations include propositional extensionality, quotient soundness, and classical choice.
least common multipleGeneral or domain usageFor positive integers, the least common multiple is the smallest positive integer divisible by all of them.
Lebesgue measureGeneral or domain usageLebesgue measure generalises length on the real line, area in the plane, and volume in higher dimensions.
lemmaGeneral or domain usageA lemma is a proved statement introduced mainly to support another argument.
lemniscateGeneral or domain usageA polynomial lemniscate is a set defined by the size of a complex polynomial, commonly the curve |p(z)| = c.
length of a curveGeneral or domain usageA curve’s length is the supremum of the lengths of polygonal paths through successive points on the curve.
level curveGeneral or domain usageA level curve is a curve along which a real-valued function has a constant value.
level setGeneral or domain usageA level set consists of all points where a function has one specified value.
limitGeneral or domain usage“Limit” can mean a restriction or, in mathematics, the value approached by a sequence or function.
limit inferiorGeneral or domain usageThe limit inferior is the limiting lower bound obtained by discarding longer and longer finite beginnings of a sequence.
limit superiorGeneral or domain usageThe limit superior is the limiting upper bound obtained by discarding longer and longer finite beginnings of a sequence.
lineageGeneral or domain usageLineage records where an item came from and which transformations led to its present form.
linear combinationGeneral or domain usageA linear combination is a finite sum of vectors multiplied by scalar coefficients.
linear formGeneral or domain usageA linear form is an expression a₁x₁+⋯+aₙxₙ, or equivalently a linear map from a vector space to its scalar field.
linear independenceGeneral or domain usageA family is linearly independent if no finite combination of its members equals zero unless every scalar coefficient is zero.
linear mapGeneral or domain usageA linear map preserves vector addition and multiplication by scalars.
little-o notationGeneral or domain usageA comparison saying one quantity becomes negligible relative to another.
living system postureSystem-coined termLiving system posture means treating claims about a changing system as statements about an identifiable state or version.
locusGeneral or domain usageA locus is a place where something occurs or is defined; in mathematics, it can mean all points satisfying a condition.
log fileGeneral or domain usageA log file stores timestamped or ordered records produced while a program, service, or job runs.
logarithmGeneral or domain usageFor a positive base b other than 1, the real logarithm log_b(x) is the exponent y satisfying bʸ = x, for x > 0.
lower semicontinuityGeneral or domain usageLower semicontinuity means a function’s value at a limit point is no larger than the limit inferior of nearby values.
machine-checkedGeneral or domain usageMachine-checked means software has verified a stated property of the supplied material.
machine-readableGeneral or domain usageMachine-readable information is structured so software can reliably parse and act on it.
manifestGeneral or domain usageA manifest is a structured inventory of the files or objects included in a build, package, or release.
mapGeneral or domain usageA map presents a collection and the relationships that help someone navigate it.
mathematical continuityGeneral or domain usageA function is continuous when sufficiently close inputs always produce sufficiently close outputs.
mathematical inductionGeneral or domain usageMathematical induction proves a claim for every natural-number index by establishing a starting case and a valid step to the next case.
mathematical limitGeneral or domain usageA mathematical limit describes the value a sequence or function approaches as its index or input approaches a specified point or infinity.
mathematical priorityGeneral or domain usageMathematical priority concerns who first established or discovered a result, as supported by the scholarly record.
mathematicianSystem-local specializationA mathematician studies mathematical structures and questions through definitions, reasoning, and proof.
mathematicsGeneral or domain usageMathematics studies patterns, quantities, structures, and relationships through precise definitions and logical reasoning.
MathlibExternally anchoredMathlib is the community-maintained library of mathematical definitions, theorems, and tools for Lean.
matrixGeneral or domain usageA matrix is a rectangular array of entries, often representing numerical data, simultaneous equations, or a linear map.
maximal idealGeneral or domain usageA maximal ideal is a proper ideal contained in no larger proper ideal. In a commutative ring with identity, quotienting by it gives a field.
maximum principleGeneral or domain usageA maximum principle says that a function satisfying specified equations or inequalities cannot have a strict interior maximum, and often places its largest value on the boundary.
mechanismSystem-local specializationA mechanism is the process or arrangement through which an outcome is produced.
mechanism contractSystem-coined termA mechanism contract states what a component is expected to do and how that expectation can be checked.
Mersenne numberGeneral or domain usageA Mersenne number has the form 2ⁿ − 1 for a positive integer n.
metabolismSystem-local specialization“Metabolism” is Plectis's name for the recurring work that keeps stored knowledge and generated views in step with their sources.
metadataGeneral or domain usageMetadata is information that describes other data, a file, a record, or an event.
metadata-onlySystem-local specializationMetadata-only means a record contains information about material or a run without including the underlying bodies themselves.
metricGeneral or domain usageA metric is either a defined performance measure or, in mathematics, a distance function satisfying the metric axioms.
metric spaceGeneral or domain usageA metric space is a set equipped with a distance satisfying the standard rules of separation, symmetry, and the triangle inequality.
MicrocosmCompatibility identifierMicrocosm is an earlier public name for Plectis that remains in some technical paths and compatibility identifiers.
miningSystem-local specializationHere, “mining” means sustained searching through candidate arguments and experiments for useful mathematical results or failures.
minor of a matrixGeneral or domain usageA determinant obtained by selecting equally many rows and columns from a matrix.
modelGeneral or domain usageA model is a representation used to describe, predict, or reason about something.
moduleGeneral or domain usageA module is a unit of code or written material organised around a subject or responsibility.
modulusGeneral or domain usageModulus means the integer defining a modular-arithmetic relation, or the magnitude of a complex number.
monicGeneral or domain usageA polynomial is monic if its leading coefficient is 1.
monodromyGeneral or domain usageMonodromy describes how a locally defined branch changes when analytically continued around loops; the monodromy theorem gives path independence under suitable simply connected hypotheses.
monodromy theoremGeneral or domain usageThe monodromy theorem says that a holomorphic function defined near one starting point extends to a single-valued function on a simply connected domain if it can be continued along every path there.
monotone sequenceGeneral or domain usageA monotone sequence is either nondecreasing at every step or nonincreasing at every step.
Morse chartGeneral or domain usageA Morse chart is a local coordinate system near a nondegenerate critical point in which a smooth function becomes a quadratic form with plus and minus squares.
Morse saddleGeneral or domain usageA Morse saddle is a critical point of a smooth real-valued function whose second-order form is nondegenerate and has both positive and negative directions.
multipleGeneral or domain usageIn arithmetic, a multiple of an integer d is a number d·k for some integer k.
multiple rootGeneral or domain usageA multiple root of a nonzero polynomial is a root appearing with multiplicity at least two.
multiplicative functionGeneral or domain usageAn arithmetic function f is multiplicative if f(1) = 1 and f(mn) = f(m)f(n) whenever m and n are coprime.
multiplicative orderGeneral or domain usageFor b coprime to a positive modulus Q, the multiplicative order is the least positive k for which bᵏ ≡ 1 modulo Q.
mutableGeneral or domain usageMutable describes a value, object, or record that can change after it is created.
möbius functionGeneral or domain usageThe Möbius function μ assigns each positive integer a value determined by its prime factorisation: zero for repeated prime factors, otherwise a sign.
named basisSystem-local specializationA named basis identifies the exact inputs, assumptions, or sources on which a claim rests.
namespaceGeneral or domain usageA namespace is a scope within which names identify objects without colliding with the same names used elsewhere.
natural numberGeneral or domain usageA natural number is a counting number; in Lean, the natural numbers include zero: 0, 1, 2, 3, … .
necessary and sufficientGeneral or domain usageA condition is necessary and sufficient for a statement when each implies the other.
negative caseSystem-local specializationA negative case is a test input designed to exercise a failure or refusal that the system should detect.
neighbourhoodGeneral or domain usageA set containing an open set around a specified point or subset.
Newton flowGeneral or domain usageFor a complex polynomial p, the Newton flow studied here follows the differential equation z′ = −p(z)/p′(z) where p′(z) ≠ 0.
Newton vector fieldGeneral or domain usageThe Newton vector field assigns the velocity −p(z)/p′(z) to points where the polynomial derivative p′ is nonzero.
nonsingular matrixGeneral or domain usageA square matrix over a field is nonsingular when it has an inverse, equivalently when its determinant is nonzero.
normGeneral or domain usageA norm measures a vector’s size, is zero only at zero, scales with absolute scalar size, and satisfies the triangle inequality.
normal extensionGeneral or domain usageAn algebraic extension L/K is normal when every irreducible polynomial over K having one root in L splits completely into linear factors over L.
normal formGeneral or domain usageA normal form is a specified standard representation of an object, expression, statement, or record.
normalised vanishingGeneral or domain usageNormalised vanishing means that a quantity tends to zero after division by a specified nonzero scale.
nowhere denseGeneral or domain usageA set is nowhere dense if its closure has empty interior.
number theoryGeneral or domain usageNumber theory studies integers and their arithmetic relationships, including primes, divisibility, and congruences.
numeratorGeneral or domain usageThe numerator is the quantity being divided in a fraction: the a in a/b.
OBS StudioExternally anchoredOBS Studio is a free, open-source application for video recording and live streaming.
observabilityGeneral or domain usageObservability is either unique state reconstruction from outputs in control theory or the practical ability to investigate a running system from recorded signals.
observeSystem-local specializationIn Plectis, observe is the step that gathers and records information without changing the material being examined.
omission receiptSystem-coined termAn omission receipt records what a shortened view leaves out and how to recover the fuller material.
open coverGeneral or domain usageAn open cover of a set is a collection of open sets whose union contains that set.
open obligationSystem-local specializationAn open obligation is a precise requirement that remains to be established in an argument or workflow.
open problemGeneral or domain usageAn open problem is a mathematical question for which no accepted resolution is known in the relevant literature.
open setGeneral or domain usageA set containing a small neighbourhood around each of its points.
open-worldSystem-coined termAn open-world approach treats missing information as unknown rather than automatically false.
operator proxySystem-coined termAn operator proxy carries out a bounded task on the operator's behalf using supplied instructions and context.
operator voiceSystem-local specializationOperator voice is the preserved record of what the human operator actually said or wrote.
option surfaceSystem-coined termAn option surface is a structured view of the items or actions available within a category.
orbitGeneral or domain usageAn orbit is the path of an object under repeated application of a rule or continuous evolution through time.
orientationGeneral or domain usageOrientation gives a new reader the context needed to understand what they are looking at and where to go next.
orphanGeneral or domain usageAn orphan is an item that exists but lacks the expected connection to its index, parent, or related records.
p-adic valuationGeneral or domain usageThe p-adic valuation of a nonzero integer counts how many factors of the prime p divide it.
packageGeneral or domain usageA package groups related material so it can be distributed, installed, or used as a unit.
packetGeneral or domain usageA packet is a selected bundle of information prepared for a particular reader or task.
PalomarExternally anchoredPalomar is an external registry used to present formally checked mathematical results with identifiable source and checking records.
paperSystem-local specializationA mathematical paper presents a question, argument, or result in a form intended for readers to study and assess.
paper moduleSystem-coined termA paper module is Plectis's maintained explanation of one subsystem or recurring mechanism.
parserGeneral or domain usageA parser reads input according to a grammar and produces a structured representation or a syntax error.
Parseval identityGeneral or domain usageParseval’s identity says that the squared norm of a function equals the sum of squared magnitudes of its orthogonal Fourier coefficients, with normalization fixed by convention.
partial sumGeneral or domain usageA partial sum adds finitely many terms from the beginning of a series.
passionSystem-local specializationIn Plectis's description of judgement, passion means keeping the purpose and human importance of the work in view.
path connectedGeneral or domain usageA set is path connected if any two of its points can be joined by a continuous path entirely within the set.
path handleSystem-coined termA path handle is a stable short name that resolves to a file or other source location.
payloadGeneral or domain usageA payload is the main data carried by a message, request, event, file wrapper, or test fixture.
PDFExternally anchoredPDF is a document format designed to preserve a page's layout across different devices and applications.
peerSystem-local specializationA peer is another participant working at a comparable level or within a shared activity.
peer reviewGeneral or domain usagePeer review is evaluation of scholarly work by other people with relevant expertise, usually within a publication or assessment process.
peer-propagateSystem-coined termA peer-propagate record passes an attributed operating lesson from one agent to later agents.
perfect setGeneral or domain usageA perfect set is closed and has no isolated points.
periodicGeneral or domain usageA sequence is periodic if shifting it by some fixed positive number of positions leaves every term unchanged.
permissionGeneral or domain usagePermission is an allowance for an actor to perform an action, within whatever scope and conditions apply.
phaseSystem-local specializationA phase is a defined stage of work; in Plectis, it carries the objective and state of a resumable work programme.
pipExternally anchoredpip is a package installer for Python.
pipelineGeneral or domain usageA pipeline is an organized set of processing stages that move or transform work from inputs toward outputs.
planted errorGeneral or domain usageA planted error is a deliberate fault added to a test to see whether a check detects it.
planted forgeryGeneral or domain usageA planted forgery is deliberately false evidence or reporting placed in a controlled test input.
polynomialGeneral or domain usageA finite sum of constant multiples of nonnegative whole-number powers of a variable.
positive integerGeneral or domain usageA positive integer is one of 1, 2, 3, … .
positive-definite matrixGeneral or domain usageA real symmetric or complex Hermitian matrix A is positive definite when x*Ax>0 for every nonzero vector x.
positive-semidefinite matrixGeneral or domain usageA real symmetric or complex Hermitian matrix A is positive semidefinite when x*Ax≥0 for every vector x.
power seriesGeneral or domain usageA power series adds constant coefficients multiplied by successive nonnegative integer powers of a variable’s offset from a centre.
preimageGeneral or domain usageAll inputs that a function sends into a specified output set.
premiseGeneral or domain usageA premise is a statement taken as a starting point for an argument, whether proved, observed, assumed, or hypothetical.
primeGeneral or domain usageA prime number is an integer greater than 1 whose only positive divisors are 1 and itself.
prime gapGeneral or domain usageA prime gap is the difference between consecutive prime numbers.
prime idealGeneral or domain usageA prime ideal p in a commutative ring R is a proper ideal such that ab∈p implies a∈p or b∈p.
prime powerGeneral or domain usageA prime power is a number pᵏ where p is prime and k is a positive integer.
principleSystem-local specializationA principle is a general rule or commitment that guides decisions.
prior artGeneral or domain usagePrior art is earlier work relevant to whether a claimed idea, method, or result is new.
privacyGeneral or domain usagePrivacy concerns boundaries around access to a person, their activities, and information about them.
probability distributionGeneral or domain usageA probability distribution specifies the probabilities of possible outcomes or sets of outcomes.
problem noteSystem-local specializationA problem note is a focused mathematical write-up about one problem and the work done on it.
producerSystem-local specializationA producer is the person, model, or program that generates an output.
productGeneral or domain usageIn mathematics, a product is the result of multiplication; in software discussions, it can mean an offering intended for users.
profile gapSystem-coined termA profile gap marks missing support for presenting a kind of system object at the promised levels of detail.
programGeneral or domain usageA computer program is a set of instructions that a computing system can execute.
progressive enhancementGeneral or domain usageProgressive enhancement starts with usable core content and adds richer presentation or interaction when the browser supports it.
projectionGeneral or domain usageA projection produces a selected representation of something, such as a source-derived view or a mathematical map onto chosen coordinates.
projection driftGeneral or domain usageProjection drift is a mismatch between a generated view and the source it is meant to represent.
proofGeneral or domain usageA proof is a logically valid argument establishing a statement from definitions, assumptions, and previously justified results.
proof assistantGeneral or domain usageA proof assistant is software for constructing and checking arguments in a formal logical system.
proof boundarySystem-local specializationA proof boundary specifies exactly what a proof establishes and which surrounding claims need additional justification.
proof checkerGeneral or domain usageA proof checker verifies that a supplied formal proof obeys a logical system's rules and establishes the claimed statement.
propositionGeneral or domain usageA proposition is a statement that can be asserted or denied once its terms and parameters are specified.
protocolGeneral or domain usageA protocol is a defined set of messages, actions, ordering rules, and outcomes for interactions among participants.
provenanceGeneral or domain usageProvenance records where an item came from and the steps or sources that produced it.
providerGeneral or domain usageA provider is a component or organization that supplies a service, resource, or capability to a consumer.
pull requestGeneral or domain usageA pull request proposes merging a set of repository changes and provides a place to review them.
pytestExternally anchoredpytest is a framework for writing and running automated tests in Python.
queryableGeneral or domain usageInformation is queryable when a reader or program can retrieve relevant items by asking a structured question or searching.
queueGeneral or domain usageA queue is a collection of waiting items managed for later processing under stated ordering and delivery rules.
quickstartGeneral or domain usageA quickstart gives the shortest supported sequence of steps to obtain a first useful result.
quotient ringGeneral or domain usageFor an ideal I in a ring R, the quotient ring R/I treats two elements as equal when their difference lies in I.
radixGeneral or domain usageRadix is another word for the base of a positional numeral system.
ramification indexGeneral or domain usageIf a prime ideal p factors upstairs as pO_L=∏P_i^{e_i}, the exponent e_i is the ramification index of P_i over p.
ramification pointGeneral or domain usageA ramification point of a holomorphic map is a point where the map has local degree greater than one, equivalently where its derivative vanishes in a local coordinate.
rank of a matrixGeneral or domain usageThe dimension of the space spanned by a matrix's rows or columns.
rate limitGeneral or domain usageA rate limit restricts how many operations an actor or system may perform within a stated period.
rationalGeneral or domain usageA rational number is a number equal to a/b for integers a and nonzero b.
rational approximationGeneral or domain usageRational approximation studies how closely fractions can approach a number, especially in relation to their denominators.
rational independenceGeneral or domain usageNumbers are rationally independent when no nontrivial rational linear combination of them equals zero.
raw seedSystem-coined termRaw seed is Plectis's preserved, append-only record of the operator's original words and developing ideas.
readerGeneral or domain usageA reader is the person or software consuming a document or other published material.
reader packetSystem-coined termA reader packet gathers selected explanations, links, source references, and scope information for someone examining the project.
readinessGeneral or domain usageReadiness is the condition of meeting the stated requirements for a particular next action or operating stage.
real numberGeneral or domain usageA real number is a point on the real number line, including rational and irrational values.
receiptGeneral or domain usageA receipt is a saved record of an action and its reported outcome.
reciprocalGeneral or domain usageThe reciprocal of a nonzero number x is 1/x.
reciprocal seriesGeneral or domain usageA reciprocal series is a sum whose terms have the form 1/aₙ for specified nonzero numbers aₙ.
recurrenceGeneral or domain usageA recurrence defines terms of a sequence through a relation involving other terms, usually earlier ones.
reductionGeneral or domain usageA reduction shows how solving one problem would allow another problem to be solved.
Reeb graphGeneral or domain usageThe Reeb graph of a suitably regular function records how connected pieces of its level sets join and split, by collapsing each piece to a point.
referenceGeneral or domain usageA reference identifies another source, object, or location relevant to the current material.
reformulationGeneral or domain usageA reformulation expresses a question or statement in a different way, ideally making a useful aspect of its structure clearer.
registryGeneral or domain usageA registry is a structured collection of identified records about a particular kind of object.
regressionGeneral or domain usageRegression means either lost software behaviour after a change or a statistical method that models an outcome from predictor variables.
regression testGeneral or domain usageA regression test checks that previously expected software behaviour still works after a change.
regular expressionGeneral or domain usageA regular expression is a pattern written in a notation for matching text.
releaseGeneral or domain usageA software release is an identified version or artifact set that a publisher makes available for others to use.
reliabilityGeneral or domain usageReliability is the degree to which something performs its stated function consistently under specified conditions over time.
rename migration receiptSystem-coined termA rename migration receipt records the plan, outcome, and checks for moving or renaming stored material.
replayGeneral or domain usageA replay repeats a recorded scenario to examine whether it produces the expected behaviour.
repositoryGeneral or domain usageA repository stores a project's tracked files and, in Git, the history of their recorded revisions.
reproducibleGeneral or domain usageA result is reproducible when someone can use the stated materials and method to obtain the same relevant outcome.
research shiftSystem-local specializationA research shift is a bounded period of work on a specific, inspectable mathematical task.
residue classGeneral or domain usageA residue class modulo m consists of all integers congruent to one another modulo m.
residue fieldGeneral or domain usageA residue field records arithmetic at a prime ideal: set the ideal’s elements to zero, then make every remaining nonzero element invertible.
result recordSystem-local specializationA result record stores what a particular check or run examined and what it reported.
retryGeneral or domain usageA retry repeats an operation after failure, uncertainty, or the absence of a usable response.
reviewer briefSystem-coined termThe reviewer brief is a compact generated packet for someone assessing the public work.
riemann mapGeneral or domain usageA bijective holomorphic map between a simply connected proper planar domain and the unit disc.
rigidityGeneral or domain usageA rigidity result shows that stated conditions leave an object unusually little freedom, often determining it up to a specified equivalence.
ringGeneral or domain usageA ring is a set with an abelian-group addition and an associative multiplication that distributes over addition.
ring automorphismGeneral or domain usageA ring automorphism is a bijective map from a ring to itself that preserves addition, multiplication, and the multiplicative identity when rings are unital.
rollbackGeneral or domain usageA rollback returns a system, transaction, or recorded state to an earlier state after a change.
root multiplicityGeneral or domain usageThe multiplicity of a root measures how many copies of its linear factor occur in a polynomial.
root of a polynomialGeneral or domain usageA number r for which a polynomial f has value f(r)=0.
root of unityGeneral or domain usageAn nth root of unity is a complex number ζ satisfying ζⁿ=1; it is primitive when no smaller positive power of ζ equals one.
routingSystem-local specializationRouting chooses the next relevant destination or action from a question, input, or current state.
row jobSystem-coined termA row job specifies one bounded operation on an identified record or small artifact selection.
rowabilitySystem-coined termRowability is Plectis's term for whether a collection can be reliably browsed as identifiable, source-linked entries.
runnableGeneral or domain usageRunnable means the material can be executed with the stated code, dependencies, inputs, and instructions.
running least common multipleGeneral or domain usageA running least common multiple takes the least common multiple of all terms up to the current position in a positive-integer sequence.
runtimeGeneral or domain usageA runtime is the software support and execution context used while a program runs.
saddle connectionGeneral or domain usageA saddle connection is a trajectory connecting saddle-type singular points, possibly returning to the same one.
saddle pointGeneral or domain usageA critical point where a function rises in some directions and falls in others.
sandboxGeneral or domain usageA sandbox is an environment that enforces specific limits on the files, networks, devices, processes, or privileges available to running code.
scalarGeneral or domain usageA scalar is an element of the number system used for coefficients, scaling, and arithmetic in a mathematical structure.
schemaGeneral or domain usageA schema defines the expected structure and constraints of data.
scopeGeneral or domain usageScope states the cases, objects, actions, and conditions to which something applies.
semantic namingSystem-coined termSemantic naming gives an identifier or label enough meaning to help a reader recognise the object's role.
separable extensionGeneral or domain usageAn algebraic extension L/K is separable when every element of L has a minimal polynomial over K with no repeated roots in a splitting field.
separatrixGeneral or domain usageA separatrix is a distinguished trajectory, or invariant boundary, separating regions with different dynamical behaviour.
sequenceGeneral or domain usageA sequence is an indexed family of terms, usually ordered by natural-number positions.
seriesGeneral or domain usageA mathematical series is a sum of terms from a sequence, often extending over infinitely many indices.
series tailGeneral or domain usageThe tail of a series is the part remaining after a chosen finite number of terms.
serverGeneral or domain usageA server is a program or computer that receives requests and provides data, computation, or another service to clients.
setGeneral or domain usageA set is a collection determined by which elements belong to it.
set intersectionGeneral or domain usageThe intersection of sets contains exactly the elements common to all of them.
set membershipGeneral or domain usageSet membership is the relation saying that an object is one of the elements of a set.
set unionGeneral or domain usageThe union of sets contains every element belonging to at least one of them.
side effectGeneral or domain usageA side effect is an observable change a computation makes beyond returning its direct result.
simple critical pointGeneral or domain usageA simple critical point of a complex polynomial p is a simple root of its derivative: p′(c) = 0 and p″(c) ≠ 0.
simply connectedGeneral or domain usagePath connected with every closed loop continuously shrinkable to a point inside the space.
simulationGeneral or domain usageA simulation executes a model of a process to study the behaviour that follows from the model's rules and inputs.
skillSystem-local specializationIn this system, a skill is a reusable set of instructions for carrying out a recognisable kind of task.
sliceGeneral or domain usageA slice is a selected part of a larger collection or system.
smoke checkGeneral or domain usageA smoke check is a quick test for major failures in basic operation.
smooth functionGeneral or domain usageA smooth function has continuous derivatives of every finite order in its stated mathematical setting.
smooth numberGeneral or domain usageA positive integer is y-smooth if none of its prime factors exceeds y.
snapshotGeneral or domain usageA snapshot is a captured representation of data or system state associated with a particular point or version.
softwareGeneral or domain usageSoftware consists of programs and related data used by computers to perform tasks.
software libraryGeneral or domain usageA software library is a reusable collection of code, interfaces, or formal definitions intended for other programs or developments to use.
sourceSystem-local specializationA source is the original or controlling material from which a particular claim or artifact is drawn.
source bodySystem-local specializationA source body is the actual content of the code or document being referenced.
source fileGeneral or domain usageA source file contains material from which another artifact is built or defined.
source sliceSystem-coined termA source slice is the explicitly selected source material included in a task, package, or public release.
linear spanGeneral or domain usageIn linear algebra, the span of a set of vectors is the set of all finite linear combinations of them.
sparse checkoutGeneral or domain usageA sparse checkout limits which tracked files Git places in the working directory.
specificationGeneral or domain usageA specification states the requirements an implementation or result is expected to satisfy.
squarefreeGeneral or domain usageSquarefree means having no repeated prime factor for an integer, or no repeated irreducible factor for a nonzero polynomial.
stack traceGeneral or domain usageA stack trace is a recorded list of active function calls at or near the point where a program failed or was inspected.
standardSystem-local specializationA standard specifies requirements that items or processes are expected to meet.
statement nodeSystem-local specializationA statement node is one identified mathematical statement in a graph of results and their relationships.
static siteGeneral or domain usageA static site serves prebuilt files rather than generating each page in response to a reader’s request.
stationary bootstrapGeneral or domain usageThe stationary bootstrap resamples a time series in blocks of randomly chosen lengths to retain some of its temporal dependence.
stochasticGeneral or domain usageStochastic describes a process or model whose outcomes involve probability or randomness.
stubGeneral or domain usageA stub is a placeholder representing an item or interface whose full contents or behaviour are not yet supplied.
subcoverGeneral or domain usageA subcover is a selection from a collection of covering sets that still covers the same target set.
subexponential growthGeneral or domain usageGrowth slower than every fixed exponential c^n with c>1.
subharmonic functionGeneral or domain usageA subharmonic function never exceeds its average on a small surrounding circle and satisfies an upper-semicontinuity condition that rules out downward jumps at a point.
sublevel setGeneral or domain usageA sublevel set of a real-valued function g at c is {x : g(x) ≤ c}; a strict sublevel set uses g(x) < c.
subseriesGeneral or domain usageA subseries is formed by selecting terms from a series and keeping them in their original order.
subsetGeneral or domain usageA set A is a subset of B if every element of A also belongs to B.
subsumGeneral or domain usageA subsum is a sum obtained by retaining selected terms of a series and omitting the others.
sumGeneral or domain usageA sum is the result of adding quantities together.
summabilityGeneral or domain usageSummability means that a family of terms has a sum under a specified definition of infinite summation.
superior predictive abilityGeneral or domain usageHansen's superior predictive ability test assesses whether any candidate forecasting method has lower expected loss than a benchmark.
supportGeneral or domain usageSupport can mean evidence for a claim or, in mathematics, the positions where a function or sequence is nonzero.
supremumGeneral or domain usageThe smallest number greater than or equal to every member of a set.
Sylvester's sequenceGeneral or domain usageSylvester's sequence starts with 2, and each later term is one plus the product of all preceding terms.
synth seedSystem-coined termA synth seed is a concise, replaceable brief for the current phase of work.
syntheticGeneral or domain usageSynthetic data is deliberately generated rather than directly observed from the real situation being studied.
Taylor seriesGeneral or domain usageA Taylor series is the power series whose coefficients are determined by a function’s derivatives at a chosen point.
telemetryGeneral or domain usageTelemetry is automatically collected operational data sent or stored for observing a system away from the point where events occur.
telescoping identityGeneral or domain usageA telescoping sum is one in which cancellations reduce a long sum to a few endpoint terms.
terminalGeneral or domain usageA terminal provides a text interface for interacting with programs, commonly through a command-line shell.
testSystem-local specializationA test examines whether something behaves as expected under specified conditions.
theoremGeneral or domain usageA theorem is a mathematical statement established by proof within stated assumptions and definitions.
thresholdGeneral or domain usageA threshold is a boundary value at which a classification, condition, or behavior changes.
throughputGeneral or domain usageThroughput is the amount of work a system completes per unit of time.
timeoutGeneral or domain usageA timeout ends or changes waiting behavior when a defined time limit expires before the awaited event is observed.
TLSGeneral or domain usageTransport Layer Security, or TLS, is a protocol that encrypts and authenticates a network connection.
toolchainGeneral or domain usageA toolchain is the collection of tools used to turn source material into a built, runnable, or checked result.
total variation distanceGeneral or domain usageTotal variation distance is the supremum of the absolute difference between the probabilities two distributions assign to the same event.
totientGeneral or domain usageEuler's totient φ(n) counts the integers from 1 through n that are coprime to the positive integer n.
transactionGeneral or domain usageA transaction groups related operations behind a stated validation and commitment boundary, with guarantees that depend on the system.
transcendentalGeneral or domain usageA number is transcendental if it is not a root of any nonzero polynomial with integer coefficients.
transcriptGeneral or domain usageA transcript is a textual record of speech or an interaction.
triangle inequalityGeneral or domain usageThe distance directly between two points is at most the length of any route through a third.
trinomialGeneral or domain usageA trinomial is a polynomial written as the sum of three nonzero terms.
truth maintenanceSystem-coined termTruth maintenance tracks claims together with their reasons and dependencies so they can be reconsidered when evidence changes.
tryingGeneral or domain usageTrying means attempting an action whose outcome is not yet established.
Type ASystem-coined termType A names an actor with direct access to the working system and permission to perform specified operations on it.
Type A judgmentSystem-coined termType A judgement is the practical reasoning an agent uses when acting on the live system.
Type A metabolismSystem-coined termType A metabolism names the maintenance work that requires judgement about the system's structure or rules.
Type A operating registerSystem-coined termThe Type A operating register describes the conduct expected of an agent working directly on the system.
Type BSystem-coined termType B names an actor reasoning from supplied or externally available context without direct authority over the working system.
Type B metabolismSystem-coined termType B metabolism names the routine upkeep of structures whose rules, inputs, and expected outputs have already been defined.
typed refusalSystem-coined termA typed refusal is a structured result saying that an operation could not proceed, with a specific reason.
typed relationGeneral or domain usageA typed relation is a connection that states how two identified items are related.
unconditional resultGeneral or domain usageAn unconditional result needs no additional unresolved hypothesis beyond its stated mathematical setting.
uniform convergenceGeneral or domain usageFunctions converge uniformly when one sufficiently late stage makes the error small simultaneously at every point of the stated domain.
uninterpretableGeneral or domain usageHere, uninterpretable describes work for which readers do not yet have an adequate account of what it says or why it works.
unit discGeneral or domain usageThe open unit disc is the set of complex numbers z with |z| < 1.
univalent functionGeneral or domain usageA univalent function is a holomorphic function that is one-to-one on its domain.
universal quantifierGeneral or domain usageA universal quantifier states that a property holds for every element of a specified domain.
unramified primeGeneral or domain usageA prime is unramified in a number-field extension when its factorization upstairs contains no repeated prime-ideal power, equivalently every ramification index is one.
up-propagateSystem-coined termTo up-propagate is to place a reusable lesson in the shared source that should guide future relevant work.
upstreamGeneral or domain usageUpstream describes a source or earlier stage whose output, changes, or decisions flow into a specified consumer.
URLGeneral or domain usageA URL is a structured identifier for a resource, commonly giving a network address and a way to access it.
validationGeneral or domain usageValidation checks whether an object, result, or system meets stated requirements or is suitable for an intended use.
validatorGeneral or domain usageA validator checks whether supplied material satisfies a declared set of requirements.
variableGeneral or domain usageA variable is a symbol or name whose value is supplied, quantified, or allowed to vary within a stated setting.
vector spaceGeneral or domain usageA vector space allows vector addition and multiplication by scalars from a field, with operations obeying the linear-algebra axioms.
verificationGeneral or domain usageVerification checks whether a specified object satisfies a stated property, agrees with a reference, or conforms to a requirement.
vibe-mathingSystem-coined term“Vibe-mathing” is this project's informal name for accepting AI-generated mathematical reasoning on plausibility without adequate independent checking.
vulnerabilityGeneral or domain usageA vulnerability is a weakness that could be exploited to violate a security requirement.
web browserGeneral or domain usageA web browser is an application that retrieves, interprets, and presents web resources.
webhookGeneral or domain usageA webhook is an HTTP request one system sends to another when a configured event occurs.
WhisperExternally anchoredWhisper is OpenAI's speech-recognition model family for converting audio speech into text.
whole-system correctnessSystem-local specializationWhole-system correctness means satisfying a complete, stated specification for an entire system.
winding numberGeneral or domain usageThe winding number of a closed plane curve around a point outside the curve counts, with sign, how many net turns the curve makes around that point.
work landingSystem-coined termWork landing is the point at which an attempted change becomes a recorded, accepted part of the system.
working recordSystem-local specializationA working record is the detailed account of research on one problem, preserving results, attempts, evidence, and unresolved questions.
workingnessSystem-coined termWorkingness is Plectis's term for whether its evidence, beliefs, uncertainty, and permitted actions remain coherently connected.
Workingness InstrumentSystem-coined termA Workingness Instrument is a proposed structured record connecting one outcome to its evidence, dependencies, and permitted next actions.
The glossary explains reader-facing words. It does not rename source paths, package ids, old URLs, compatibility handles, or authority records by itself.