The Principia Machina/TPS/2.2 The Prime Kernel

Instruction artifact, machine-optimized text: TPS, section 2.2 The Prime Kernel. Part of TPS and the TPM hub. Human-only edit (TPS 5.13). TPS 0.1.0 was declared final at revision 4 on 2026-09-22, a version declaration recorded in the foundations record; the chain begins at TPX's first landing (TPS 5.6.7). TPS 0.1.1, which changed only the status lines, was declared final on 2026-09-26, TPS 0.3.0, revision 6, on 2026-09-28, and TPS 0.4.0, revision 7, on 2026-09-30. This page is revision 8 of the tree, declared final as TPS 0.5.0 by H-DECL on 2026-10-03 (naming TPS_0.5.0.txt by its file digest and its D(TPS)); revision 7 is carried whole, and revision 5, proposed as 0.2.0, stays undeclared. The text below is this section of the TPS artifact at 0.5.0, verbatim; the whole artifact and its file digest are on The Principia Machina/TPS. Human readers: the contents page is the map.

TPS 2.2  THE PRIME KERNEL
purpose: laws, assumptions, hard boundaries, CONSTRAINT entries; the
         TPK schema; the kernel tests T1-T6 and which parts are
         MECHANICAL; the declared form and its grammar; the D variable;
         the closed world; the structure check; initial and boundary
         values
governs: 2.2 | version: 0.5.0 (proposed) | class: instruction artifact
audience: operator, agent

2.2.1  The TPK is the first zone of the TFK: laws, assumptions, hard
       boundaries, CONSTRAINT entries. It is the guide's L0 KERNEL (see
       1.1). [I-020]
2.2.2  A restriction is declared as CONSTRAINT entries in the TPK, so the
       TPK yields the restricted DOF inventory (see 2.3.4). [B-02]
2.2.3  The kernel tests T1-T6 are the guide's tests of a TPK. TPX runs
       them as the TPK zone is entered and returns a rejected component
       to the author (see 5.5). [I-057]
       The bodies of T1-T6 are specified at guide 3.6: T1
       WELL-FORMEDNESS; T2 ATOMICITY OF ASSUMPTIONS; T3 CONSISTENCY TO
       DEPTH, bounded by a declared depth s_max; T4 DIMENSIONAL
       HOMOGENEITY; T5 DOF YIELD, which is where a CONSTRAINT entry is
       tested (2.2.2, 2.3.4); T6 BOUNDARY CLOSURE. Each names its
       inputs, class, pass condition and failure report; they run in
       order and T1 stops the run on failure. T2's semantic part, T3
       where the TPK is not executable, and T6 where a boundary
       predicate is not executable, are INSPECTION by the guide's own
       classing; every other part is MECHANICAL. [I-161] [D85.2]
       EXECUTABLE, in TPC, both residences, over the fields of 2.2.6:
       T1 whole, including the resolution of every REFS and TARGET,
       the UNIT checks of 2.2.9 and 2.2.10, and, where a declared form
       is present, its parse and the names rule (2.2.12); T2's
       syntactic part: an ASSUMPTION's PROPOSITION is refused when, at
       top level - outside closed bracket pairs and closed quotations,
       enclosing brackets stripped, an unclosed pair hiding nothing -
       it holds the words "and", "but" or "whereas", the phrase "as
       well as", the symbols "&" or U+2227, a semicolon, a second
       sentence or a list line, ASCII words matched whole in any case;
       T3 over the CONSTRAINT entries at depth 1 within every S_MAX >= 1
       (a TARGET both removed and fixed, or fixed at two values
       compared after normalization to coherent SI through the
       twelve-significant-digit canonical form; two FIX values of
       different KIND, or a value that cannot be normalized, returned
       to the author) and, where a LAW carries EQUATION, over the laws
       to the ground fragment (2.2.17); T4's constraint half inside T1
       (a FIX's UNIT against its TARGET's DIMENSION) and, where a LAW
       carries EQUATION, its law half (2.2.15); T5 (a) inside T1, and
       (b) every CONSTRAINT's TARGET named in the REFS of some LAW,
       (c) every DOF named in the REFS of some LAW, a DOF named only by
       an ASSUMPTION or a BOUNDARY being idle; T6's clause that a
       BOUNDARY's REFS lie within the DOF and CONSTANTs, inside T1,
       and, where a BOUNDARY carries CONDITION, its totality (2.2.16).
       T3 runs at the final pass, after the TMS is entered, since it
       reads STEP_CONVENTION and S_MAX from the TMS (5.5.2); a TMS
       without a depth of at least 1 is refused. Recorded limits: T2's
       rule refuses a one-claim proposition that uses a listed joiner
       and does not detect a comma splice or an unlisted connective,
       which reach the inspection the guide keeps; T3 over the fragment
       finds constraint-level contradictions only. [D106.1] [D107.1]
       [D108.1] [D132.1]
       INSPECTION, by H-DECL before the declaration: T2's semantic
       part; a law without EQUATION under T4 and T3; a boundary without
       CONDITION under T6; agreement between the prose and its declared
       form; T3 over the assumptions and beyond depth 1 (2.2.18).
       OWED: none of the bodies above; what stays INSPECTION is stated
       at 2.2.18 and is classed so by the guide or by the absence of a
       form, not by an owed body; C-01 stands for the parts a future
       declared form could carry. [DI-4.1] [D132.1]
       AMENDED (D176.1, D177.1). T1 also refuses a LAW without ROLE, a
       ROLE outside the grammar of 2.2.6 and an EOM(<NAME>) whose NAME
       is not a DOF of the TPK, and applies the D VARIABLE rules of
       2.2.13 under the TPK's D_VARIABLES; T4's law half reads D(x, s,
       n) by 2.2.15. After T3 and IC2's disposition the final pass
       runs the structure check (2.2.20), which refuses nothing.
       [D176.1] [D177.1]
