SYNDEOM

Calibration infrastructure for mathematical proof triage.

SYNDEOM (συνδέω, syndéō, “to bind together”) is a research program for measuring how reliably triage methods detect flaws in mathematical proofs, and how much expert attention that detection costs. Its intended instrument combines labeled synthetic proofs, documented real examples, a versioned flaw taxonomy, and a calibrated detector battery for informal mathematics and Lean 4.

The principal deliverables are fooling length—where a detector becomes statistically equivalent to chance—and expert-minutes per true positive. A precisely measured failure to detect flaws is a valid result. Outputs about real manuscripts are triage scores with uncertainty; they are never verdicts.

Status · Architecture · Artifact contract · Calibration · Quick start · Repository · Governance

Research stage: S1 — ground-truth corpus. The manifest library, ingestion CLI, first canonical derivation producer, narrow positive-pair producer, and Lean verification fixture are implemented. Synthetic generation, the detector battery, calibration reports, and contact scoring remain planned work. This repository does not yet provide a calibrated proof-triage service.

Status

PR 7 activated the accepted first-parent amendment on main. The owner merged it at 2026-10-21T03:33:35Z (2026-10-20 23:33:35 America/New_York), producing 1c56028532ea135603dbad5423d5555313bfd9ec. Its tree exactly matches tested head a337375dbae49150a1a40fa46f6d1417835aadd2. The post-merge event records the actual merge, successful checks and fresh Rust reproduction separately from the prior owner acceptance and verified integration. The readiness assessment finds no additional substantive S1 exit criterion unmet for the admitted prefix. Gate S1 remains OPEN pending a separate genuine cold-start examination. The authoritative checklist and next action are in PROGRAM/STATE.md.

Surface	Implemented or recorded	Remaining boundary
Foundation	Ratified constitution; 14 flaw classes in taxonomy 0.1.0; S0 closed	Case-specific D3/SD12 exception is recorded in ADR-0003; no general classifier authority
Ground truth	Verified main: 35 archived representations, 32 effective logical items, two canonical children, one admitted positive pair	Canonical selection/context/locator review and external-byte verification remain separate scoring prerequisites
Rust engine	Manifest library; ingestion, derivation and pair CLIs; one-case effective inventory consumer	Producers and counting tools do not adjudicate other mathematical truth questions
Formal verification	Pinned Lean/Mathlib project, golden theorem and axiom audit	The witness's full analytic bridge is not formalized; no PROVEN transition
Calibration	Experimental design and phase gates specified	No synthetic corpus, calibrated battery, freeze tag or contact report yet

The effective map keeps s1_ingest-v0.1.0-63e23a952084 as the stable logical key, selecting s1_ingest-v0.1.0-15ab865466d6 exactly once for status. Both raw objects and their original producing revisions survive unchanged. The replacement carries the exact executor-written, hash-bound counterexample; S-0025 remains author error/locator evidence, not the source of that witness. It is a raw metadata amendment, not a canonical-child relation. The accepted candidate's historical proposed notes remain unchanged; the later owner decision and validated map activate its use.

The effective Rust inventory, reproduced byte-for-byte on merged main, reports 35 archived representations (33 raw, two canonical), 32 effective logical items, 46 flaw instances across five classes, nine zero-coverage classes and 30 logical items without canonical representations. Statement truth is 5 true / 17 false / 10 undetermined; offered-proof validity is 1 valid / 31 invalid. The unflagged subset is 18; truth-qualified counts are 5 true / 10 false. The seven older truth questions, seven severity questions and unnamed-result question retain their documented dispositions and exclusions. Missing raw lengths are not zero lengths.

The complete frozen S1.4 packet remains byte-for-byte historical: its 34-representation/32-root census, 17-item unflagged subset, first-parent hold, first-write bins and receipts describe the original pinned snapshot. The new event does not replace that report. Its canonical selections still measure 75 tokens / one informal proof step and seven tokens / zero informal proof steps; the latter is a statement pair. The 14-token Lean alias does not measure a transitive Mathlib proof. All real-item cells remain expected underpowered pending S3's design-derived N_min; no detector performance or numerical power follows from these metadata counts.

