Tutorial 5: Check the draft
| The Principia Machina: map |
|---|
| Reading the diagrams Structure key Process key Definition of terms Roles |
| Reading by audience Start here: the walk through The operator's guide Tutorial: create a UUID Workspace Container (UWC) Public Recorder inputs Sponsors: your first agent |
| The specification Contents: parts, tables, diagrams TPS 0.5.0 (declared 2026-10-03, revision 8; machine-optimized text) Decisions (the foundations record, one line each) |
Tutorial: create a new UWC. One small example - a mass on a linear spring, moving only along x - is taken from a blank file to a declared UWC in eight steps. Each step says what runs today and what is specified but not yet built. It explains; the specification governs. Field-by-field reference: Public Recorder inputs.
Purpose
Run the full check, read every line of its output, and understand what the four digests are and are not.
Explains: TPS 0.1.0, revision 4 (declared final 2026-09-22); the zone schemas the declaring authority selected on 2026-09-22 (records D92.1, D98.1, D99.1, D100.1, and for units D103.1, D104.1, D105.1; schema 0.3.0), whose text enters TPS at revision 5, and the kernel tests and isomorphism checks selected the same day (D106.1, D107.1, D108.1; tpm_kernel_tests 0.2.0), whose text follows at the next TPS revision; TPC-PY as built 2026-09-22 (tpc_zone 0.3.0, tpc_units 0.1.0, tpc_tests 0.1.0; no TPC-PY version is declared yet) with check_draft 0.3.0. Where this page and the specification differ, the specification governs.
The finished draft
This is examples/spring_draft.json, exactly. You can copy it from here into a file.
{
"TPK": {
"DOF": [
{"NAME": "x", "DIMENSION": "L1"},
{"NAME": "v", "DIMENSION": "L1 T-1"},
{"NAME": "z", "DIMENSION": "L1"}
],
"CONSTANT": [
{"NAME": "m", "DIMENSION": "M1"},
{"NAME": "k_s", "DIMENSION": "M1 T-2"},
{
"NAME": "x_max",
"DIMENSION": "L1",
"VALUE": "0.05",
"UNIT": "m",
"UNCERTAINTY": "0.001"
}
],
"LAW": [
{
"NAME": "N2",
"STATEMENT": "m dv/dt = -k_s x",
"REFS": ["m", "v", "k_s", "x"]
},
{
"NAME": "KIN",
"STATEMENT": "dx/dt = v",
"REFS": ["x", "v"]
},
{
"NAME": "FREE_Z",
"STATEMENT": "d2z/dt2 = 0",
"REFS": ["z"]
}
],
"ASSUMPTION": [
{
"NAME": "A_lin",
"PROPOSITION": "the restoring force is linear in x (Hooke régime)",
"REFS": ["x"]
}
],
"CONSTRAINT": [
{
"NAME": "C_NOZ",
"TARGET": "z",
"ACTION": "FIX",
"VALUE": "0",
"UNIT": "m",
"STATEMENT": "motion confined to z = 0"
}
],
"BOUNDARY": [
{
"NAME": "B_small",
"PREDICATE": "|x| < x_max",
"REFS": ["x", "x_max"]
}
]
},
"TrM": {
"HEADER": {
"ENVIRONMENT_INVENTORY": [
{"ENVIRONMENT_QUANTITY": "position", "DIMENSION": "L1"},
{"ENVIRONMENT_QUANTITY": "velocity", "DIMENSION": "L1 T-1"},
{"ENVIRONMENT_QUANTITY": "height", "DIMENSION": "L1"}
],
"SIGNATURE": [
{
"NAME": "time_derivative",
"OVER": ["x", "v"],
"IMAGE": "d/dt maps position to velocity"
}
],
"TRANSFORMATIONS": [
{"NAME": "time_translation", "STATEMENT": "t -> t + t0"}
]
},
"ENTRIES": [
{
"NAME": "E_x",
"DOF": "x",
"DOMAIN": "|x| < x_max",
"ENVIRONMENT_QUANTITY": "position",
"IDENTIFICATION": "x is the displacement from equilibrium along the spring axis",
"FALSIFIER": "a measured restoring force not proportional to x inside the domain",
"FALSIFIER_CLASS": "F3",
"BEARS": ["N2", "KIN"],
"DIMENSION": "L1"
},
{
"NAME": "E_v",
"DOF": "v",
"DOMAIN": "|x| < x_max",
"ENVIRONMENT_QUANTITY": "velocity",
"IDENTIFICATION": "v is the time derivative of x",
"FALSIFIER": "a measured velocity differing from dx/dt beyond uncertainty",
"FALSIFIER_CLASS": "F2",
"BEARS": ["KIN"],
"DIMENSION": "L1 T-1"
},
{
"NAME": "E_z",
"DOF": "z",
"DOMAIN": "always",
"ENVIRONMENT_QUANTITY": "height",
"IDENTIFICATION": "z is the height above the track",
"FALSIFIER": "any measured z different from 0",
"FALSIFIER_CLASS": "F3",
"BEARS": ["FREE_Z", "C_NOZ"],
"DIMENSION": "L1"
}
]
},
"TMS": {
"PARAMETERS": {
"STEP_CONVENTION": "one application of an inference rule or algebraic identity is one step",
"K": "2",
"N_X": 2,
"S_MAX": 10
},
"CONSTANTS": [
{"NAME": "w_a", "VALUE": "1"},
{"NAME": "w_s", "VALUE": "0.5"}
],
"YARDSTICKS": [
{
"NAME": "combined_distance",
"KEY": ["SR1", "WSUM:w_a*A;w_s*S", "S"],
"LIMITING": []
}
]
}
}
Run it
python3 check_draft.py my_draft.json (Linux, macOS) py check_draft.py my_draft.json (Windows)
TPK PASS
T2 PASS
T5 PASS
TrM PASS
IC1-IC4 PASS
TMS PASS
YARDSTICK combined_distance: C1 pass, C2 pass, C4 pass
FINAL T3 and IC2 PASS
D(TPK) 9774fa1529e68d99ae555a6859f84f8d8ecbd60f72494d5614a99e11ba4cde54
D(TrM) f2d947467bebb3b1c226374d9d811b6492171454e373a72c3bfe8121a3a01b6d
D(TMS) 2b9c565165aeb13b808d9715012de71b3f46a8a6172ae4482b593ec68256ba75
D(TFK) 3e92bae72f437acac87d3f6a0683978cf629e61df17bed2ceb5e9da3c8c352b1
Inspections still owed to the declaring authority before declaring:
- T2 the semantic part: each ASSUMPTION states one claim (guide 3.6)
- T3 over the laws and assumptions to depth S_MAX; the constraints ran above (guide 3.6)
- T4 dimensional homogeneity of each law (guide 3.6; D108.1)
- T6 each boundary is total over its DOF (guide 3.6; D108.1)
- IC4 (a) the SIGNATURE is carried, and each borne law is expressible (guide 4.6)
- IC5 falsifier invariance under the TRANSFORMATIONS (guide 4.6)
- equivalence of environment quantities under the TRANSFORMATIONS (names are taken as written)
- every STATEMENT, PROPOSITION and PREDICATE names only what its REFS list
Advisory result (TPC-PY: tpc_zone 0.3.0, tpc_units 0.1.0, tpc_tests 0.1.0; schema 0.3.0). TPX decides at the gate.
Reading the output
TPK PASS,TrM PASS,TMS PASS- Each zone passed its structure checks: T1 for the kernel, and the schema checks for the manifold and the Measure Set, including the yardstick key rules.
T2 PASS,T5 PASS- The two kernel tests that run as the kernel is entered: no assumption is joined into two claims, and no DOF or constraint is idle.
IC1-IC4 PASS- The isomorphism checks, as the manifold is entered: every quantity and every DOF is identified exactly once, the dimensions match, and what each entry bears has entries. An untied DOF would be listed here and held for the final pass.
YARDSTICK combined_distance: C1 pass, C2 pass, C4 pass- The yardstick ran on the synthetic record suite and met SR9 C1, C2 and C4.
FINAL T3 and IC2 PASS- The final pass, which needs all three zones: no DOF is both removed and fixed, or fixed twice (T3 over the constraints), and no untied DOF is left for IC2_POLICY to settle.
- The four
D(...)lines - The digests of the three zones and of the whole TFK. See below.
- The list of inspections
- What no machine checks yet. The declaring authority performs these by eye before declaring (step 7).
- The last line
- A reminder that this result is advisory.
The exit status is 0: all three zones are present and every check passes.
What the digests are
Each is a SHA-256 fingerprint of one zone in a canonical form, and D(TFK) combines the three in a fixed order. The UWC will be bound to D(TFK): every write is checked against it, and a mismatch halts all writes until the declaring authority decides (TPS 2.5). Because the canonical form normalizes spelling, only a change of meaning moves a digest (Text and numbers).
What the digests are not
- Not something to type anywhere. TPX computes the digests again from the draft it stores; a digest copied by hand is not a digest.
- Not a certificate. TPX of record decides. These digests exist so that you and the declaring authority can compare them with TPX's candidate certificate at step 7: a difference means the draft TPX holds is not the file you checked.
If your copy of the example gives different digests, your file differs from the one above; compare them line by line.
Non-goals
A pass does not mean the kernel is right. It means the draft is well-formed under the checks that exist.
Worked example
The step is its own example.
Governing sections: TPS 2.5, 5.5 and 4.5.
Previous: 4 Write the Measure Set. Next: 6 Fix refusals.