2.2.4  While the body of a kernel test is owed, that check is INSPECTION,
       performed by H-DECL before the declaration that instantiates the
       container, and recorded as ratchet debt. TPX executes the check
       when its body lands. [DI-4.1]
2.2.5  Completeness certified by CAC is relative to the declared TPK's
       DOF inventory. CAC cannot detect a degree of freedom the TPK
       failed to yield (see 2.3.6, 7.1). [I-124]
2.2.6  THE TPK SCHEMA. A TPK is an object whose keys are an optional
       PARAMETERS part, ahead of its kinds, and its kinds, six kinds in
       this fixed order, a kind that is absent meaning empty:
         PART        FIELD                           WHEN ABSENT
         PARAMETERS  D_VARIABLES, ONE or SEVERAL     ONE
         KIND        REQUIRED FIELDS                 OPTIONAL FIELDS
         DOF         NAME DIMENSION                  ROLE
         CONSTANT    NAME DIMENSION                  VALUE UNIT
                                                     UNCERTAINTY
         LAW         NAME STATEMENT REFS ROLE        EQUATION
         ASSUMPTION  NAME PROPOSITION REFS           -
         CONSTRAINT  NAME TARGET ACTION STATEMENT    VALUE UNIT
         BOUNDARY    NAME PREDICATE REFS             CONDITION
       These are the guide's 3.1 contents under TPM names: DOF
       INVENTORY, CONSTANTS, LAWS, ASSUMPTIONS, CONSTRAINT entries,
       HARD BOUNDARIES. STATEMENT, PROPOSITION and PREDICATE are prose;
       what a check must read is a field. [D98.1] [D132.1]
       A BOUNDARY's PREDICATE, and its CONDITION where one is declared,
       states where the kernel IS asserted. Several BOUNDARY entries
       conjoin; a TPK with none is asserted everywhere. DIVERGENCE,
       recorded against the guide under its 2.5: guide 3.1 reads a hard
       boundary as where the kernel is not asserted; the specification
       governs the project and the guide's text is unchanged. [D179.1]
       PARAMETERS carries one field, D_VARIABLES: ONE, every D in the
       TPK's forms using one and the same D VARIABLE, or SEVERAL, any
       number of them (2.2.13). An absent PARAMETERS part or an absent
       D_VARIABLES means ONE and serializes exactly as an explicit
       ONE, so declaring the default and saying nothing give one
       digest (2.5.11). ROLE on a LAW is required and is one of these
       values, spelled exactly so, without spaces: EOM(<NAME>), the
       law is the equation of motion of the DOF named, which T1
       resolves to a DOF of this TPK; CONSTRAINT, an algebraic
       relation the DOF must satisfy, such as a pendulum's fixed
       length; CONSTITUTIVE, a relation giving a force or a material's
       response, such as a spring's force; INVARIANT, a quantity the
       motion conserves, such as an energy, which stays out of the
       structure check's matching; DEFINITION, a law defining one
       quantity from others, such as a momentum. ROLE on a DOF is
       optional and its one value is INPUT: a DOF the kernel takes as
       given, such as a forcing or a noise, for which no equation of
       motion is expected. The roles are the author's declaration: T1
       checks their spelling and EOM's NAME, and every other
       consistency of a ROLE is a finding of the structure check
       (2.2.20), never a refusal. ROLE CONSTRAINT names a law; it is
       not a CONSTRAINT entry, which removes or fixes one DOF (2.2.9).
       Example: a law "D(x, t) = v" is ROLE EOM(x); a law "m * D(v, t)
       = -k_s * x" is ROLE EOM(v). [D176.1] [D177.1]