The status-support hold is discharged on verified main. Canonical production still needs its own authorized selection, context and locator review. Once this reconciliation is on main, a separate fresh session should attempt Gate S1's cold-start examination under §2/SD15 using constitution §6's Session-N resume prompt verbatim and alone. This informed session does not close Gate S1. S1.1 supports the admitted, unskipped prefix; the harvest is not exhausted. Harvest remains paused through candidate 27 / 1403.4485, with candidate 28 / 1403.6317 saved for a later harvest.

Orientation is governed by ADR-0008, the addendum to constitution §4.1 accepted by the owner on 2026-10-21: before any program state is reconstructed or any NEXT executed, a session fetches, discovers the default branch, records the fetched and checked-out SHAs and trees, selects the examined snapshot (fast-forward only for a clean behind-only checkout; an isolated worktree otherwise) and rechecks the target before publishing; scripts/orient_preflight.py performs and records it, outside the build gate. A later harvest of candidates 28–30 is preserved on branch claude/s1-harvest-candidates-28-30 at its recorded commit for admission review after Gate S1 closes (owner decision 1); its retrieval evidence is pinned in analysis/s1-orientation-repair/.

Architecture

SYNDEOM currently operates as a local, file-based research pipeline. Rust owns canonical manifest construction, canonical derivation, validation, and coverage aggregation; Lean checks the formal fixture; Python assists discovery and orchestrates reproduction. The repository holds the evidence, decisions, and execution record. There is no deployed API, queue, or database in the present implementation.

01 · Evidence into an archive

The S1.1 path begins with a published original and its erratum or retraction notice. The separate S1.2 path pairs one independently published statement with its reviewed Mathlib argument. Admission review establishes provenance, records the licence, and argues the flaw classification before the producer runs. The CLI validates structure and consistency, computes hashes, and writes the manifest.

%%{init: {"theme":"base","themeVariables":{"fontFamily":"Georgia, serif","fontSize":"14px","primaryColor":"#faf8f3","primaryTextColor":"#292723","primaryBorderColor":"#716b63","lineColor":"#81796f","edgeLabelBackground":"#faf8f3"},"flowchart":{"curve":"basis","nodeSpacing":30,"rankSpacing":45,"htmlLabels":true}}}%%
flowchart LR
    accTitle: S1 evidence and ingestion architecture
    accDescr: Primary sources and the flaw taxonomy inform admission review. Review supplies configuration and original bytes to the Rust ingestion tool, which uses the manifest library and writes the ground-truth archive. Review separately supplies the written record.

    S(("Primary<br/>sources")) -->|"original + notice"| R(("Admission<br/>review"))
    T(("Flaw<br/>taxonomy")) -->|"classification"| R
    R -->|"config + bytes"| I(("Rust<br/>ingest"))
    M(("Manifest<br/>library")) -->|"hash + self-check"| I
    I -->|"manifest.json"| A(("S1<br/>archive"))
    R -->|"RECORD.md"| A

    classDef default fill:#faf8f3,stroke:#716b63,color:#292723,stroke-width:1px;
    classDef focal fill:#fff5ef,stroke:#9c473b,color:#74372f,stroke-width:1.3px;
    class A focal;
    linkStyle default stroke:#81796f,stroke-width:1px;

Loading

Implemented relationships. Circles identify actors or artifacts; arrows name their contribution.

• lab/ retrieves candidates and comparison material; it has zero result authority.
• engine/ingest/ implements the deterministic producer s1_ingest. It rejects inconsistent inputs and refuses conflicting content under an existing artifact ID.
• engine/manifest/ implements schema checks, byte-format parsing, hashes, commanded-versus-achieved fidelity, and parent/derivative consistency checks.
• engine/derive/ implements s1_derive: reviewed statement/proof slices from one gzip TeX source become canonical informal Markdown, with the full original source retained as external context. It validates actual bytes, inherited labels, and mapped flaw locations.
• engine/pair/ implements the fixed ADR-0007 archive/canonical pair contract, with executable-input provenance, actual-byte validation, full output preflight and fresh receipts.
• analysis/s1-4/ publishes the Rust-owned inventory, qualified coverage, frozen length bins and interim-power statement. The example target lives outside the pair producer's frozen source closure; Python only orchestrates reproducibility checks.
• groundtruth/ retains the archival item and its written evidence. lean/ supplies the separate formal build and axiom-audit path.

