BFP Rauch: 1 revision imported

2026-09-30T02:11:04Z

1 revision imported

← Older revision		Revision as of 02:11, 30 September 2026
(No difference)

BFP Rauch: TPC-PY source tpc_sr9.py (0.1.1), SHA-256 8856950baf55a6ea; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0)

2026-09-30T02:10:58Z

TPC-PY source tpc_sr9.py (0.1.1), SHA-256 8856950baf55a6ea; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0)

← Older revision		Revision as of 02:10, 30 September 2026
Line 45:		Line 45:
	import tpc_strike as S		import tpc_strike as S

	TPC_SR9_VERSION = "0.1.0"		TPC_SR9_VERSION = "0.1.1" # proposed PATCH with TPC-PY 0.2.0 (C-MS-5: TPC-PHP copies before it adds the fresh assumption)
	_FRESH = "~FRESH~" # prefix for the assumption added by the C2 transform		_FRESH = "~FRESH~" # prefix for the assumption added by the C2 transform

BFP Rauch: 1 revision imported

2026-09-28T04:37:36Z

1 revision imported

← Older revision	Revision as of 04:37, 28 September 2026
(No difference)

BFP Rauch: TPC-PY source tpc_sr9.py (0.1.0), SHA-256 5a3f02bd8e536455; conformed TPS 0.3.0; PROPOSED, not declared (CO-8)

2026-09-27T15:43:18Z

TPC-PY source tpc_sr9.py (0.1.0), SHA-256 5a3f02bd8e536455; conformed TPS 0.3.0; PROPOSED, not declared (CO-8)

New page

# -*- coding: utf-8 -*-
"""
TPC-PY --- SR9 C-test harness (TPC step 2, increment 3)
=======================================================
Discharges the SR9 part of TPS 4.5.3 OWED C-08: "the mechanical
implementation of ... SR9; the synthetic record suite for C1, C2, C4".
(SR3, SR4, SR8 were increment 1, tpc_strike.py.) Standard library only;
Python 3.7+; Windows/Linux.

WHAT IS CHECKED (TPS 4.5.2; check-class matrix row 17, MECHANICAL when
the entry is executable; on failure CAC refuses certification):
C1 the entry never ranks a record failing SR1 above one passing it;
C2 within a regime, adding an ASSUMPTION never improves rank, except
in a declared limiting case naming its DOMAIN, applied only there;
C4 the entry does not let an M contradiction strike an L derivation.
Plus the TPS 4.5.3 gate: the TMS declares k, STEP CONVENTION and N_x.
C3 and C5 are INSPECTION (row 18) and are not here.

EXECUTABLE ENTRY INTERFACE (what the harness runs):
key(rid, records, tfk) -> tuple; lexicographic; lower = closer
resolve(id1, id2, records, tfk) -> "STRIKE:<id>" | "AUDIT" |
"GAP:<id>" | "DOMAIN:<id>"
limiting -> list of DOMAIN strings where a C2
exemption is declared
A UWC declares an executable local yardstick in the closed grammar of
the TMS zone schema (D100.1); tpc_yardstick compiles it into this
interface, and every check below accepts that entry tuple in place of a
fixture name.

FIXTURES. ENTRIES holds one compliant entry (the strike skeleton itself)
and deliberately broken entries, each violating exactly one check, so the
corpus proves the harness catches what it must (a check that accepts what
it should reject is a soundness defect).

LIMIT. A pass on a finite synthetic suite is evidence, not proof: an entry
can still violate C1/C2/C4 on records the suite lacks. This is the design
TPS 4.5.2 specifies (MECHANICAL on a synthetic record suite); C3/C5 stay
INSPECTION.

SYNTHETIC RECORD FIELDS: regime ("L"|"M"), assumptions [ids], cites [ids],
steps (int), domain (str), sr1_fail (bool; given, since SR1 detection
needs a derivation oracle and is not a TPC function).
"""

import tpc_strike as S

TPC_SR9_VERSION = "0.1.0"
_FRESH = "~FRESH~" # prefix for the assumption added by the C2 transform

def _a(rid, records, tfk):
return S.a_of_r(rid, records, tfk)

def _sr1(r):
return 1 if r["sr1_fail"] else 0

# ---- key builders (total functions of record fields) ---------------------
def _key_skeleton(rid, records, tfk):
"""Skeleton (i)+(iii): SR1-failing records sort after all passing ones
(struck without ranking); then d(r) = (a(r), s(r))."""
r = records[rid]
return (_sr1(r), _a(rid, records, tfk), int(r["steps"]))

def _key_naive(rid, records, tfk):
"""Broken for C1: plain d(r), ignoring SR1 status."""
r = records[rid]
return (_a(rid, records, tfk), int(r["steps"]))

def _key_more_is_better(rid, records, tfk):
"""Broken for C2: more assumptions rank closer."""
r = records[rid]
return (_sr1(r), -_a(rid, records, tfk), int(r["steps"]))

def _key_invert_in(domain):
"""Inverts the assumption count inside one DOMAIN only (a limiting case)."""
def key(rid, records, tfk):
r = records[rid]
a = _a(rid, records, tfk)
return (_sr1(r), -a if r["domain"] == domain else a, int(r["steps"]))
return key

# ---- resolvers -----------------------------------------------------------
def _sr5(key, id1, id2, records, tfk):
k1, k2 = key(id1, records, tfk), key(id2, records, tfk)
if k1 < k2:
return "STRIKE:" + id2
if k2 < k1:
return "STRIKE:" + id1
return "AUDIT"