2.2.7  NAME is an ASCII identifier, [A-Za-z_][A-Za-z0-9_]*, unique
       across the whole TPK, not only within its kind. A kernel written
       with Greek letters spells them; a Unicode name would let two
       look-alike names read as one citation and resolve as two.
       [D98.1]
2.2.8  REFS is a set of NAMEs: the DOF and CONSTANTs the entry names.
       Every REFS member resolves to a DOF or a CONSTANT of the same
       TPK. REFS and TARGET are declared by the author, not extracted
       from the prose; that REFS lists every name the prose uses is
       INSPECTION until a declared form (2.2.12) carries the names
       rule. [D98.1]
2.2.9  TARGET names the one DOF a CONSTRAINT removes or fixes. ACTION
       is REMOVE or FIX. FIX requires VALUE and UNIT; REMOVE forbids
       both. A FIX's UNIT is commensurable with the TARGET DOF's
       DIMENSION ("1", or an angle unit, for a dimensionless DOF),
       checked at zone entry; a mismatch refuses the component.
       [D98.1] [D104.1]
2.2.10 A CONSTANT with VALUE carries UNIT, and UNIT requires VALUE;
       UNCERTAINTY requires VALUE, is not negative and is in the same
       UNIT. UNIT parses under the unit grammar (3.2.11) and is
       commensurable with the CONSTANT's DIMENSION, checked at zone
       entry; a problem names the unit and both dimensions. UNIT is
       checked for its dimension, not its size: a value meant in m and
       written in km passes. [D104.1]
2.2.11 No entry carries a mutable field (STATE, SCRUTINY, RIDER, NOTE,
       CHECKS_OWED, RECORDS; 2.1.3). Such a field is refused, never
       dropped: content outside the digest is content the chain does
       not cover. Any other unknown field is refused likewise. [D98.1]
2.2.12 THE DECLARED FORM. Beside the prose, an OPTIONAL machine-readable
       form: EQUATION on a LAW, CONDITION on a BOUNDARY, and on a
       SIGNATURE of the TrM header FORM and IMAGE_FORM, both or neither
       (2.3.14). An absent form means no form; nothing is forced on an
       author, and a TPK without any form passes every mechanical check
       it passes without one. Where the form is present, T4's law half,
       T6's totality and the names rule - every identifier in the form
       a REFS member and every REFS member named in the form or the
       derivative variable - are MECHANICAL, and T3 over laws runs to
       the ground fragment; where it is absent those parts are
       INSPECTION by H-DECL at instantiation, listed by name at the
       gate and never silently passed. A form that does not parse, or
       fails the names rule, is T1's finding and the other checks skip
       that entry. [D108.1] [D132.1]