Admission and licensing are review obligations: the CLI checks their input shape, not the underlying scholarship or redistribution rights. The procedure is ADR-0003 for errata and ADR-0007 for the reviewed positive pair.

Artifact contract

Every counted proof artifact has a manifest. The current producer writes syndeom-manifest/2; the library also accepts /1 under its original rules. Consumers pin the schema they understand. ADR-0001 defines the contract and amendments.

02 · Identity, bytes, and provenance

%%{init: {"theme":"base","themeVariables":{"fontFamily":"Georgia, serif","fontSize":"14px","primaryColor":"#faf8f3","primaryTextColor":"#292723","primaryBorderColor":"#716b63","lineColor":"#81796f","edgeLabelBackground":"#faf8f3"},"flowchart":{"curve":"basis","nodeSpacing":30,"rankSpacing":42,"htmlLabels":true}}}%%
flowchart LR
    accTitle: Artifact identity and content integrity
    accDescr: Canonical JSON configuration is hashed to form a configuration hash. Its prefix joins the producer identity and optional seed to form the artifact ID. The manifest records that identity, the exact-byte content hash, and the engine commit separately.

    C(("Config")) -->|"JCS + SHA-256"| H(("Config<br/>hash"))
    H -->|"first 12 hex"| ID(("Artifact<br/>ID"))
    P(("Producer<br/>+ seed")) -->|"id + version"| ID
    ID -->|"identity"| M(("Manifest"))
    B(("Proof<br/>bytes")) -->|"SHA-256"| M
    E(("Engine<br/>commit")) -->|"provenance"| M

    classDef default fill:#faf8f3,stroke:#716b63,color:#292723,stroke-width:1px;
    classDef focal fill:#fff5ef,stroke:#9c473b,color:#74372f,stroke-width:1.3px;
    class M focal;
    linkStyle default stroke:#81796f,stroke-width:1px;

Loading

Artifact identity is derived from configuration and producer identity. Content integrity is checked separately against the exact file bytes.

config_hash = SHA-256(JCS(config))
content_hash = SHA-256(exact file bytes)
artifact_id = <generator.id>-v<version>-<config_hash[0:12]>[-s<seed>]

JCS is the JSON Canonicalization Scheme. Synthetic artifacts carry an integer seed; ground-truth and contact items carry seed: null and omit the suffix. The manifest also records origin, producer version, engine commit, file formats and storage, ground truth where permitted, and commanded/achieved statistics with fidelity verdicts. Formal files carry their toolchain pins.

Origin	Location	Ground-truth basis	Use
synthetic	corpora/	by-construction	Planned S2 generation and S3 calibration
ground-truth	groundtruth/	documented-by-source or formalized-in-mathlib	S1 evidence; later S4 validation
contact	contact/	ground_truth: null	S5 only; quarantined until the prescribed gates pass

Archival and detector inputs are distinct. raw/1 preserves original bytes. The detector interface is specified for syndeom-informal-md/1 (proof.md) and syndeom-lean/1 (Proof.lean). A real item to be scored needs a derived canonical artifact naming config.derived_from and config.method, preserving its parent's status and flaw labels, and documenting re-expressed locations. The first derivation producer and one canonical child now exist under ADR-0006: s1_derive-v0.1.0-c08f9e3ec092, derived from s1_ingest-v0.1.0-00f28e252823. The reviewed procedure preserves the original offered proof; it does not repair its argument. Metadata, the source map, and the source-fidelity review are committed; restricted proof/context bytes are external. The existing Lean golden audit does not formalize or certify this informal child. The separate first-parent status-support hold is discharged on verified main following PR 7's merge. Canonical selection/context/locator review remains separate.

