Terminology

PRINCIPIA MACHINA: terminology

Every version 1 term beside its version 2 word, its three-letter code, its Lean namespace, and the collision and rule behind the choice.

Terminology map as of 14 October 2026 · 33 rows · the three-letter codes are proposed, not yet approved · version 1, The Principia Machina, keeps its own words

On this page: What this registry is · The codes are proposed · The registry · The naming rules · How a new term gets a row · Read further

What this registry is

Version 2 of the Principia Machina restates the framework in Lean 4, a language in which proofs are checked by machine. Lean, its build tool Lake and its mathematics library Mathlib already use many of the words version 1 used every day. In Lean the kernel is the proof checker, an environment is everything defined so far, and a module is a source file; Mathlib has measures and manifolds. A version 2 text that used those words bare would mean two things at once.

This registry records how each version 1 term carries over. A row gives the version 1 term; the version 2 word that replaces it, or "unchanged"; its three-letter code, where it has one; the Lean namespace where it lives in the Lean sources; and the collision the new word avoids, or the rule that settles it. Every term of version 1's framework that has no row here is carried into version 2 unchanged.

The move is declared, term by term; it is not a search and replace. Version 1's records, digests and version numbers are not changed, and version 1's pages keep version 1's words. In version 2, words are the names, in prose and in the Lean sources alike. A three-letter code is an abbreviation for tables, digest labels and page titles, and is used nowhere a word fits.

The codes are proposed

The three-letter codes on this page are a proposal, not a decision. The Declarer approves the code table once, as a whole, and may change any code before he does. Until he has approved it, no code here is final and none should be cited as settled; that is why the code column is headed "Code (proposed)".

The codes were drawn up under rule R8 below: any two differ in at least two letters and none is a Lean core type, and a code that is also a known acronym elsewhere is flagged in its row. A note such as "not PRS (one letter from PFS)" records a candidate code that failed the rule.

The registry

One row per term, in the order of the terminology map this page is generated from. A blank cell means the map gives nothing there: the term has no code, or no Lean namespace of its own. "none" in the code column means the word deliberately has no code and is always written in full. Rules are cited by number (R1 to R9, below); a row that avoids a Mathlib word binds only under rule R7.