2.2.13 THE GRAMMAR of a declared form, closed:
         equation   := expr "=" expr                 EQUATION on a LAW
         form       := expr ( "=" expr )?            FORM, IMAGE_FORM
         predicate  := disj                          CONDITION
         disj       := conj ( "or" conj )*           left-associative
         conj       := neg ( "and" neg )*            left-associative
         neg        := "not" neg | "(" predicate ")" | expr cmp expr
         cmp        := "<" | "<=" | ">" | ">=" | "=" | "!="
         expr       := term ( ("+" | "-") term )*    left-associative
         term       := unary ( ("*" | "/") unary )*  left-associative
         unary      := "-" power | power             -a^2 is -(a^2)
         power      := atom ( "^" exponent )?        a^2^3 is refused
         exponent   := integer | "(" "-"? integer ")"
                     | "(" "-"? integer "/" integer ")"
         atom       := identifier | literal | "(" expr ")"
                     | function "(" expr ")"
                     | "D" "(" identifier "," identifier
                       ( "," integer )? ")"
         function   := exp | ln | sin | cos | tan | abs | sqrt
         identifier := [A-Za-z_][A-Za-z0-9_]*  a REFS, OVER or
                                               inventory NAME
         literal    := digits ("." digits)? ([eE] [-+]? digits{1,4})?
                       unsigned
         integer    := digit{1,4}                an exponent, a
                       rational exponent's parts, D's order; a leading
                       zero counts toward the four
       Tokens are identifiers, literals, the operators + - * / ^ = <
       <= > >= != ( ) and ",", and the keywords and, or, not;
       whitespace between tokens is ignored. No implicit
       multiplication, no unit inside an expression, no chained
       comparison, no two operators in a row (a*(-b) is written), no
       "^-1" (x^(-1) is written). D(x, s) and D(x, s, n), n >= 1, is
       the n-th derivative of x with respect to s, x any REFS member
       and s the D VARIABLE, a REFS member of any DIMENSION held to the
       rules of THE D VARIABLE below; D of a bound identifier
       evaluates to 0; D(x, s, 1) is spelled D(x, s); D is not
       permitted in a CONDITION. A function name without "(" is an
       identifier; a keyword is never an identifier. The parser is
       deterministic with one token of lookahead; its 33 grammar
       witnesses are asserted in both residences at load and pinned as
       vectors. [D132.1]
       BOUNDS. A form is at most 4,096 code points of its text after
       line-ending normalization and NFC (2.5.12), whitespace counted,
       and at most 64 parentheses deep: every "(" opens a level, a
       function's, D's and a parenthesized exponent's included, and a
       ")" with no level open closes none. An integer of the grammar is
       at most four digits as written, the bound of a DIMENSION
       exponent (2.5.12), so at most 9999; a literal is not an integer
       of the grammar, and its digits are bounded by the length alone.
       The length is checked first and the depth second, both before
       any token is read; the tokens and the grammar follow, an
       integer's digits checked where the grammar reads that integer
       and before its value is taken. A form past a bound is refused at
       the first bound it passes and read no further, as a form that
       does not parse: T1's finding for an EQUATION or a CONDITION
       (2.2.12), the TrM structural check's for a FORM or an IMAGE_FORM
       (2.3.14). The reasons read "the form is longer than 4096 code
       points", "more than 64 nested parentheses at N" and "an integer
       of more than 4 digits at N", N a 1-based code point position.
       Both residences refuse alike, and no integer past the bound is
       converted.
       The exponent a form composes is bounded alike: for every
       identifier and every D under nested powers and square roots, the
       product of the exponents enclosing it, taken from the innermost,
       a sqrt counting 1/2 and abs 1, while exp, ln, sin, cos and tan
       yield a pure number and end the product, has in lowest terms a
       numerator and a denominator of at most 9999 at every power and
       root. The parser checks it as it completes each power or root,
       after that power's own grammar; past it the form does not parse,
       with the reason "a computed exponent beyond 9999 at N", N the
       position of that ^ or of the root's name. [D186.1] [S14]
       THE D VARIABLE (D177.1). In the TPK's forms the second argument
       of D is a D VARIABLE: a DOF of the TPK that is the TARGET of no
       CONSTRAINT entry, whether FIX or REMOVE; T1 refuses any other.
       Under D_VARIABLES ONE (2.2.6) every D in every form of the TPK
       uses one and the same D VARIABLE, and a second, distinct one is
       T1's refusal; under SEVERAL any number may be used. The variable
       need not be the time and need not have DIMENSION T1: a scaled,
       dimensionless time is written like any other. A TPK whose forms
       use two or more D VARIABLES is a PDE kernel, which the structure
       check does not analyse (2.2.18, 2.2.20); one declared SEVERAL
       whose forms use one is analysed as under ONE. A D VARIABLE stays
       a DOF, with its TrM entry like any other. In a SIGNATURE's FORM
       and IMAGE_FORM (2.3.14) the names rule governs D's arguments and
       no D VARIABLE rule applies. The earlier rule, a variable of
       DIMENSION T1 exactly, is withdrawn. [D177.1]