Statement truth and proof validity are independent fields. Schema /2 permits an undetermined statement (value: null, method: "undetermined") only with an invalid proof. Ten current items have this status. They may contribute to proof-flaw calibration, but must be excluded from truth-dependent cells, including the FLAW-0011 and FLAW-0012 composites. correct: false on such an item does not assert that its theorem is false.

Storage is explicit: committed retains permitted bytes; external retains a manifest and digest without redistributing the original; regenerable is reserved for synthetic artifacts. Synthetic proof bytes default to regeneration and hash verification; manifests remain committed.

Calibration and validation

The following is the specified research architecture, not an implemented scoring path. Three populations remain separate: synthetic artifacts establish calibration, real proofs with documented status test the frozen battery, and AI-generated contact corpora are examined last.

03 · Three populations, one frozen protocol

%%{init: {"theme":"base","themeVariables":{"fontFamily":"Georgia, serif","fontSize":"14px","primaryColor":"#faf8f3","primaryTextColor":"#292723","primaryBorderColor":"#716b63","lineColor":"#81796f","edgeLabelBackground":"#faf8f3"},"flowchart":{"curve":"basis","nodeSpacing":34,"rankSpacing":44,"htmlLabels":true}}}%%
flowchart LR
    accTitle: Planned calibration, blind validation, and contact boundary
    accDescr: Synthetic proofs calibrate a battery that is then frozen. The fixed protocol is validated on real ground-truth proofs. Only after the S4 gate passes can the same frozen version score quarantined AI contact corpora. Contact results never modify that version.

    S(("Synthetic<br/>S2")) -.->|"calibrate in S3"| F((("Frozen<br/>battery")))
    F -.->|"fixed protocol"| V(("Blind test<br/>S4"))
    G(("Real proofs<br/>S1")) -.->|"documented status"| V
    V -.->|"gate passes"| O(("Triage<br/>S5"))
    C(("AI corpora<br/>quarantined")) -.->|"read only"| O
    F -.->|"same version"| O

    classDef default fill:#faf8f3,stroke:#716b63,color:#292723,stroke-width:1px;
    classDef boundary fill:#fff5ef,stroke:#9c473b,color:#74372f,stroke-width:1.3px;
    class F,C boundary;
    linkStyle default stroke:#81796f,stroke-width:1px;

Loading

Dashed arrows are planned execution paths. The double ring marks the immutable battery version; red identifies the freeze and contact boundary. Contact observations cannot tune that version.

Phase	Required outcome	State
S0 · Foundation	Verified sources, ratified rules, manifest schema, taxonomy, reproducible scaffold	Closed
S1 · Ground truth	Sourced real items, canonical derivatives, informal–formal pairs, coverage and power statement	Open
S2 · Generator	Seeded informal/formal variants, flaw injection, padding, measured generation fidelity	Planned
S3 · Calibration	Detector battery, ROC/AUC with intervals, fooling lengths, cost model, referee design, battery-freeze-v1	Planned
S4 · Validation	Blind test on S1 items; class-specific recall, false-positive rates, and power analysis	Planned
S5 · Contact	Versioned manuscript triage scores with uncertainty; reproducible report and engineer sign-off	Planned

The first generator family is specified as seeded Rust templates and grammars. Any LLM-assisted family requires a separate ADR covering reproducibility and leakage. The planned battery prioritizes dependency extraction, hypothesis checks, lemma usage, citation existence, autoformalization, statement fidelity, and axiom audits. Surface statistics remain controls whose expected weakness must be tested.

Calibration crosses detector × flaw class × proof length × severity, with matched correct proofs, padded correct proofs, and other flaw classes as controls. Leave-one-generator-out and leave-one-flaw-class-out evaluations test whether detectors recognize flaws or merely generators. Conclusions require joint detector evidence within measured false-positive and ROC contexts. The 14-class taxonomy includes both local errors and failures that compilation alone cannot establish, such as statement drift and uninformative padding.