Version 1 term	Version 2 word	Code (proposed)	Lean namespace	Collision or rule
The Principia Machina, TPM	Principia Machina	PMA	Principia	the name is the Declarer's selection
TPS, The Principia Machina Specification	Principia Framework Specification	PFS	generated docs	also "perfect forward secrecy", flagged
TPK, The Prime Kernel	Starting Set	SST	Principia.StartingSet	"kernel" is Lean's checker; R2
TrM, The Translation Manifold	Correspondence Table	COR	Principia.Correspondence	Mathlib manifolds
TMS, The Measure Set	Criteria Set	CRI	Principia.Criteria	Mathlib Measure, MeasurableSet
TFK, The Full Kernel	Research Assembly	RAS	Principia.ResearchAssembly	"sealed" stays the adjective
ENVIRONMENT; ENVIRONMENT INVENTORY; ENVIRONMENT_QUANTITY	Physical Referent; REFERENT INVENTORY; REFERENT_QUANTITY	none	Principia.Referent	Lean.Environment; R5
ENVIRONMENT MODULE and its declarations	Provision, kinds Interaction and Convention	PRV	Principia.Provision	Lean and Lake modules; not INT (Int)
RR, Research Register	Research Record Register	RRG	Principia.Register
Congruence Protocol; CAC	Audit and Congruence Protocol; CAC	ACP; CAC	Principia.Congruence	Mathlib Con; compound
Public Recorder; PLATFORM	Recorder; Platform	REC	Principia.Recorder	not PRS (one letter from PFS)
TPX	Custos	CUS	PHP extension; Principia.Governor for its pure decisions	the name is the Declarer's selection
TPC, TPC-PHP, TPC-PY	Calculator, one residence; binary pcalc	PCC	Principia, Main	not calc, a Lean keyword
PRB	Research Client	RCL	Python	not RAC (one letter from RAS)
GTP	Agent Contract	AGC	spec part	not GAC (one letter from CAC)
CA-GTP	Certified Agent	CTA		not CRA (one from CRI), not CAG (one from CAC)
(no v1 term)	Agent Implementation Profile: the vendor-neutral generic prompt any agent may load, published with its digest	AIP		the term is the Declarer's selection
PACKAGE (probe)	Probe Pack	none	Principia.ProbePack	Lake.Package
MANIFEST page, tree, revision	Index page, Index tree, INDEX REVISION	none	Principia.Index	lake-manifest.json
LIBRARY PAGE	Reading page	none		lean_lib
kernel tests T1-T6	fundamental tests T1-T6		Principia.StartingSet.Tests
H-DECL, H-OP, H-OWN, H-SPON, ANY	Declarer, Operator, Initiator, Sponsor, Public		Principia.Role	groups pma-declarer, pma-operator, pma-initiator, pma-sponsor; Public is *
AI-LEAD, AI-CO	Holder, Coworker (lock states)		Principia.LockState	not "position" (Lean.Position)
USER, AGENT	unchanged		Principia.AccountClass	group pma-agent
D(TPK), D(TrM), D(TMS), D(TFK), D(TPS), D(IS)	D(SST), D(COR), D(CRI), D(RAS), D(PFS), D(IS)
content hash, page hash	digest; page digest			R4
UWC, DOF, DOMAIN, UNIT, REGIME, GRADE, STATUS, STRIKE, HOLD, RELEASE, falcon, canary, parrot, sponsor, fingerprint, governor, lane, seat	unchanged			checked, no collision
register record; CLASS, GRADE, STATUS, the envelope	unchanged		Principia.Record	the record table's types
envelope field TPS (the specification version a push conformed to)	PFS		EnvelopeField.pfsVersion	follows the TPS row; the code is proposed with the code table; v1 records keep TPS
record-table writers LEAD; TPX	HOLDER; CUSTOS		FieldWriter.holder, .custos	follow the AI-LEAD and TPX rows
type class (the record table's RID, IDSET, ... OBJECT)	value type		Principia.Record.ValueType	a type class is a Lean mechanism; R2
DERIVATION {STEPS, TEXT}	DERIVATION, forms PROSE, STRUCTURED, KERNEL		Principia.Record.Derivation, DerivationForm	wire word KERNEL kept; Lean name kernelProof (R2); PROSE may carry an unchecked attachment
(no v1 term)	DERIVATION_CLASS: INSPECTION, MECHANICAL, PROVED		Principia.Record.DerivationClass	the check classes, with PROSE credited INSPECTION, STRUCTURED MECHANICAL, KERNEL PROVED

The naming rules

Nine rules govern every version 2 name. The registry's last column cites them by number.

1. R1. Wire names and Lean names. A record field, state or code keeps its capital spelling on pages, in records and in prose (UNIT, AT, MATCH). In Lean the same thing is a lowerCamel word that is not a Lean keyword (unit, atPoint, outcome). One table maps each wire name to its Lean name; no name is escaped to get past a keyword.
2. R2. No bare colliding word. A word that clashes seriously with a meaning in Lean, Lake or Mathlib is never used alone. It is written as a two-word compound, in prose and in code, and Lean's own sense is always qualified: "the Lean kernel" when Lean's proof checker is meant.
3. R3. Every layer and zone is a namespace. Each layer and zone of the framework is a namespace under Principia, such as Principia.StartingSet. No single-word framework type sits at the root, and nothing shadows a Lean, Lake or Mathlib type.
4. R4. Digest, not hash. Every SHA-256 value is a digest. "Hash" is left to Lean's own 64-bit hash and to MediaWiki's SHA-1 of a page, which version 2 text calls the page digest.
5. R5. No type named like a Lean type. No framework type is named Name, Option, Unit, Level, Position, Format, Json, Declaration, Module, Environment, Kernel, Task, Job, Package, Workspace, Manifest, Target, Script, Cache, Env or Int.
6. R6. A registry. This page: every version 1 term with its version 2 word, code, Lean name, collision and rule. The move is declared, term by term, not done by search and replace, and version 1's records, digests and version numbers are not changed.
7. R7. Mathlib rows are conditional. A row that avoids a Mathlib word binds only if version 2 adopts Mathlib, Lean's mathematics library. Whether it does, or stays with core Lean, is still to be decided; the rows are recorded now so the choice is made with them in view.
8. R8. Codes. Any two codes differ in at least two letters, so a one-letter slip cannot turn one into another. No code is a Lean core type, and none is a well-known acronym in computing, cryptography or physics; where an overlap remains, the row says so.
9. R9. The size test. A name must read right for a spring on a track: nothing may sound too big for the smallest system the framework is used on.

How a new term gets a row

Every term of version 1's framework that is not listed here is carried into version 2 unchanged until a row says otherwise. Nothing is renamed silently.

When the work meets a term that needs a new word, most often because Lean, Lake or Mathlib already uses it, a row is added to the terminology map with all five columns:

1. the version 1 term, as version 1 wrote it;
2. the version 2 word, checked against Lean, Lake and Mathlib (R2, R3, R5) and against the size test (R9);
3. a code, only if the word needs one, checked under R8 against every code already in the table; a new code is proposed until the Declarer approves it;
4. the Lean namespace, under Principia (R3);
5. the collision the word avoids, or the rule applied.

This page is then generated again from the map and checked against it row by row, so the page and the map cannot differ. Like every framework page, it reaches this wiki only after the Declarer approves the change.

Read further

• The move to Lean: why version 2 is written in Lean, with the new words in context.
• The Principia Machina Specification: version 1's normative text, where the terms in the left-hand column are defined.
• The Principia Machina: version 1, its home page; it stays as history.

This page is generated from the terminology map in the Principia Machina source and replaced whole at each publish; an edit made here is overwritten. Terminology map as of 14 October 2026.