2.2.14 CANONICAL SPELLING of a form, the spelling that enters the
       preimage (2.5.12): NFC; no whitespace, except one space around
       "and" and "or" and after "not"; literals in the canonical decimal
       form of 2.5.12; integer exponents without leading zeros; a
       rational exponent p/q kept as written; D(x,t,1) written D(x,t);
       the author's operand order and parenthesization kept, enclosing
       parentheses dropped only at delimiter-bounded slots (the whole;
       each side of "=" or of a comparison; a function argument), inner
       ones kept. Only spelling is canonical: "x*2" and "2*x" are
       different statements and digest apart. The canonical form parses
       back to the same tree. [D132.1]
2.2.15 DIMENSIONAL RULES. + and - need equal canonical DIMENSIONs and
       yield it; * adds exponents and / subtracts them; ^ multiplies by
       the integer exponent, or by p/q when every resulting exponent is
       an integer; exp, ln, sin, cos and tan need a dimensionless
       argument and yield 1; abs keeps its argument's; sqrt halves, every
       exponent even; a literal is dimensionless, and the literal zero
       has every dimension, so D(z, t, 2) = 0 and a guard x != 0 are
       homogeneous while dividing by an expression of the zero's
       dimension is refused; D(x, s, n) yields dim(x) less n times
       dim(s), base by base in exact integer arithmetic, so a derivative
       with respect to a dimensionless s keeps dim(x) and one with
       respect to a time lowers T by n; "=" and every comparison need
       equal DIMENSIONs. An unparsable DIMENSION or an absent identifier
       refuses the form's dimension. T4's law half: the two sides of
       EQUATION have one DIMENSION.
       Every exponent the rules read or compute - an identifier's
       DIMENSION as read, and each result of *, /, ^ and D - lies
       within -9999..9999, the bound of a DIMENSION exponent (2.5.12)
       that a UNIT's DIMENSION already keeps (3.2.11, tpm_units 0.2.3);
       past it the form's dimension is refused, "an exponent is out of
       range", a T4 or T6 finding. [D132.1] [S14] [D177.1]
2.2.16 TOTALITY of a CONDITION is decided syntactically over a closed
       guard table: / on E needs the conjunct E != 0 or 0 != E; ln(E)
       needs E > 0 or 0 < E; sqrt(E) and E^(p/q) need E >= 0 or 0 <=
       E; E^(negative) needs E != 0; tan is refused in a predicate; + -
       * abs exp sin cos and ^ with an integer >= 0 are total. A guard
       is a conjunct beside the comparison: the other operand of every
       "and" on the path from the root, through "not" and parentheses;
       an "or" on the path hides the conjuncts below it from those
       above; guards match by the canonical spelling of E; a > 0 does
       not guard /a. Every comparison of a CONDITION is dimensionally
       homogeneous. T6's totality: a partial operation without its
       guard refuses the BOUNDARY. [D132.1]
       OWED: two guard extensions and a listing, deferred to the
       sandboxes (D181.2): an expression built only from even integer
       powers, abs, sqrt, exp, positive literals, + and * counts as >= 0
       (exp as > 0); a CONSTANT with a nonzero VALUE guards division by
       itself, and one with a positive VALUE guards ln and sqrt of
       itself; every unguarded partial operation inside an EQUATION is
       listed for inspection; kind: computation, built and tested in the
       sandboxes, then a revision of this clause; C-01.
