Finite Python proof-of-concept checker for selected-terminal run-to-status transport in Ledgered Scientific Availability.

Paper:

Takahashi, K. (2026). Constraint Generative Theory: Typed Constraint Effects
and Scientific Availability. Zenodo.
Supplement: Ledgered Scientific Availability.
DOI: 10.5281/zenodo.20426928

DOI link: https://doi.org/10.5281/zenodo.20426928

The paper is the source of truth. This repository is an independent finite PoC, not a theorem prover and not a complete mechanization of CGT.

For exact implemented scope and non-claims, see docs/limitations.md.

It checks whether a supplied finite selected-terminal run can be transported into one purpose-indexed status:

• available
• blocked
• informational_only

The main executable object is StatusTransportRecord. It ties together a selected terminal proof, extracted terminal rows, coordinate-level rows coverage, decision transport, registry coverage, residue modes, NonSynth, projection coherence, severe evidence tensor coupling, and BuildStatus.

Expected theoretical failures are returned as data: markers, debts, frontiers, rows reports, transport agreement reports, and blocked statuses. The checker fails closed.

Ledgered Scientific Availability separates three claims:

terminal proof success != visible report success != scientific availability

A terminal proof can replay and spend its terminal row. A projected report can look positive. Final availability can still be blocked by a missing source witness, stale session, open positive-coordinate registry alias, hidden-report mismatch, retained residue, NonSynth debt, unwitnessed decision target, projection mismatch, or uncoupled severe evidence tensor.

This is the central point of the repository: availability is not a raw report. It is the result of selected-terminal run-to-status transport plus BuildStatus.

The finite pipeline is:

1. Build an EffectProfile and ReportProjection.
2. Build a finite capability object with branches.
3. Select one branch and write only its digest to the ledger.
4. Replay ordinary evidence without generating terminal wins.
5. Check replay identity and replay delta.
6. Check terminal kind, liveness, spend certificate, and terminal delta.
7. Commit terminal spend.
8. Extract terminal rows.
9. Build RowsCoverageReport with coordinate categories and dependency witnesses.
10. Build TransportAgreementReport.
11. Check decision target, registry residual report, residue modes, NonSynth, projection coherence, and severe tensor coupling.
12. Run BuildStatus.

The PoC also exposes a CertifiedAvailabilityFragment for audit output. It connects the finite effect profile, report projection, projected report, marker/residue nucleus, and boundary-status digest. It is explanatory and checkable; it is not the full CGT effect-profile calculus.

uv sync
uv run pytest

Run the successful toy availability case:

uv run python -m cgt_ledgered_availability.cli run-example examples/toy_availability.json

Sample abbreviated output:

selected branch: <branch digest>
terminal kind: SessionSpend
replay result: ok
terminal spend result: terminal_spend_ok
decision transport result: {"tag": "ResolutionValue", ...}
final status: {"tag": "available", ...}

Run the natural-kind case where decision transport is neutral:

uv run python -m cgt_ledgered_availability.cli run-example examples/natural_kind_availability.json

Run the causal-power frontier case, where the report is positive but availability is blocked by extrapolation residue:

uv run python -m cgt_ledgered_availability.cli run-example examples/causal_power_frontier.json

Explain profile/report/status separation:

uv run python -m cgt_ledgered_availability.cli explain-example examples/toy_availability.json

Inspect the finite audit bundle:

uv run python -m cgt_ledgered_availability.cli audit-example examples/toy_availability.json

audit-example prints the status transport record, rows coverage report, coordinate dependency witnesses, transport agreement report, registry residual report, decision target witness, projection coherence result, severe tensor result, certified availability fragment, and final status.

This repository does not implement:

• proof search,
• a full formal proof assistant,
• the full CGT effect-profile calculus,
• setoids, categories, or functorial semantics,
• infinite contexts or general measurable selector theory,
• general registry alias theory,
• the complete NonSynth audit universe,
• the full dynamic residue LTS,
• the complete severe-evidence algebra,
• cryptographic trust.

Digests are deterministic structural identifiers, not a security model. The JSON examples are readable finite case descriptors, not a general proof assistant input language.

See docs/limitations.md.

• Theory mapping
• Transport record schema
• Run-to-status walkthrough
• Ledgered availability kernel
• Concepts for engineers
• API overview
• Failure catalog
• Limitations

Apache License 2.0. Runtime dependencies are empty. Tests use pytest. The repository contains no secrets, credentials, telemetry, generated binary artifacts, databases, web APIs, or hidden external calls.

Takahashi, K. (2026). Constraint Generative Theory: Typed Constraint Effects
and Scientific Availability. Zenodo.
Supplement: Ledgered Scientific Availability.