"""RUN-043 - UESFCM: the unbounded-expansion, self-referential finite-closure methodology, and its own application. UESFCM v0.1 (dated 2026-09-19) is a research protocol, not a result: fix one canonical target Q*; let methods, representations and sources expand without a preset bound; link every artifact back to Q* (eleven LinkBack types); close each round into a finite, recoverable state C_t; recentre on Q* and the remaining obligations; stop only at proof or counterexample closure. It ships with a one-page operational protocol and a VALIDATION record. Nothing in it is computed, so this run reads it three ways: its vocabularies and stop rules against each other and against the protocol; its governance rules against the one application in its folder - seventeen Lebesgue cycles (2026-09-19 to 09-20), each a document and a state crystal - at the level of labels, chaining and ledger arithmetic (their mathematics is for the runs that follow); and its package record against the bytes. Checks A0 anchors the rules and lists below occur in the methodology and the protocol as written W1 vocabulary sec. 6.1's LinkBack types against the protocol's; the obligation, artifact and closure labels; the two closure states W2 stopping which states end the loop: the abstract, sec. 3, 21, 49, 50, 58 and 61, the protocol's sec. 7 and 10 W3 chain the cycles' headers and crystals: target, previous state, status; where the target and the first state are written down; the crystals' ledger arithmetic and continuity W4 labels the cycles' labels against the method: numerical evidence never marked proved or closed (sec. 45), the phrases sec. 40 bans, the method's labels used and unused, sec. 39's round format, reopening W5 relations the theories it relates itself to, which of them are in the archive; its lagged line against DLMVC P1 package the VALIDATION record against the documents' bytes and the archive R1 registry UESFCM's judgments reviewed, first-used statuses defined Usage: python code/run043_uesfcm.py [--drill] [--blind CID] """ import argparse import collections import copy import hashlib import json import re from decimal import ROUND_FLOOR, Decimal import gate import registry from corpus import SOURCES, TREE, source_bytes, walk_sources FOLDER = "main.zip!/UESFCM/" PKG = FOLDER + "UESFCM_v0.1_Package.zip!/" DOC = PKG + "UESFCM_Unbounded_Expansion_Self_Referential_Finite_Closure_Methodology_v0.1.md" PROTOCOL = PKG + "UESFCM_Operational_Protocol_v0.1.md" VALIDATION = PKG + "UESFCM_v0.1_VALIDATION.json" DLMVC_FOLDER = "main.zip!/DLMVC_Deep_Lag_Multi_Pass_Verification_Closure_Methodology/" DLMVC = DLMVC_FOLDER + "DLMVC_Deep_Lag_Multi_Pass_Verification_Closure_Methodology_v0.1.md" LOG = TREE / "data" / "gate-logs" / "run043-uesfcm.json" MANIFEST = TREE / "data" / "SOURCE_MANIFEST.v1.json" CYCLES = range(1, 18) TARGET = "UESFCM-LUC-TARGET-v0.1" FIRST_STATE = "UESFCM-LUC-C00-v0.1" CEILING = 0.834781191 # the theories sec. 33-37 and the references relate UESFCM to, by the word that names each REFERENCES = {"UBE": "無界展開論", "Paper 08": "有限符號與無界語義", "UBGUL": "UBGUL", "RCHM": "RCHM", "SREG / PEC": "SREG", "RCIG": "RCIG", "DLMVC": "DLMVC"} def cycle_package(i): return FOLDER + f"UESFCM_Lebesgue_Cycle_{i:02d}_Package_v0.1.zip!/" def is_cycle_doc(leaf_id): """the one Markdown document at the top of a cycle's package""" return any(leaf_id.startswith(cycle_package(i)) and "/" not in leaf_id[len(cycle_package(i)):] and leaf_id.endswith(".md") for i in CYCLES) def crystal_of(i): return cycle_package(i) + f"UESFCM_Lebesgue_State_Crystal_Cycle_{i:02d}_v0.1.json" def load_inputs(): blobs = {n: source_bytes(n) for n in SOURCES} got, names = {}, [] mentions = {"target": [], "first_state": []} refs = {k: {"mentions": [], "named": []} for k in REFERENCES} dlmvc_folder_mentions = [] for leaf, d in walk_sources(blobs, keep=lambda l: True): if d is None: continue names.append(leaf.id) if leaf.id in (DOC, PROTOCOL, VALIDATION, DLMVC) or is_cycle_doc(leaf.id) or leaf.id in {crystal_of(i) for i in CYCLES}: got[leaf.id] = d if TARGET.encode() in d: mentions["target"].append(leaf.id) if FIRST_STATE.encode() in d: mentions["first_state"].append(leaf.id) if not leaf.id.startswith(FOLDER): for k, term in REFERENCES.items(): if term.encode() in d: refs[k]["mentions"].append(leaf.id) if term in leaf.id: refs[k]["named"].append(leaf.id) if leaf.id.startswith(DLMVC_FOLDER) and b"UESFCM" in d: dlmvc_folder_mentions.append(leaf.id) cycles = {} for i in CYCLES: doc = [k for k in got if is_cycle_doc(k) and k.startswith(cycle_package(i))] assert len(doc) == 1, doc cycles[i] = {"name": doc[0][len(FOLDER):], "doc": got[doc[0]].decode("utf-8"), "crystal": json.loads(got[crystal_of(i)])} manifest = json.loads(MANIFEST.read_text(encoding="utf-8")) rows = {row[0]: row for row in manifest["leaves"]} return {"text": got[DOC].decode("utf-8"), "protocol": got[PROTOCOL].decode("utf-8"), "doc_bytes": got[DOC], "protocol_bytes": got[PROTOCOL], "validation": json.loads(got[VALIDATION]), "dlmvc": got[DLMVC].decode("utf-8"), "cycles": cycles, "cycle_leaves": sorted([FOLDER + c["name"] for c in cycles.values()] + [crystal_of(i) for i in CYCLES]), "mentions": mentions, "folder": sorted(n[len(FOLDER):] for n in names if n.startswith(FOLDER)), "refs": refs, "dlmvc_folder_mentions": dlmvc_folder_mentions, "manifest_rows": {k: rows[k] for k in (DOC, PROTOCOL)}} # ---------------------------------------------------------------- reading the texts def norm(text): return text.replace("\r\n", "\n") def sec(text, n): """top-level section n: from its heading to the next top-level heading""" text = norm(text) m = re.search(rf"^# {n}\. .*$", text, re.M) if not m: return "" rest = text[m.end():] k = re.search(r"^# ", rest, re.M) return rest[:k.start()] if k else rest def components(s): m = re.search(r"C_t\s*=\s*\((.*?)\)", norm(s), re.S) return [x.strip() for x in m.group(1).split(",")] if m else [] def vocabulary(text, protocol): items = r"^- `([A-Z][A-Z-]*)`$" return {"links": re.findall(r"^### `([A-Z][A-Z-]*)`$", sec(text, 6), re.M), "links_protocol": re.findall(items, sec(protocol, 4), re.M), "obligations": re.findall(items, sec(text, 14), re.M), "artifacts": re.findall(items, sec(text, 40), re.M), "closures_21": re.findall(r"^`([A-Z][A-Z-]*)`", sec(text, 21), re.M), "closures_30": re.findall(r"^`([A-Z][A-Z-]*)`$", sec(text, 30), re.M) + re.findall(r"\\text\{([A-Z-]+)\}", sec(text, 30)), "stalled": re.findall(r"\\text\{([A-Z-]+)\}", sec(text, 49)), "frozen": re.findall(r"^`([A-Z][A-Z-]*)`$", sec(protocol, 1), re.M), "avoid": re.findall(r"^- ([a-z][a-z ]+)；$", sec(text, 40), re.M)} def method_labels(text): """every label the methodology itself defines or lists""" v = vocabulary(text, "") return sorted(set(v["links"] + v["obligations"] + v["artifacts"] + v["closures_21"] + v["closures_30"] + v["stalled"])) EXITS = {"ProofClosed": "proof", "CounterexampleClosed": "counterexample", "IndependenceClosed": "independence", "PROOF": "proof", "REFUTED": "counterexample", "Proof": "proof", "Counterexample": "counterexample", "Independence": "independence", "InvalidTarget": "target-failure", "NoProgress": "search-stalled", "ProofClosure": "proof", "CounterexampleClosure": "counterexample", "TargetFailure": "target-failure", "proof": "proof", "refutation": "counterexample", "independence": "independence", "有限完整符號證明": "proof", "反例": "counterexample", "明確的作用域相對獨立性閉包": "independence"} def operators(s): return re.findall(r"\\operatorname\{(\w+)\}(?:_T)?\(Q\^\\star\)=1", gate.squash(s)) def stopping(text, protocol): text, protocol = norm(text), norm(protocol) abstract = text[text.index("# 摘要"):text.index("\n# 1. ")] code = re.search(r"```text\n(.*?)```", sec(text, 50), re.S) code = code.group(1) if code else "" s61 = gate.squash(sec(text, 61)) m61 = re.search(r"直到取得(.+?)、(.+?)或(.+?)。", s61) runtime = re.search(r"Stop only at (\S+) closure", sec(protocol, 10)) places = {"abstract": operators(abstract), "sec. 3": operators(sec(text, 3)), "sec. 21": [h.replace(" ", "") for h in re.findall(r"^## 21\.\d (.+)$", sec(text, 21), re.M)], "sec. 50": re.findall(r"return (\w+)", code), "sec. 58": operators(sec(text, 58)), "sec. 61": list(m61.groups()) if m61 else [], "protocol sec. 7": [h.replace(" ", "") for h in re.findall(r"^### (.+)$", sec(protocol, 7), re.M)], "protocol sec. 10": runtime.group(1).split("/") if runtime else []} exits = {k: sorted({EXITS.get(x, "?" + x) for x in v}) for k, v in places.items()} s49, s7 = sec(text, 49), sec(protocol, 7) return {"exits": exits, "distinct": len({tuple(v) for k, v in exits.items() if k != "sec. 58"}), "sec. 21 says three": "UESFCM 定義三種主要終止狀態" in sec(text, 21), "sec. 49 stalls into more expansion": "SEARCH-STALLED" in s49 and "然後觸發" in s49, "protocol stops at SEARCH-STALLED": bool(re.search(r"### No Progress\s+`SEARCH-STALLED`", s7)), "pseudocode": {"loop": "while True:" in code, "breaks": code.count("break"), "handles": {k: bool(re.search(p, code)) for k, p in {"target failure": r"(?i)target.?fail", "search stalled": r"(?i)stall", "independence": r"(?i)independ"}.items()}}} # ---------------------------------------------------------------- the cycles HEADER = {"code": r"文件代號：\*\*\s*(\S+)", "date": r"日期：\*\*\s*(\S+)", "target": r"Target：\*\*\s*`([^`]+)`", "previous": r"Previous state：\*\*\s*`([^`]+)`", "status": r"Cycle status：\*\*\s*`([^`]+)`"} def header(doc): head = norm(doc).split("\n---\n")[0] return {k: (m.group(1) if (m := re.search(p, head)) else None) for k, p in HEADER.items()} def leaves(obj, path=()): if isinstance(obj, dict): for k, v in obj.items(): yield from leaves(v, path + (k,)) elif isinstance(obj, list): for i, v in enumerate(obj): yield from leaves(v, path + (i,)) else: yield path, obj def dec(x): return Decimal(repr(x)) if isinstance(x, float) else Decimal(x) def identities(cr): """the crystals' ledger: every number one crystal derives from others, and every count one cycle hands the next""" c, r = cr, {} close = lambda a, b, tol=1e-15: abs(a - b) <= tol s = c[1]["representative_search"] r["C01 master gap = 0.8440935944 - 0.8344"] = dec(c[1]["master_gap_public"]) == Decimal("0.8440935944") - Decimal("0.8344") r["C01 structural lower = grid minimum - orientation loss"] = close(s["B7_grid_min"] - s["B7_orientation_loss_conservative"], s["B7_structural_lower_before_fp_error"]) r["C02, C03, C09 family ceiling 0.834781191"] = c[2]["family_ceiling"] == c[3]["family_ceiling"] == c[9]["taylor_diagnostic"]["family_ceiling"] == CEILING a, b = c[3]["sharp_root_domain"], c[4]["sharp_root"] r["C03 sharp root domain = C04's"] = [a["d_star"], a["tmax_B3"], a["tmax_B5"], a["translation_square_4volume_shrink_vs_0.70"]] == \ [b["d_star"], b["T3"], b["T5"], b["translation_4volume_shrink_vs_0.70_square"]] ga, gb = c[4]["gate_A"], c[4]["gate_B"] r["C04 certified lower = sample lower - orientation loss"] = close(ga["sample_lower"] - ga["orientation_loss"], ga["certified_global_lower"]) r["C04 search margin = candidate - ceiling"] = close(gb["search_candidate"] - CEILING, gb["search_margin_above_ceiling"]) r["C04 gate B states the certified lower"] = repr(ga["certified_global_lower"]) in gb["statement"] g5 = c[5]["gate_A"] r["C05 safe lower = C04's certified lower, rounded down to 7 places"] = dec(g5["safe_lower"]) == dec(ga["certified_global_lower"]).quantize(Decimal("1e-7"), rounding=ROUND_FLOOR) r["C05 gate B states the safe lower"] = repr(g5["safe_lower"]) in c[5]["gate_B"]["statement"] dr = c[5]["domain_reduction"] r["C05 combined factor = translation x angle"] = close(dr["translation_volume_factor"] * dr["angle_factor"], dr["combined_naive_coordinate_volume_factor"], 1e-12) r["C05 translation factor = C03's to 1e-13"] = abs(dr["translation_volume_factor"] / a["translation_square_4volume_shrink_vs_0.70"] - 1) < 1e-13 an = c[6]["symmetric_anchor"] r["C06 safe margin = C05's safe lower - the anchor's move"] = dec(an["gateA_margin_safe"]) == dec(g5["safe_lower"]) - dec(an["hausdorff_from_published_U0_upper"]) r["C06 far branches at the safe margin"] = all(repr(an["gateA_margin_safe"]) in f for f in (c[6]["far_decomposition"]["F3"], c[6]["far_decomposition"]["F5"])) se = c[6]["search_evidence"] r["C06 branch gaps = minima - ceiling"] = close(se["F3_min_candidate"] - CEILING, se["F3_gap_above_ceiling"]) and close(se["F5_min_candidate"] - CEILING, se["F5_gap_above_ceiling"]) p = c[7]["runtime_probe"] rounds, fr = p["rounds"], p["current_frontier"] r["C07 requeued roots feed the next round and the frontier"] = all(rounds[k]["requeued_roots"] == rounds[k + 1]["tasks"] for k in range(len(rounds) - 1)) \ and rounds[-1]["requeued_roots"] == fr["roots"] r["C07 frontier fractions sum to 1"] = close(fr["fully_F3_fraction"] + fr["straddles_F3_boundary_fraction"] + fr["already_not_F3_fraction"], 1.0, 1e-12) r["C07 frontier gap = minimum - ceiling"] = close(fr["exact_center_area_min"] - CEILING, fr["exact_center_area_gap_above_family_ceiling"]) t = c[8]["topology_compression"] r["C08 frontier = C07's"] = c[8]["frontier_roots"] == fr["roots"] r["C08 reduction = signatures / skeletons"] = t["observed_full_piece_center_signatures"] / t["observed_body_level_center_skeletons"] == t["signature_count_reduction_factor"] q, td = c[9]["reflection_quotient"], c[9]["taylor_diagnostic"] r["C09 skeletons = C08's, halved by reflection"] = q["oriented_skeletons"] == t["observed_body_level_center_skeletons"] == 2 * q["unoriented_reflection_classes"] r["C09 dominant fraction = roots / C08's frontier = C08's top-2 coverage"] = close(q["dominant_fraction"], q["dominant_roots"] / c[8]["frontier_roots"]) \ and q["dominant_fraction"] == t["top2_coverage"] r["C09 dominant roots = its diagnostic's"] = q["dominant_roots"] == td["dominant_reflection_class_roots"] r["C09 centre-area minimum = C07's"] = td["center_area_min"] == fr["exact_center_area_min"] r["C09 first-order split = roots within 1e-3"] = td["first_order_positive"] + td["first_order_nonpositive"] == td["roots_with_center_area_within_1e-3_of_ceiling"] \ and len(td["first_order_exception_frontier_indices"]) == td["first_order_nonpositive"] r["C09 second order positive on all roots within 5e-4"] = td["second_order_positive"] == td["roots_with_center_area_within_5e-4_of_ceiling"] pt = c[10]["priority_tier"] r["C10 tier = C09's roots within 5e-4, all closed"] = pt["roots"] == pt["closed"] == td["roots_with_center_area_within_5e-4_of_ceiling"] r["C10 verified slack = raw slack - safe eta"] = close(pt["min_raw_slack"] - pt["eta_safe"], pt["min_verified_slack"], 1e-22) and pt["eta_model"] <= pt["eta_safe"] fb = c[11]["formal_batch"] r["C11 input = C09's roots within 1e-3 - C10's closed"] = fb["input_roots"] == td["roots_with_center_area_within_1e-3_of_ceiling"] - pt["closed"] r["C11 input = verified + packaging debt + persistent families"] = fb["input_roots"] == fb["verified_closed_roots"] + len(c[11]["packaging_debt"]) \ + len(c[11]["persistent_research_families"]) fp = c[12]["formal_progress"] r["C12 input = C11's root-6217 subroots"] = fp["input_subroots"] == c[11]["persistent_research_families"]["6217_subroots"] r["C12 closed + remaining = input"] = fp["closed_subroots"] + fp["remaining_subroots"] == fp["input_subroots"] sc = c[12]["structural_reduction"]["symmetric_contact"] r["C12 candidate gap = area - ceiling"] = close(sc["candidate_area"] - CEILING, sc["candidate_gap_above_ceiling"]) r["C12 contact x3 = C06's anchor x3 - safe margin"] = dec(sc["x3_star"]) == dec(an["x3"]) - dec(an["gateA_margin_safe"]) ro = c[14]["root_6217"] r["C13 gate A closed, carried by C14 and C15"] = c[13]["root_6217"]["gate_A_rho0"]["status"] == ro["gate_A_rho0"] == c[15]["root_6217"]["gate_A_rho0"] == "CLOSED" r["C14 before = C12's remaining; remaining = before - closed"] = ro["formal_boxes_before"] == fp["remaining_subroots"] \ and ro["formal_boxes_remaining"] == ro["formal_boxes_before"] - ro["formally_closed_this_cycle"] r["C16 remaining = C14's"] = c[16]["root_6217"]["formal_remaining_cells"] == ro["formal_boxes_remaining"] r["C16 tight reference below C15's"] = c[16]["root_6217"]["tight_A_ref"]["value"] < c[15]["root_6217"]["boundary_locking"]["A_ref"] r17 = c[17]["root_6217"] r["C17 before = C16's; remaining = before - closed"] = r17["formal_cells_before"] == c[16]["root_6217"]["formal_remaining_cells"] \ and r17["formal_cells_remaining"] == r17["formal_cells_before"] - len(r17["formal_Aref_closed"]) - len(r17["formal_target_closed"]) cc = r17["competitive_core_diagnostic"] r["C17 unresolved = low cells - closed"] = sorted(set(cc["cells_at_or_below_0_835_before_cycle17_closure"]) - set(r17["formal_target_closed"])) \ == sorted(cc["unresolved_after_cycle17"]) return r EVIDENCE = re.compile(r"(? len(cycles) / 2 else {"cycles": len(v), "only": v} for k, v in fmt.items()} reopen = {i: [line.strip() for line in t.split("\n") if re.search(r"(?i)reopen", line)] for i, t in docs.items()} reopen = {i: v for i, v in reopen.items() if v} return {"discipline": {"crystal_strings": strings, "verdict_lines": lines, "violations": violations, "closure_joined_to_evidence": joined}, "banned": {x: len(re.findall(re.escape(x), everything, re.I)) for x in avoid}, "method_used": {k: v for k, v in sorted(used.items()) if v}, "method_unused": sorted(k for k, v in used.items() if not v), "own_labels": len(own), "own_top": [[k, v] for k, v in own.most_common(6)], "cycle_status": sorted({header(t)["status"] for t in docs.values()}), "link_types_used": {i: v for i, v in link_use.items() if v}, "cycle01_linkback_map": c01_map, "format": {k: (len(v) if len(v) > 8 else v) for k, v in fmt.items()}, "reopening": {"REOPENED": label_count("REOPENED", everything), "mentions": reopen, "all_prohibitive": all(re.search(r"(?i)not", m) for v in reopen.values() for m in v), "rejections": sorted(i for i in cycles if re.search(r"REJECTED", docs[i] + crystals[i]))}} # ---------------------------------------------------------------- checks ANCHORS = { "text": { "W1": [r"\boxed{\Lambda_{Q^\star}(x)}", "只有：$$\\Lambda_{Q^\\star}(x)\\neqNULL$$的產物才能進：", "`NULL`產物可以保存到：", r"C_t=(G_t,O_t,B_t,R_t,D_t,V_t,P_t,K_t).", "避免：-probablysolved；-lookscorrect；-essentiallyproved；被當成正式狀態。"], "W2": [r"它只以：$$\boxed{\operatorname{ProofClosed}(Q^\star)=1}$$或：$$\boxed{\operatorname{CounterexampleClosed}(Q^\star)=1}$$為該數學問題的終止條件。", "UESFCM定義三種主要終止狀態。", "ifProofClosed(Q*,Ct):returnPROOF,CanonicalProofArtifact", "ifCounterexampleClosed(Q*,Ct):returnREFUTED,CounterexampleArtifact", r"\boxed{\text{SEARCH-STALLED}.}", "然後觸發：-representationexpansion；-methodexpansion；-externalliteratureexpansion；-independentAI；-DLMVCaudit。", r"\boxed{\operatorname{IndependenceClosed}_T(Q^\star)=1.}", "直到取得有限完整符號證明、反例或明確的作用域相對獨立性閉包。"], "W3": [r"\boxed{\text{Expansionmaybeunbounded;targetreferencemaynotdriftsilently.}}", "$$Q^\\star$$不得silentdrift。", "12.targethashing/versioning。", r"\boxed{\text{proofkernel}+\text{counterexamplebasis}+\text{debtledger}+\text{provenance}.}", "$$C_t$$必須有限。"], "W4": [r"\text{NUMERICAL-EVIDENCE}\Rightarrow\text{PROVED}$$非法。", "新反例或missingbranch可以重新打開舊closure。", "不應保護舊closure。", "##E.LinkBackmap每個新artifact如何連回：", "`ROUND-CLOSED``BRANCH-CLOSED``REPRESENTATION-CLOSED``CERTIFICATE-CLOSED`但只能在所有proofobligations真正完成後使用："], "W5": [r"\boxed{\text{UESFCM}\parallel\text{DLMVC}}", "8.Neo.KwithAletheia,*DLMVC—Deep-LagMulti-PassVerification&ClosureMethodology*,v0.1,2026."], "R1": ["**SemanticTargetContract：DEFINED**", "**UnboundedExpansion：DEFINED**", "**LinkBackOperator：DEFINED**", "**FiniteClosureState：DEFINED**", "**Self-ReferentialRecenter：DEFINED**", "**ProofObligationLedger：DEFINED**", "**ProblemClosure：DEFINED**", "**Anti-DriftGovernance：DEFINED**", "**UBErelation：DEFINED**", "**RCHMrelation：DEFINED**", "**SREG/PECrelation：DEFINED**", "**DLMVCrelation：DEFINED**", "**Formalconvergencetheorem：NOTCLAIMED**", "**Universalproofsolvability：NOTCLAIMED**", "**Empiricalbenchmarkvalidation：OPEN**"]}, "protocol": { "W1": ["`TARGET-FROZEN`", r"C_t=(G_t,O_t,B_t,D_t,P_t).", "`NULL`不進主proofgraph。"], "W2": [r"###Independence$$\operatorname{IndependenceClosed}_T(Q^\star)=1.$$###InvalidTarget`TARGET-FAILURE`###NoProgress`SEARCH-STALLED`注意：`SEARCH-STALLED`不等於：`PROVED`或`REFUTED`。", "→Stoponlyatproof/refutation/independenceclosure"], "W5": ["Lagged:oldclosure->blindreconstruct->audit->strengthen->handback"]}, } CLAIMS = { "vocabulary_claim": {"links": ["PROVES", "REFUTES", "REDUCES", "ELIMINATES", "REPRESENTS", "CERTIFIES", "BOUNDS", "CONNECTS", "OPENS", "META", "NULL"], "same_in_protocol": True, "sizes": {"links": 11, "links_protocol": 11, "obligations": 9, "artifacts": 15, "closures_21": 3, "closures_30": 5, "stalled": 1, "frozen": 1}, "repeated": [], "state": {"methodology": ["G_t", "O_t", "B_t", "R_t", "D_t", "V_t", "P_t", "K_t"], "protocol": ["G_t", "O_t", "B_t", "D_t", "P_t"]}, "banned": ["probably solved", "looks correct", "essentially proved"]}, "stopping_claim": {"exits": {"abstract": ["counterexample", "proof"], "sec. 3": ["counterexample", "proof"], "sec. 21": ["counterexample", "proof", "target-failure"], "sec. 50": ["counterexample", "proof"], "sec. 58": ["independence"], "sec. 61": ["counterexample", "independence", "proof"], "protocol sec. 7": ["counterexample", "independence", "proof", "search-stalled", "target-failure"], "protocol sec. 10": ["counterexample", "independence", "proof"]}, "distinct": 4, "sec. 21 says three": True, "sec. 49 stalls into more expansion": True, "protocol stops at SEARCH-STALLED": True, "pseudocode": {"loop": True, "breaks": 0, "handles": {"target failure": False, "search stalled": False, "independence": False}}}, "chain_claim": {"codes": [], "previous": [FIRST_STATE], "targets": [TARGET], "statuses": ["FINITE-CLOSED / PROBLEM-OPEN"], "problem_status": ["OPEN"], "schema": ["UESFCM-LUC-State-v0.1"], "dates": {"2026-09-19": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "2026-09-20": [11, 12, 13, 14, 15, 16, 17]}, "headers_agree": True, "problem_closed": False, "target_written_down": [], "first_state_mentions": ["UESFCM_Lebesgue_Cycle_01_Package_v0.1.zip!/UESFCM_Lebesgue_Cycle_01_B7_Separator_Gate_v0.1.md"], "named_files": [], "crystal_provenance": [5], "identities": 39, "identities_failing": []}, "labels_claim": {"discipline": {"crystal_strings": 15, "verdict_lines": 15, "violations": [], "closure_joined_to_evidence": {11: 2}}, "banned": {"probably solved": 0, "looks correct": 0, "essentially proved": 0}, "method_used": {"COMPUTE-DEFERRED": 4, "DEPENDENCY-DEFERRED": 2, "NUMERICAL-EVIDENCE": 14, "OPEN": 70, "OPENS": 1, "PROVED": 64, "REDUCED": 1, "REDUCES": 1, "REFUTED": 1, "REJECTED": 3, "SEARCH-ONLY": 2}, "method_unused": ["BOUNDS", "BRANCH-CLOSED", "CERTIFICATE-CLOSED", "CERTIFIED-COMPUTATION", "CERTIFIES", "CONNECTS", "COUNTEREXAMPLE", "COUNTEREXAMPLE-CLOSED", "DERIVED-CANDIDATE", "ELIMINATES", "FORMALIZATION-DEFERRED", "HIDDEN-BRANCH", "INVALID", "META", "MISSING-LEMMA", "NULL", "PROBLEM-PROOF-CLOSED", "PROOF-CLOSED", "PROVES", "REFUTES", "REOPENED", "REPRESENTATION-CLOSED", "REPRESENTATION-ONLY", "REPRESENTS", "ROUND-CLOSED", "SEARCH-STALLED", "SUPERSEDED", "TARGET-FAILURE", "VERIFIED-THEOREM-APPLICATION"], "own_labels": 84, "own_top": [["NOT-F3", 24], ["FINITE-CLOSED", 17], ["PROBLEM-OPEN", 17], ["AREA-PRUNED", 13], ["ORBIT-COVERED", 8], ["AREF-PRUNED", 8]], "cycle_status": ["FINITE-CLOSED / PROBLEM-OPEN"], "link_types_used": {1: ["REDUCES", "OPENS"]}, "cycle01_linkback_map": ["EXTERNAL-DATA", "CERTIFICATE-INTERFACE", "OPENS", "REDUCES", "SEARCH-ONLY", "SEARCH-PRIOR"], "format": {"recentre on entry": {"cycles": 17, "except": []}, "next recentre": {"cycles": 15, "except": [8, 10]}, "obligation or responsibility ledger": {"cycles": 10, "except": [1, 6, 7, 8, 9, 12, 15]}, "LinkBack section": {"cycles": 2, "only": [1, 3]}, "finite-closure section": {"cycles": 2, "only": [1, 2]}, "verdict": {"cycles": 17, "except": []}, "crystal's next recentre": {"cycles": 17, "except": []}}, "reopening": {"REOPENED": 0, "mentions": {16: ["# 10. Formal Responsibility Must Not Be Reopened"], 17: ["Do not reopen:", "Do not reopen the five tight-reference cells."]}, "all_prohibitive": True, "rejections": [3, 7, 15, 16]}}, "relations_claim": {"references": 9, "documents": {"UBE": False, "Paper 08": False, "UBGUL": False, "RCHM": False, "SREG / PEC": False, "RCIG": False, "DLMVC": True}, "mentioned_by": {"UBE": 0, "Paper 08": 0, "UBGUL": 0, "RCHM": 19, "SREG / PEC": 0, "RCIG": 0, "DLMVC": 1}, "lagged_line": "old closure -> blind reconstruct -> audit -> strengthen -> hand back", "dlmvc_sections": [True, True, True, True, True], "dlmvc_names_uesfcm": []}, } def a0_anchors(w): out = [] for doc, groups in ANCHORS.items(): text = gate.squash(w[doc]) out += [f"{doc} {cid}: anchor not found: {a[:50]}" for cid, frags in groups.items() for a in frags if a not in text] return out def w1_vocabulary(w): """sec. 6.1's eleven LinkBack types, in the protocol's order too; the obligation states (sec. 14), artifact statuses (sec. 40), closure labels (sec. 21, 30), SEARCH-STALLED (sec. 49), TARGET-FROZEN (protocol sec. 1); the closure state of sec. 9 and the protocol's smaller one""" v = vocabulary(w["text"], w["protocol"]) lists = {k: x for k, x in v.items() if k != "avoid"} got = {"links": v["links"], "same_in_protocol": v["links"] == v["links_protocol"], "sizes": {k: len(x) for k, x in lists.items()}, "repeated": sorted({x for k, xs in lists.items() if k != "links_protocol" for x in xs if xs.count(x) > 1}), "state": {"methodology": components(sec(w["text"], 9)), "protocol": components(sec(w["protocol"], 2))}, "banned": v["avoid"]} w["w1"] = got return [] if got["same_in_protocol"] and not got["repeated"] and got == w["vocabulary_claim"] else [f"the method's vocabulary: {got}"] def w2_stopping(w): """the states that end the loop, place by place: the abstract, sec. 3, sec. 21's closures, the pseudocode's returns, sec. 58, the one-line version, the protocol's stop conditions and its runtime line; what sec. 49 and the protocol do with SEARCH-STALLED""" got = stopping(w["text"], w["protocol"]) w["w2"] = got return [] if got == w["stopping_claim"] else [f"the stop rules: {got}"] def w3_chain(w): """the seventeen cycles as a chain of closure states: codes and previous states in sequence, one target, one status; the target and the first state, where they are written down; the crystals' own arithmetic and the counts each hands the next""" cycles = w["cycles"] hs = {i: header(c["doc"]) for i, c in cycles.items()} cr = {i: c["crystal"] for i, c in cycles.items()} ids = identities(cr) everything = "\n".join(c["doc"] + json.dumps(c["crystal"]) for c in cycles.values()) got = {"codes": [i for i, h in hs.items() if h["code"] != f"UESFCM-LUC-C{i:02d}-v0.1"], "previous": [hs[1]["previous"]] + [i for i in hs if i > 1 and hs[i]["previous"] != f"UESFCM-LUC-C{i - 1:02d}-v0.1"], "targets": sorted({h["target"] for h in hs.values()} | {x["target_id"] for x in cr.values()}), "statuses": sorted({h["status"] for h in hs.values()}), "problem_status": sorted({x["problem_status"] for x in cr.values()}), "schema": sorted({x["schema"] for x in cr.values()}), "dates": {d: [i for i in cr if cr[i]["date"] == d] for d in sorted({x["date"] for x in cr.values()})}, "headers_agree": all(hs[i]["date"] == cr[i]["date"] and cr[i]["cycle"] == i for i in cr), "problem_closed": "PROBLEM-PROOF-CLOSED" in everything, "target_written_down": sorted(set(w["mentions"]["target"]) - set(w["cycle_leaves"])), "first_state_mentions": [x[len(FOLDER):] for x in w["mentions"]["first_state"]], "named_files": [n for n in w["folder"] if re.search(r"(?i)target|cycle_00|C00", n)], "crystal_provenance": sorted(i for i, x in cr.items() if any(re.search(r"(?i)sha256|digest|parent|previous|provenance|source", str(k)) for path, _ in leaves(x) for k in path)), "identities": len(ids), "identities_failing": [k for k, ok in ids.items() if not ok]} w["w3"] = got return [] if not got["identities_failing"] and got == w["chain_claim"] else [f"the cycles' chain: {got}"] def w4_labels(w): """the cycles' labels against the method's: numerical evidence never marked proved or closed (sec. 45), sec. 40's banned phrases, which of the method's labels are used, the LinkBack types, sec. 39's round format, and reopening (I7)""" got = labels(w) w["w4"] = got return [] if not got["discipline"]["violations"] and not any(got["banned"].values()) and got == w["labels_claim"] else [f"the cycles' labels: {got}"] def w5_relations(w): """sec. 33-37 and the references: which related theories are in the archive, by document or by mention; the protocol's lagged line against DLMVC's sections; whether DLMVC or its case studies ever name UESFCM""" refs, d = w["refs"], norm(w["dlmvc"]) listed = re.findall(r"^\d+\. (.+)$", norm(w["text"]).split("# References")[1].split("# Canonical Source")[0], re.M) lagged = re.search(r"^Lagged:$\n^(.+)$", sec(w["protocol"], 11), re.M) got = {"references": len(listed), "documents": {k: len(v["named"]) > 0 for k, v in refs.items()}, "mentioned_by": {k: len(v["mentions"]) for k, v in refs.items()}, "lagged_line": lagged.group(1) if lagged else None, "dlmvc_sections": [bool(re.search(p, d, re.M)) for p in (r"^# 4\. Deep-Lag Target Rule", r"^## Pass A — Independent Reconstruction", r"^## Pass B — Adversarial Audit", r"^## Pass D — Theorem Strengthening", r"^# 12\. Frontier 回流規則")], "dlmvc_names_uesfcm": w["dlmvc_folder_mentions"]} w["w5"] = got return [] if got == w["relations_claim"] else [f"the relations: {got}"] def record_of(b): t = b.decode("utf-8") return {"sha256": hashlib.sha256(b).hexdigest(), "bytes": len(b), "lines": len(t.split("\n")), "utf8": True, "hidden_ascii_control_count": sum(1 for ch in t if ord(ch) < 32 and ch not in "\t\n\r"), "display_delimiters_paired": t.count("$$") % 2 == 0, "inline_delimiters_paired": t.replace("$$", "").count("$") % 2 == 0, "alternative_math_delimiters_present": bool(re.search(r"\\\[|\\\]|\\\(|\\\)", t))} def p1_package(w): """VALIDATION's record of each document, field by field, against its bytes hashed here and the archive's manifest row; its status and file list""" out, v = [], w["validation"] files = {DOC: w["doc_bytes"], PROTOCOL: w["protocol_bytes"]} recs = {r["file"]: r for r in v["canonical_files"]} if sorted(recs) != sorted(k.split("!/")[-1] for k in files) or v["status"] != "PASS": out.append("VALIDATION's file list or status") for leaf, b in files.items(): rec, mine, row = recs.get(leaf.split("!/")[-1], {}), record_of(b), w["manifest_rows"][leaf] if {k: rec.get(k) for k in mine} != mine: out.append(f"VALIDATION's record of {leaf.split('!/')[-1]}: {[k for k in mine if rec.get(k) != mine[k]]}") if (row[1], row[2]) != (mine["bytes"], mine["sha256"]): out.append(f"the archive's manifest row for {leaf.split('!/')[-1]}") w["p1"] = {"records": {leaf.split("!/")[-1]: record_of(b) for leaf, b in files.items()}, "lines": "newline count + 1"} return out _LINK = "a LinkBack type defined in sec. 6.1; no judgment" R43_DEFINITIONS = { "NOT CLAIMED": ("contextual", "sec. 62: a result the document names and expressly does not assert"), "PROVES": ("in-line", "sec. 6.1, a LinkBack type: the artifact proves the target or a necessary obligation directly"), "REFUTES": ("in-line", "sec. 6.1: the artifact is a counterexample or a contradiction"), "REDUCES": ("in-line", "sec. 6.1: the artifact reduces the problem to a smaller obligation"), "ELIMINATES": ("in-line", "sec. 6.1: the artifact excludes a branch or an escape"), "REPRESENTS": ("in-line", "sec. 6.1: the artifact builds a new exact representation"), "CERTIFIES": ("in-line", "sec. 6.1: the artifact supplies a proof, computation, interval or formal certificate"), "BOUNDS": ("in-line", "sec. 6.1: the artifact gives an upper or lower bound or an error budget"), "CONNECTS": ("in-line", "sec. 6.1: the artifact is a legal bridge between two nodes of the proof graph"), "OPENS": ("in-line", "sec. 6.1: the artifact finds a new necessary obligation or hidden branch"), "META": ("in-line", "sec. 6.1: the artifact changes the search or verification method, with proof that the change is valid for the target"), "NULL": ("in-line", "sec. 6.1: no substantive relation to the target found; kept out of the main proof graph (sec. 6.2)"), "PROOF-CLOSED": ("in-line", "sec. 21.1: ProofClosed(Q*) = 1, a finite proof artifact meeting the eight requirements listed there"), "COUNTEREXAMPLE-CLOSED": ("in-line", "sec. 21.2: a replayable counterexample in the target's domain, with no approximation false positive, " "verified to negate the canonical statement"), "TARGET-FAILURE": ("in-line", "sec. 21.3: the target itself is ill-defined, inconsistent or malformed; neither closure, and a new target " "version is built"), "ROUND-CLOSED": ("contextual", "sec. 30: a closure within one round, never the problem's; listed without further definition"), "BRANCH-CLOSED": ("contextual", "sec. 30: a closure of one branch, never the problem's; listed without further definition"), "REPRESENTATION-CLOSED": ("contextual", "sec. 30: a closure within one representation, never the problem's; listed without further definition"), "CERTIFICATE-CLOSED": ("contextual", "sec. 30: a closure by one certificate, never the problem's; listed without further definition"), "PROBLEM-PROOF-CLOSED": ("in-line", "sec. 30: usable only once every proof obligation is truly complete"), "SEARCH-STALLED": ("in-line", "sec. 49: rounds with no new branch, reduction, error reduction or obligation change; not a completion, " "and it triggers representation, method, literature, independent-AI or DLMVC expansion"), } R43_REVIEWS = [ ("OPEN", "Empirical benchmark validation", "reading", "PASS", "right: sec. 56 proposes benchmarks and none is run; the folder's seventeen Lebesgue cycles apply the method to one open problem " "with no control, as sec. 55 would need, and no DLMVC pass targets a cycle (W4, W5)"), ("DEFINED", "Semantic Target Contract", "reading", "PASS", "true as a text (sec. 2): Q* as a seven-part object, and versioning; its one application names a target that is written down " "nowhere in the archive (W3)"), ("DEFINED", "Unbounded Expansion", "reading", "PASS", "sec. 5"), ("DEFINED", "LinkBack Operator", "reading", "PASS", "sec. 6: eleven types, the protocol's the same (W1); the application labels artifacts with them in one cycle of seventeen (W4)"), ("DEFINED", "Finite Closure State", "reading", "PASS", "sec. 8-10: eight components; the protocol's state keeps five (W1)"), ("DEFINED", "Self-Referential Recenter", "reading", "PASS", "sec. 11"), ("DEFINED", "Proof Obligation Ledger", "reading", "PASS", "sec. 14-15"), ("DEFINED", "Problem Closure", "reading", "PARTIAL", "each closure is defined (sec. 21.1-21.3, 58), but the texts disagree on which states end the loop: two in the abstract, sec. 3 and " "the pseudocode (sec. 50), three in sec. 21, three others in sec. 61 and the protocol's runtime, five in the protocol's stop " "conditions - which include SEARCH-STALLED, a trigger for more expansion in sec. 49 (W2)"), ("DEFINED", "Anti-Drift Governance", "reading", "PASS", "sec. 7, 24-26, 42"), ("DEFINED", "UBE relation", "reading", "PASS", "written down (sec. 33); the UBE papers it cites are not in the archive (W5)"), ("DEFINED", "RCHM relation", "reading", "PASS", "written down (sec. 35); RCHM is named throughout the AMRAL rounds, but no RCHM document is in the archive (W5)"), ("DEFINED", "SREG / PEC relation", "reading", "PASS", "written down (sec. 36); the SREG / PEC series is not in the archive (W5)"), ("DEFINED", "DLMVC relation", "reading", "PASS", "written down (sec. 37, protocol sec. 11); the lagged line maps onto DLMVC's target rule, Passes A, B and D and return rule; " "DLMVC, of the same date, never names UESFCM (W5)"), ("NOT CLAIMED", "Formal convergence theorem", "reading", "PASS", "true: none is stated; sec. 55 Q3 asks it as a research question"), ("NOT CLAIMED", "Universal proof solvability", "reading", "PASS", "true, and disclaimed in sec. 57"), ("PROVES", "", "n/a", "n/a", _LINK), ("REFUTES", "", "n/a", "n/a", _LINK), ("REDUCES", "", "n/a", "n/a", _LINK), ("ELIMINATES", "", "n/a", "n/a", _LINK), ("REPRESENTS", "", "n/a", "n/a", _LINK), ("CERTIFIES", "", "n/a", "n/a", _LINK), ("BOUNDS", "", "n/a", "n/a", _LINK), ("CONNECTS", "", "n/a", "n/a", _LINK), ("OPENS", "", "n/a", "n/a", _LINK), ("META", "", "n/a", "n/a", _LINK), ("NULL", "", "n/a", "n/a", _LINK), ("TARGET-FAILURE", "21.3 Target Failure", "n/a", "n/a", "a terminal label named in sec. 21.3; no judgment"), ("PROOF-CLOSED", "21.3 Target Failure", "n/a", "n/a", "a terminal label named in sec. 21.3; no judgment"), ("COUNTEREXAMPLE-CLOSED", "21.3 Target Failure", "n/a", "n/a", "a terminal label named in sec. 21.3; no judgment"), ("ROUND-CLOSED", "30. Closed-for-Now 與 Proof-Closed", "n/a", "n/a", "a closed-for-now label listed in sec. 30; no judgment"), ("BRANCH-CLOSED", "30. Closed-for-Now 與 Proof-Closed", "n/a", "n/a", "a closed-for-now label listed in sec. 30; no judgment"), ("REPRESENTATION-CLOSED", "30. Closed-for-Now 與 Proof-Closed", "n/a", "n/a", "a closed-for-now label listed in sec. 30; no judgment"), ("CERTIFICATE-CLOSED", "30. Closed-for-Now 與 Proof-Closed", "n/a", "n/a", "a closed-for-now label listed in sec. 30; no judgment"), ("PROBLEM-PROOF-CLOSED", "", "n/a", "n/a", "the problem-level label of sec. 30; no judgment"), ("SEARCH-STALLED", "", "n/a", "n/a", "the stall label of sec. 49; no judgment"), ] def r1_registry(w): return registry.completeness(w["registry"], "UESFCM", w["definitions"], w["reviews"]) CHECKS = {"A0": a0_anchors, "W1": w1_vocabulary, "W2": w2_stopping, "W3": w3_chain, "W4": w4_labels, "W5": w5_relations, "P1": p1_package, "R1": r1_registry} DEPENDS = {"A0": {"text", "protocol"}, "W1": {"text", "protocol", "vocabulary_claim"}, "W2": {"text", "protocol", "stopping_claim"}, "W3": {"cycles", "mentions", "cycle_leaves", "folder", "chain_claim"}, "W4": {"text", "cycles", "labels_claim"}, "W5": {"text", "protocol", "dlmvc", "refs", "dlmvc_folder_mentions", "relations_claim"}, "P1": {"validation", "doc_bytes", "protocol_bytes", "manifest_rows"}, "R1": {"registry", "definitions", "reviews"}} def drill_cases(base): def edit(obj, fn): x = copy.deepcopy(obj) fn(x) return x def doc(i, old, new): def fn(c): assert old in c[i]["doc"], (i, old) c[i]["doc"] = c[i]["doc"].replace(old, new, 1) return edit(base["cycles"], fn) def crystal(i, fn): return edit(base["cycles"], lambda c: fn(c[i]["crystal"])) text, protocol, v = base["text"], base["protocol"], base["validation"] crlf = {i: {**c, "doc": c["doc"].replace("\n", "\r\n")} for i, c in base["cycles"].items()} stalled = " Obligations = Recenter(Q*, Ct)\n" return [ ("K0-unmodified", "control", {}, set()), ("K1-crlf", "control", {"text": text.replace("\n", "\r\n"), "protocol": protocol.replace("\n", "\r\n"), "cycles": crlf, "dlmvc": base["dlmvc"].replace("\n", "\r\n")}, set()), ("K2-validation-keys-sorted", "control", {"validation": json.loads(json.dumps(v, sort_keys=True))}, set()), ("M1-status-line", "mutation", {"text": text.replace("**Empirical benchmark validation：OPEN**", "**Empirical benchmark validation：PASS**")}, {"A0"}), ("M2-protocol-link-type", "mutation", {"protocol": protocol.replace("- `CONNECTS`", "- `CONNECT`")}, {"W1"}), ("M3-pseudocode-stall-exit", "mutation", {"text": text.replace(stalled, stalled + "\n if SearchStalled(Q*, Ct):\n return STALLED, StallReport\n")}, {"W2"}), ("M4-stall-stops", "mutation", {"text": text.replace("然後觸發：", "然後停止：")}, {"A0", "W2"}), ("M5-remaining-subroots", "mutation", {"cycles": crystal(12, lambda x: x["formal_progress"].update(remaining_subroots=75))}, {"W3"}), ("M6-target-drift", "mutation", {"cycles": crystal(9, lambda x: x.update(target_id="UESFCM-LUC-TARGET-v0.2"))}, {"W3"}), ("M7-target-contract-shipped", "mutation", {"mentions": {**base["mentions"], "target": base["mentions"]["target"] + [FOLDER + "UESFCM_Lebesgue_Target_v0.1.md"]}}, {"W3"}), ("M8-problem-closed", "mutation", {"cycles": doc(17, "`ROOT 6217 FORMAL CLOSURE: OPEN`", "`PROBLEM-PROOF-CLOSED`\n\n`ROOT 6217 FORMAL CLOSURE: OPEN`")}, {"W3", "W4"}), ("M9-diagnostic-proved", "mutation", {"cycles": crystal(9, lambda x: x["taylor_diagnostic"].update(status="PROVED"))}, {"W4"}), ("M10-reopened", "mutation", {"cycles": doc(5, "# 23. Cycle 06 Recenter", "`REOPENED`\n\n# 23. Cycle 06 Recenter")}, {"W4"}), ("M11-verdict-heading", "mutation", {"cycles": doc(8, "# 23. Cycle 08 Verdict", "# 23. Cycle 08 Summary")}, {"W4"}), ("M12-reference-in-archive", "mutation", {"refs": edit(base["refs"], lambda r: r["RCIG"]["named"].append("main.zip!/RCIG/RCIG_Runs_116_117.md"))}, {"W5"}), ("M13-dlmvc-names-uesfcm", "mutation", {"dlmvc_folder_mentions": [DLMVC]}, {"W5"}), ("M14-validation-digest", "mutation", {"validation": edit(v, lambda x: x["canonical_files"][0].update(sha256="0" * 64))}, {"P1"}), ("M15-document-bytes", "mutation", {"doc_bytes": base["doc_bytes"] + b"\n"}, {"P1"}), ("M16-review-dropped", "mutation", {"reviews": list(R43_REVIEWS[1:])}, {"R1"}), ("M17-definition-dropped", "mutation", {"definitions": {k: d for k, d in R43_DEFINITIONS.items() if k != "SEARCH-STALLED"}}, {"R1"}), ] def main(): ap = argparse.ArgumentParser() ap.add_argument("--drill", action="store_true") ap.add_argument("--blind", metavar="CID") args = ap.parse_args() base = load_inputs() def build(): return {**base, "registry": registry.load(), "definitions": dict(R43_DEFINITIONS), "reviews": list(R43_REVIEWS), **copy.deepcopy(CLAIMS)} if args.blind: CHECKS[args.blind] = lambda w: [] args.drill = True w = build() results = {} for c, fn in CHECKS.items(): try: results[c] = fn(w) except KeyError as e: results[c] = [f"claim missing: {e}"] for c, f in results.items(): print(f"{c} {'PASS' if not f else 'FAIL'}", *(f"\n {x}" for x in f[:6])) for key in ("w1", "w2", "w3", "w4", "w5", "p1"): print(key, "=", json.dumps(w.get(key), default=str, ensure_ascii=False)) if not args.drill: return cases = drill_cases(base) if args.blind: cases = [c for c in cases if args.blind in c[3]] d = gate.run_drill(build, CHECKS, DEPENDS, cases) summary = gate.summarize(d, CHECKS) print(gate.report_drill(summary)) for x in d: if not x["ok"]: print(" DRILL FAIL", x) if args.blind: n = sum(1 for x in d if args.blind in x["expected"] and args.blind not in x["tripped"]) print(f"blind {args.blind}: drill reported it blind in {n} cases (nothing written)") return log = {"run": "RUN-043", "subject": "UESFCM: the unbounded-expansion, self-referential finite-closure methodology, and its own application", "document": DOC, "checks": {c: {"pass": not f, "failures": f} for c, f in results.items()}, **{k: w.get(k) for k in ("w1", "w2", "w3", "w4", "w5", "p1")}, "drill": summary} LOG.write_text(json.dumps(log, ensure_ascii=False, indent=1, default=str) + "\n", encoding="utf-8") if not results["R1"]: registry.record("UESFCM", "RUN-043", R43_DEFINITIONS, R43_REVIEWS) print(f"registry: {len(R43_DEFINITIONS)} definitions, {len(R43_REVIEWS)} reviews recorded for UESFCM") if __name__ == "__main__": main()