{
"ACCESS_POLICY": "OPEN",
"AUDIT_TRIGGER": "AUTOMATIC",
"BIBLIOGRAPHY_SETTING": "OFF",
"CLOSED_WORLD_QUESTION": "Is every interaction not written in the TPK absent from the system modelled?",
"CREATED": "2026-10-07T23:10:33Z",
"DECLARED": "2026-10-07T23:12:07Z",
"DECLARED_BY": "BFP Rauch",
"D_IS": "662a69d8a947ecb2c11caae2fc3f9de461d2e9b61e6a3fdaec02225b7935292e",
"D_TFK": "46db0af2a3f5fd6e86447bd1764cd5b934cf0f0be3c9f91d16fd47aa435afe5b",
"D_TMS": "7a962e2297d6798801fa2593be9cd92995cc3a5f9c817cc8a19335c625784128",
"D_TPK": "ad9d20d633d374edf7f7a2ddfefa6e886e67132a6e8a7cd42edd0237d3927088",
"D_TPS": "e45ef3a89f40c1335e2750dd7568e2be92b392717f90d23c917e0ee184688a0b",
"D_TRM": "f767f3635d0cbc54473b6f889c20a94d8d37f95d627d2c856516bac9c7d37de9",
"IC2_GAPS": [],
"INITIATOR": "DeltaS Zero",
"INSPECTIONS_OWED": [
"T2 the semantic part: each ASSUMPTION states one claim (guide 3.6)",
"T3 over the assumptions, and over the laws beyond the ground fragment at depth 1, to depth S_MAX (guide 3.6)",
"T4, T6 and T3 over every law or boundary without a declared form, as listed beside the kernel tests (D108.1)",
"IC4 (a) that each SIGNATURE image holds in the environment, beyond the syntactic reading, 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, PREDICATE and IMAGE names only what its REFS or OVER list, and agrees with its declared form where one exists"
],
"INTERVIEW": "NONE (no ENVIRONMENT MODULE is declared)",
"MODULES_USED": "NONE",
"PREFIX": "SPZ",
"STATE": "DECLARED",
"STRUCTURE_FINDINGS": [],
"STRUCTURE_LINE": "STRUCTURE structurally regular",
"TPC_PY": "0.3.0",
"TPC_PY_TREE": "63ef0f2decb5b2c15c19274026b2f9a95160d0f54fee3f58e273088901f564f1",
"TPS": "0.5.0",
"UNDER_GAPS": [],
"UUID": "c83c020c-6221-4ba4-8160-67a860c46d1a"
}
{
"TPK": {
"DOF": [
{
"NAME": "t",
"DIMENSION": "T1"
},
{
"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": "EOM_X",
"STATEMENT": "m dv/dt = -k_s x",
"REFS": [
"m",
"v",
"k_s",
"x",
"t"
],
"ROLE": "EOM(v)",
"EQUATION": "m * D(v, t) = -k_s * x"
},
{
"NAME": "KIN",
"STATEMENT": "dx/dt = v",
"REFS": [
"x",
"v",
"t"
],
"ROLE": "EOM(x)",
"EQUATION": "D(x, t) = v"
},
{
"NAME": "EOM_Z",
"STATEMENT": "m d2z/dt2 = 0",
"REFS": [
"m",
"z",
"t"
],
"ROLE": "CONSTRAINT",
"EQUATION": "m * D(z, t, 2) = 0"
}
],
"ASSUMPTION": [
{
"NAME": "A_kpos",
"PROPOSITION": "k_s is positive",
"REFS": [
"k_s"
]
},
{
"NAME": "A_mpos",
"PROPOSITION": "m is positive",
"REFS": [
"m"
]
}
],
"CONSTRAINT": [
{
"NAME": "C_NOZ",
"TARGET": "z",
"ACTION": "FIX",
"VALUE": "0",
"UNIT": "m",
"STATEMENT": "only motion on the spring axis is described: z = 0"
}
],
"BOUNDARY": [
{
"NAME": "B_small",
"PREDICATE": "|x| < x_max",
"REFS": [
"x",
"x_max"
],
"CONDITION": "abs(x) < x_max"
}
]
},
"TrM": {
"HEADER": {
"ENVIRONMENT_INVENTORY": [
{
"ENVIRONMENT_QUANTITY": "time",
"DIMENSION": "T1"
},
{
"ENVIRONMENT_QUANTITY": "position",
"DIMENSION": "L1"
},
{
"ENVIRONMENT_QUANTITY": "velocity",
"DIMENSION": "L1 T-1"
},
{
"ENVIRONMENT_QUANTITY": "transverse_position",
"DIMENSION": "L1"
}
],
"SIGNATURE": [
{
"NAME": "time_derivative",
"OVER": [
"x",
"v",
"t"
],
"IMAGE": "d/dt maps position to velocity",
"FORM": "D(x, t) = v",
"IMAGE_FORM": "D(position, time) = velocity"
}
],
"TRANSFORMATIONS": [
{
"NAME": "time_translation",
"STATEMENT": "t -> t + t0"
}
]
},
"ENTRIES": [
{
"NAME": "E_t",
"DOF": "t",
"DOMAIN": "always",
"ENVIRONMENT_QUANTITY": "time",
"IDENTIFICATION": "t is the reading of a laboratory clock from an arbitrary origin",
"FALSIFIER": "a second clock whose readings differ from t by more than a constant offset beyond the stated uncertainty",
"FALSIFIER_CLASS": "F3",
"BEARS": [],
"DIMENSION": "T1"
},
{
"NAME": "E_x",
"DOF": "x",
"DOMAIN": "|x| < x_max",
"ENVIRONMENT_QUANTITY": "position",
"IDENTIFICATION": "x is the displacement of the mass along the spring axis from the point where the spring exerts no force",
"FALSIFIER": "a measured spring force not proportional to x inside the domain",
"FALSIFIER_CLASS": "F3",
"BEARS": [
"EOM_X",
"KIN"
],
"DIMENSION": "L1"
},
{
"NAME": "E_v",
"DOF": "v",
"DOMAIN": "|x| < x_max",
"ENVIRONMENT_QUANTITY": "velocity",
"IDENTIFICATION": "v is the rate of change of x with t",
"FALSIFIER": "a measured velocity that differs from the rate of change of the measured x beyond uncertainty",
"FALSIFIER_CLASS": "F2",
"BEARS": [
"KIN"
],
"DIMENSION": "L1 T-1"
},
{
"NAME": "E_z",
"DOF": "z",
"DOMAIN": "always",
"ENVIRONMENT_QUANTITY": "transverse_position",
"IDENTIFICATION": "z is the displacement of the mass perpendicular to the spring axis",
"FALSIFIER": "a measured z different from 0 beyond its uncertainty",
"FALSIFIER_CLASS": "F3",
"BEARS": [
"EOM_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": []
}
]
}
}