2.2.17 T3 OVER LAWS, THE GROUND FRAGMENT, at depth 1: a LAW whose every
       identifier is bound - every REFS member a CONSTANT with VALUE or
       a DOF under a FIX, the first FIX by NAME when two bind one DOF -
       is evaluated in coherent SI to a closed equation; an equation
       false through the twelve-significant-digit canonical form is P
       and not-P; two laws with one canonical left side and different
       right sides are P and not-P syntactically; a difference of KIND
       between the sides is returned; a derivative of a FIXed DOF is 0.
       Evaluation is in IEEE doubles in one written order, integer
       powers by repeated multiplication, a rational power by the one
       library call, overflow to infinity as C does, ln, sqrt and a
       negative base under a rational exponent refused outside their
       domains, division by zero refused, sin, cos and tan of a
       non-finite value refused; a non-finite result or a binding that
       cannot be normalized refuses the law with the reason.
       Every KIND exponent the evaluation reads or computes lies within
       -9999..9999, else the law is refused, "a kind exponent is out of
       range"; a zero base under a negative rational exponent is
       refused before the library call, as under a negative integer
       exponent, "0 under a negative exponent".
       The fragment finds a closed equation false and is not a
       consistency proof; beyond it T3 is INSPECTION by the guide's
       classing. [D132.1] [S14]
2.2.18 WHAT STAYS INSPECTION at the TPK gate: a law without EQUATION
       (T4 and T3 over it) and a boundary without CONDITION (T6),
       listed by name at the gate; agreement between the prose and its
       declared form (STATEMENT against EQUATION, PREDICATE against
       CONDITION); T2's semantic part; T3 over the assumptions and over
       the laws beyond depth 1, S_MAX staying a bound the fragment does
       not reach. The kernel tests are filters over declared fields:
       prose that disagrees with its fields escapes them. [D132.1]
       AMENDED (D176.1, D177.1). Also INSPECTION: in a PDE kernel,
       whose forms use two or more D VARIABLES, which DOF depends on
       which variable, and the structure of its equations, which the
       structure check does not analyse ("PDE: not analyzed"); a ROLE
       declared on a law without EQUATION, a claim the gate cannot
       verify, the PROSE line naming such a law where its REFS name an
       unknown DOF; the consistency of an INVARIANT law with the other
       laws; and each question the structure check puts to H-DECL
       under STRUCTURE_CHECK ON (2.2.20). Under STRUCTURE_CHECK OFF
       the structure check lists nothing for H-DECL. [D176.1] [D177.1]
2.2.19 THE CLOSED WORLD. A TFK asserts exactly what its entries state
       and nothing else. No force, field, medium, frame effect or
       constant is implied: gravity, electromagnetic fields, friction,
       drag and fictitious forces act only where a LAW names them, and a
       constant, pi included, exists only as a CONSTANT entry. An
       interaction the entries omit is not modelled; a CONSTRAINT entry
       is modelled and held, and declares no force, so a force that
       keeps it, a track's or a string's, is declared like any other
       (2.3.4). A register record may bring an interaction in only as
       its own ASSUMPTION record, cited in its ASSUMPTIONS and priced in
       a(r): it extends the world of that record and of the records that
       cite it, never the TFK's (3.2.7, 4.4). Where a LAW carries
       EQUATION the names rule makes this mechanical (2.2.12); a law in
       prose is held to it by H-DECL's inspection at the gate (2.2.18),
       and the structure check names a prose law that bears on an
       unknown DOF (2.2.20). No check reports what the entries leave
       out: completeness is relative to what the TPK declares (2.2.5).
       [S1]
