This repository is intentionally certificate-only. As of tag chronos-certificates-frozen, the Chronos depth constants and related artifacts are frozen, cryptographically signed, and treated as canonical. The files chronos_constants.json and Chronos/Cert/ChronosDepthConstants.lean, together with their corresponding .minisig signatures, constitute the complete, verifiable Chronos certificate set. No Chronos theory is developed here: all mathematical definitions, transport lemmas (including the PSH → boundary-overlap conditional), and proofs live upstream in urf-core. Any modification to the frozen artifacts requires an explicit unfreeze decision, regeneration of signatures, and a new freeze tag.
This project relies on shared tooling and reproducibility infrastructure provided by the scientific-infrastructure repository; it contains domain-specific research code only.
The clause-transcript entropy approach to resolution lower bounds has been formally closed (see chronos-urf-rr).
Support-symmetric and linear entropy functionals cannot capture resolution hardness.
Active direction: Communication Information Complexity of Search_F.
See: chronos-urf-rr/manuscripts/communication_information_reduction chronos-urf-rr/manuscripts/tseitin_ic_lower_bound
docs/CERTIFICATE_BOUNDARY_NOTE_2026_04.md— conditional note specifying the weakest certificate-boundary audit compatible with the repository's frozen certificate-only scope.
This repository is governed by docs/status/LEAN_PROOF_PORTFOLIO_CLASSIFICATION.md. Its role in the portfolio is explicitly classified as proof-facing, conditional frontier, infrastructure/documentation, or legacy/scaffold.
This repository is governed by docs/status/EXTERNAL_STATUS_LOCK.md. Build success, CI success, dashboards, ledgers, axioms, admits, sorry, or placeholder witnesses do not constitute theorem-level closure.