“Fooled” has a pre-declared statistical meaning. A cell qualifies only when its 95% bootstrap AUC interval lies entirely within [0.45, 0.55] and its sample size meets N_min. Fooling length is the smallest tested length meeting that rule, per detector and flaw class. An interval merely containing 0.5 is “not distinguished from chance”; an insufficient cell is “underpowered.” N_min must be derived for balanced flawed/correct cells at 90% power when true AUC is 0.5, then simulation-checked before curves are computed. Dependence among variants of one seed theorem must be accounted for. See ADR-0004.

Expert cost initially uses a pre-declared review-time model. The blinded human-referee protocol is to be designed and versioned; recruitment, contact, and execution require the engineer of record's decision. A post-contact battery change creates a new version and freeze; prior results retain their original version.

Quick start

Use Git, Bash, Python 3, Rust through rustup, and Lean through elan. On Windows, run the shell examples in Git Bash with Python, Cargo, and Lake on PATH. Keep the checkout and scratch files on a local disk outside OneDrive.

Dependency	Repository pin
Rust	1.91.0, with clippy and rustfmt — rust-toolchain.toml
Lean	leanprover/lean4:v4.34.1 — lean/lean-toolchain
Mathlib	d13f23b723b8a846827a245b89c10fc7d3f11612 — lean/lakefile.toml
Dependency locks	engine/Cargo.lock and lean/lake-manifest.json

From a local parent directory:

git clone https://github.com/Quigles1337/Syndeom.git
cd Syndeom

# Populate the compiled Mathlib cache, then run the complete repository gate.
(cd lean && lake exe cache get)
bash scripts/check.sh

The first run downloads dependencies and compiled Lean modules; allow time and disk space for Mathlib. The gate checks the Lean build and golden fixture's axiom set, Rust formatting and Clippy, all Rust tests, LF/BOM/trailing-newline hygiene, and register cross-references. A successful run ends with GATE: GREEN. CI runs the same gate as an advisory check; the recorded local run is authoritative.

Exercise ingestion without writing a corpus item

From the repository root, this dry run uses the checked-in test fixture, whose source IDs are placeholders. It prints a manifest and leaves groundtruth/ untouched.

cargo run --locked --manifest-path engine/Cargo.toml -p syndeom-ingest -- \
  --config engine/ingest/tests/fixtures/item-a.json \
  --bytes engine/ingest/tests/fixtures/original.bin \
  --root . \
  --engine-commit "$(git rev-parse HEAD)" \
  --dry-run

Real ingestion follows ADR-0003: register the original and notice, resolve storage rights, prepare the item config, run the producer, then add the written record and harvest-log entry. Test fixtures are never admitted as real evidence.

CLI exit	Meaning
0	Manifest printed, written, or already identical
1	Usage or I/O error
2	Input shape or manifest consistency failure
3	Different manifest or bytes already exist under that artifact ID

For a Rust-only development check, run cargo test --locked --manifest-path engine/Cargo.toml --all-targets --all-features. This is a partial check; it does not replace the repository gate.

Reproduce the first canonical derivation

Follow the S1.3 reproduction instructions. The Python helper verifies the original source hash and invokes the Rust producer twice, comparing exact proof, context, manifest, and source-map bytes. Choose a new external work directory for each run; existing destinations are refused. The retained evidence pins producer commit 49e47237924eddf0c39c24aefad0eb9aa02ee8b3, which predates generation of the real child.

Reproduce the admitted first positive pair

Follow the S1.2 implementation instructions. The helper retrieves frozen sources, invokes the committed Rust producer, compiles/audits the actual emitted alias, compares a fresh replay and runs labeled refusal controls. Every run uses a new external destination. The owner admitted this pair by merging PR 4; this reproduction preserves its original producing revision and does not imply PROVEN promotion.

Reproduce the effective inventory

Use the post-merge reproduction instructions. The existing Rust consumer validates the one-case amendment and historical preservation, then emits one effective status per logical item. Choose a fresh external output directory; the wrapper compares two runs and confirms overwrite refusal. Inventory bytes match the retained result when inputs are unchanged; provenance names the actual checkout revision/tree.

Repository map