def _resolve_regime_aware(key):
"""SR7 for an L-M pair (never strike the L derivation: named GAP when
a(L) > 0, DOMAIN finding when a(L) = 0); SR5 on the key otherwise."""
def resolve(id1, id2, records, tfk):
r1, r2 = records[id1], records[id2]
if r1["regime"] != r2["regime"]:
lid = id1 if r1["regime"] == "L" else id2
return ("GAP:" if _a(lid, records, tfk) > 0 else "DOMAIN:") + lid
return _sr5(key, id1, id2, records, tfk)
return resolve

def _resolve_ignores_regime(key):
"""Broken for C4: SR5 on the key for every pair, L-M included."""
def resolve(id1, id2, records, tfk):
return _sr5(key, id1, id2, records, tfk)
return resolve

_K_LIM = _key_invert_in("LIM")
_K_OTHER = _key_invert_in("OTHER")

ENTRIES = {
# name: (key, resolve, declared limiting-case DOMAINs)
"skeleton": (_key_skeleton, _resolve_regime_aware(_key_skeleton), []),
"naive_d": (_key_naive, _resolve_regime_aware(_key_naive), []),
"more_is_better": (_key_more_is_better, _resolve_regime_aware(_key_more_is_better), []),
"ignores_regime": (_key_skeleton, _resolve_ignores_regime(_key_skeleton), []),
"limiting_declared": (_K_LIM, _resolve_regime_aware(_K_LIM), ["LIM"]),
"limiting_undeclared": (_K_LIM, _resolve_regime_aware(_K_LIM), []),
"limiting_leak": (_K_OTHER, _resolve_regime_aware(_K_OTHER), ["LIM"]),
}

def _entry(entry):
"""A fixture by name, or an entry tuple (key, resolve, limiting) built
elsewhere, such as a declared TMS yardstick (tpc_yardstick)."""
if isinstance(entry, tuple):
return entry
if entry not in ENTRIES:
raise KeyError("sr9: unknown entry %r" % entry)
return ENTRIES[entry]

def _suite(suite):
return suite["records"], list(suite.get("tfk_assumptions", []))

# ---- the checks ----------------------------------------------------------
def sr9_c1(entry, suite):
"""C1. Witnesses "F>P": SR1-failing F ranked strictly above passing P.
Returns [pass, sorted witnesses]."""
key, _, _ = _entry(entry)
recs, tfk = _suite(suite)
fails = sorted(i for i, r in recs.items() if r["sr1_fail"])
passes = sorted(i for i, r in recs.items() if not r["sr1_fail"])
w = []
for f in fails:
kf = key(f, recs, tfk)
for p in passes:
if kf < key(p, recs, tfk):
w.append(f + ">" + p)
w.sort()
return [not w, w]

def sr9_c2(entry, suite):
"""C2. For each record r, r+ = r with one fresh assumption (same regime).
A violation is key(r+) < key(r) outside a declared limiting DOMAIN; the
same inside one is recorded as exempt. Returns [pass, violations, exempt]."""
key, _, limiting = _entry(entry)
recs, tfk = _suite(suite)
viol, exempt = [], []
for rid in sorted(recs):
plus = dict(recs[rid])
plus["assumptions"] = list(plus.get("assumptions", [])) + [_FRESH + rid]
recs2 = dict(recs)
recs2[rid + "+"] = plus
if key(rid + "+", recs2, tfk) < key(rid, recs2, tfk):
(exempt if recs[rid]["domain"] in limiting else viol).append(rid)
viol.sort()
exempt.sort()
return [not viol, viol, exempt]

def sr9_c4(entry, suite):
"""C4. For each listed L-M contradiction, resolve in both orders; a
violation is any outcome striking the L record. Returns
[pass, sorted "L|M" witnesses]."""
_, resolve, _ = _entry(entry)
recs, tfk = _suite(suite)
viol = []
for a, b in suite.get("contradictions", []):
if recs[a]["regime"] == recs[b]["regime"]:
continue # C4 concerns M-vs-L only
lid, mid = (a, b) if recs[a]["regime"] == "L" else (b, a)
outcomes = {resolve(lid, mid, recs, tfk), resolve(mid, lid, recs, tfk)}
if ("STRIKE:" + lid) in outcomes:
viol.append(lid + "|" + mid)
viol.sort()
return [not viol, viol]

def sr9_harness(entry, suite):
"""Summary for the CAC gate: [C1 pass, C2 pass, C4 pass, total violations]."""
c1, c2, c4 = sr9_c1(entry, suite), sr9_c2(entry, suite), sr9_c4(entry, suite)
return [c1[0], c2[0], c4[0], len(c1[1]) + len(c2[1]) + len(c4[1])]

def tms_params_ok(params):
"""TPS 4.5.3: CAC refuses a TMS that does not declare k (SR3), STEP
CONVENTION (SR4) or N_x (SR6). k > 0; STEP CONVENTION a non-empty
string; N_x an integer >= 2. Returns [pass, missing-or-invalid names]."""
missing = []
k = params.get("k")
if isinstance(k, bool) or not isinstance(k, (int, float)) or not k > 0:
missing.append("k")
sc = params.get("step_convention")
if not isinstance(sc, str) or not sc.strip():
missing.append("step_convention")
nx = params.get("n_x")
if isinstance(nx, bool) or not isinstance(nx, int) or nx < 2:
missing.append("n_x")
return [not missing, missing]

The Principia Machina/TPC-PY/tpc sr9.py - Revision history

BFP Rauch: 1 revision imported

BFP Rauch: TPC-PY source tpc_sr9.py (0.1.1), SHA-256 8856950baf55a6ea; conformed TPS 0.4.0; PROPOSED, not declared (TPC-PY 0.2.0)

BFP Rauch: 1 revision imported

BFP Rauch: TPC-PY source tpc_sr9.py (0.1.0), SHA-256 5a3f02bd8e536455; conformed TPS 0.3.0; PROPOSED, not declared (CO-8)