2.2.20 THE STRUCTURE CHECK (D176.1, D177.1). At the final pass, after
       T3 and IC2's disposition, TPX runs the structure check over the
       TFK with TPC-PHP (eom_map, eom_findings, eom_class; 5.1.14). It
       asks whether the equations of motion determine the motion:
       every unknown DOF by exactly one law, nothing missing and
       nothing doubled.
       KNOWNS AND UNKNOWNS. Known: every CONSTANT; every DOF that a FIX
       or REMOVE CONSTRAINT targets, a FIXed DOF's derivatives being 0,
       propagated before matching; every DOF with ROLE INPUT; every D
       VARIABLE. Unknown: every other DOF. A law enters the matching
       when it carries EQUATION and its ROLE is EOM(<NAME>),
       CONSTRAINT, CONSTITUTIVE or DEFINITION; an INVARIANT law stays
       out and is listed as information; a law without EQUATION
       enters nothing.
       METHOD. A maximum bipartite matching of laws to unknowns; the
       Dulmage-Mendelsohn coarse parts, under-determined,
       over-determined and square; on the square part, Pryce's
       signature method with a Hungarian maximum transversal and
       offsets by the standard fixed point, giving the structural
       index and the number of initial values needed. Integer
       arithmetic throughout; every tie broken by NAME in code point
       order, so both residences agree byte for byte. The result is
       the EOM MAP. A TPK whose forms use two or more D VARIABLES is
       not analysed: "PDE: not analyzed" (2.2.13).
       FINDINGS, each named with its question for H-DECL:
         UNDER          an unknown determined by no form: a named gap
                        (3.3.5), opening EOM-0 under STRUCTURE_CHECK ON
                        (3.3.16);
         OVER-EOM       two or more laws of ROLE EOM(q) for one q, or
                        two laws each of the equation-of-motion shape,
                        a D of one DOF and order alone on one side up
                        to constant factors: "are they one equation?";
         OVER           any other structural redundancy, the
                        over-determined part: "is this law implied by
                        the others, or an independent claim?";
         CLOSED         a law that, after zero propagation, names no
                        unknown yet names a CONSTANT without VALUE:
                        "is the force that holds this DOF declared?";
                        a fully bound law is T3's ground fragment
                        (2.2.17), and one that reduces to 0 = 0 prints
                        nothing;
         ROLE MISMATCH  an EOM(q) law whose form holds no D(q, s, n)
                        with n >= 1, or whose q is a known: "is the
                        ROLE right?".
       LINES beside the findings: PROSE, a law without EQUATION whose
       ROLE enters the matching and whose REFS name an unknown ("v's
       equation of motion is stated only in prose"); NO FORM, no LAW
       carries EQUATION, one line asking the equation-of-motion
       question of each DOF; PDE, as above. An unknown with no EOM
       ROLE that a law of ROLE CONSTRAINT or CONSTITUTIVE determines, a
       multiplier or a constraint force, is not a finding.
       THE CLASS (eom_class, a pure function of the TFK), written on
       the STRUCTURE LINE (5.5.3). STRUCTURE_CHECK OFF: "Structure not
       Validated at Inception", reason CHECK OFF alone. STRUCTURE_CHECK
       ON: "structurally regular" only when declared forms are
       present, no finding is listed, neither PROSE nor PDE is printed
       and the square part is structurally nonsingular; otherwise
       "Structure not Validated at Inception" with every reason that
       applies, in this order: FINDINGS (any finding), PROSE, PDE, NO
       FORM. The two labels are the user's, byte for byte. The class is
       fixed at the declaration and never rewritten; the later test
       stands beside it (5.3.47). A UWC of either class is valid and
       does research; none is refused, retired or restricted by its
       class.
       DISPOSITIONS. STRUCTURE_CHECK ON: an UNDER finding is a named
       gap and opens EOM-0; OVER-EOM, OVER, CLOSED, ROLE MISMATCH and
       the PROSE, NO FORM and PDE lines are listed for H-DECL with
       their questions, each answered before the declaration or by
       declining it; nothing new is refused. STRUCTURE_CHECK OFF: the
       gate runs no structure check, opens no EOM-0 and lists nothing
       for H-DECL. Under either value the draft's check page shows the
       EOM MAP (5.5.12).
       The word is "structurally regular", never "well-posed": the
       check proves structural facts of the formed part only (7.1.54).
       [D176.1] [D177.1]
2.2.21 INITIAL AND BOUNDARY VALUES (D180.3). The TFK carries no initial
       value and no boundary value of a trajectory: its laws say how the
       DOF change, not where they start. A LAW that states a DOF's value
       at one instant (x = x0) is a modelling error; the structure check
       names it where the DOF also has an equation of motion (OVER or
       OVER-EOM) or where its ROLE is EOM(<NAME>) and it holds no
       derivative (ROLE MISMATCH), and otherwise it is H-DECL's
       inspection at the gate (2.2.18, 2.2.20). An initial or boundary
       value enters the register as its own ASSUMPTION record (3.2.15).
       [D180.3]