Path	Responsibility
PROGRAM/	Constitution, current state, claims, sources, taxonomy, ADRs, and session history
engine/manifest/	Canonical Rust schema, identity, byte formats, fidelity, and consistency library
engine/ingest/	Deterministic S1 ingestion CLI, tests and the one-case effective inventory example
engine/derive/	Deterministic reviewed TeX derivation CLI and mechanical tests
engine/pair/	Narrow reviewed positive-pair archive/canonical CLI, provenance and refusal tests
lean/	Pinned formal project, golden theorem, and axiom audit
lab/	Exploratory Python candidate discovery and examination
groundtruth/	Real archival manifests, canonical child metadata and recipes, item records, permitted originals, and harvest log
corpora/	Reserved for manifested synthetic artifacts in S2
contact/	Reserved for quarantined AI-generated corpora in S5
analysis/	Engineering evidence and future experimental designs and calibration/validation/contact reports
analysis/s1-3/	First canonical derivation receipts, preservation checks, and reproduction instructions
analysis/s1-2/	Historical procedure evidence, separate source-map correction, implementation and proposed-admission evidence
analysis/s1-4/	Complete frozen historical coverage packet and first-write bins
analysis/s1-first-parent-integration/	Accepted ruling, separate effective inventory and preserved integration evidence
analysis/s1-post-merge-readiness/	Actual main activation, fresh reproduction and criterion-by-criterion S1 readiness
sources/	Source copies whose licences permit redistribution
scripts/	Local verification gate and register checks
scripts/reproduce_s1_3.py	Source retrieval and orchestration of two independent Rust derivations
scripts/orient_preflight.py	ADR-0008 orientation preflight: fetch, snapshot selection, receipt, pre-publication recheck (not part of the gate)
scripts/orient_preflight_cases.py	Offline verification of the preflight against temporary Git repositories
analysis/s1-orientation-repair/	Owner decisions of 2026-10-21, held-harvest evidence pins, preflight cases and live receipts, preservation and gate receipts

Governance and contribution

The constitution and recorded architectural decisions govern the program. This README is an orientation layer. Begin work with STATE.md, the latest HANDOFF.md entry, and the relevant decisions; verify their claims against the code and gate.

Evidence rule	Practical consequence
Truth and triage, not understanding	No scores for insight, pedagogy, or explanatory quality
No manuscript verdicts	Report detector scores, uncertainty, battery version, and named flaw classes
“Proven” is reserved	Require sorry/admit-free Lean, an axiom audit allowing at most propext, Classical.choice, and Quot.sound, and recorded line-by-line statement-fidelity review
Reproducibility is required	Results record engine SHA, seeds, configuration, taxonomy/battery versions, and uncertainty
Contact is quarantined	Freeze before validation and contact; never tune an existing battery from contact observations
Evidence has an audit trail	Sources and claims live in registers; decisions and session handoffs preserve the reasoning

Use feature branches for work in progress, preserve UTF-8/LF text, run scripts/check.sh, and record evidence in the session handoff. Commit messages follow [S<phase>][<CLAIM-ID or ADR-ID or FLAW-ID or INFRA>] imperative summary. Public release, constitutional amendments, and human-referee participation follow the engineer-of-record decisions specified in the constitution.

Reading paths: constitution for scope; state for readiness; claims for assertions and evidence; sources for provenance; taxonomy for flaw semantics; decisions for contracts; handoff for continuity.

SYNDEOM combines the calibration discipline of FRIEDMAN with the formal-methods discipline of KOBER. The sibling interface is a versioned manifest extension; neither sibling's code is imported. The structural map records the relationship.

Licence

SYNDEOM's original software and technical documentation are released under the Apache License 2.0 (SPDX Apache-2.0; full text in LICENSE).

This release excludes third-party materials under sources/, groundtruth/, and contact/, which retain the terms recorded in PROGRAM/SOURCES.md. It also excludes separately controlled DARQ Labs research materials: these are marked where they appear, remain proprietary, and are outside the Apache release.

The engineer of record established this boundary on 2026-10-13 in ADR-0000, Addendum 2. Licence-text provenance is recorded as S-0019 in the source register.