Completion, Lean coverage, and confidence
Recorded 2026-10-27 · Komorebi P.
Filter by discipline, completion and proof evidence · Browse the collection · Start here · Repository home
Completion, Lean coverage, and confidence describe different things. A finished book may contain open research. A checked Lean proof may belong to an unfinished project. Choose a completion stage below, open a work's evidence record, then follow its paper, proofs, Lean, and code link.
This guide summarizes the existing release and status records at source revision 4c09d41f2793. It covers 90 primary components and 71 supporting collections. The labels report those records, rather than a new proof review or Lean run. Each recorded pass keeps its original date and scope.
Finalization queue · Detailed evidence catalogue · Component/file index · Machine-readable status
Reader selection and soundness
Lean is optional. A clear written proof, exact finite certificate, or appropriately scoped experiment can support its own claim. File counts, formatting, and compilation alone do not establish soundness. The records guide brings together dated reviews, claim coverage, the files each record covers, and software checks. Read each report's scope and unresolved findings before relying on its conclusions.
Entries deferred from the main reading lists remain in the incubator, with their source and status records intact. The component counts below describe the complete selected inventory, including those deferred entries.
Completion stages
| Stage | Primary entries | Meaning |
|---|---|---|
| Scoped release | 10 | The release record marks the stated mathematical or executable requirements as complete. The scope below defines what is covered. |
| Reading edition complete | 41 | The stated manuscript or reader set is released. Formal coverage, review depth and wider research can remain incomplete. |
| Active development | 19 | A candidate, working manuscript or bounded research milestone with identified unfinished work. |
| Experiment / prototype | 12 | A research instrument, implementation or experiment whose tested scope does not establish a general scientific endpoint. |
| Reader available, source qualification pending | 1 | The PDF edition and reading scope have been identified. Matching editable sources, full page review, and reproducible build qualification remain pending. |
| Needs assessment | 6 | Available material lacks a sufficient assessed source/status record for a stronger label. |
| Earlier checkpoint | 1 | An earlier edition kept with its own evidence. Later acceptance records do not change that evidence. |
These categories describe the state of a work. They are not percentages or a ranking of mathematical importance. “Scoped release” means the stated release requirements are recorded as complete. Broader claims and implementations may remain unfinished. “Reading edition complete” means the stated manuscript or reader set has been released. It does not imply journal acceptance or a completed research program.
“Reader available” means the PDF edition and its reading scope have been identified. Matching editable sources, a full page review, and a reproducible build still need checking. This label does not establish mathematical confidence or a completed reading edition.
Lean coverage
| Label | Meaning |
|---|---|
| Declared contract recorded | The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses. |
| Selected results recorded | Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied. |
| Inherited / related evidence | The edition relies on earlier or related formal evidence. That evidence is not a fresh full-edition replay. |
| Source available, no current pass | Lean text is present, but the assessed edition has no accepted current compiler pass. |
| No Lean claim | The assessed scope claims writing, calculations or experiments rather than Lean verification. |
| Not assessed | No formal-coverage assessment is made. |
“Declared contract” covers only the registered claims in the linked map. Modules, declarations, named theorems, proof bodies and finite test cases count different things, so their totals cannot be combined into a project completion percentage. A source map, file hash, Lean guide PDF or inventory does not establish that Lean accepted a proof. Evidence from an earlier edition keeps its own scope and does not certify a changed or expanded edition.
Confidence basis
| Label | What supports confidence |
|---|---|
| Recorded formal evidence | Strong evidence for the exact checked subset, conditional on correct formal statements, source correspondence, dependencies and recorded execution. |
| Historical formal evidence | Earlier/related formal records support their own scope. Current-edition replay or expanded coverage may be missing. |
| Recorded written review | The cited edition records a scoped written review and/or proof audit with its stated depth. Finite checks support only their tested claims. |
| Written / finite evidence | Written arguments, author review or bounded computations. These records do not establish independent review or formal assurance. |
| Experimental evidence | Confidence is limited to the stated experiment, fixture, prototype or engineering tests. Generalization and scientific endpoints remain separate. |
| Unassessed | There is not enough assessed evidence for a confidence classification. |
Confidence labels identify the strongest recorded evidence for the stated subset. They do not assign a probability that the whole project is correct. A record can contain checked results alongside open or refuted claims. A written review covers only its stated scope and does not imply external peer review. Lean proofs still need correct hypotheses and a faithful match to the written statements. Experiments support claims about the populations, inputs, and conditions actually tested.
All executable software remains beta / work in progress, including implementations attached to completed mathematical releases. See LICENSE.md for the current reuse terms. Older undecided notices remain part of the historical record.
Scoped release (10)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates | Declared contract recorded | Recorded formal evidence |
| Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets | Declared contract recorded | Recorded formal evidence |
| Paper X: Universal Residual Seeds and Conditional Occupied-System Completion | Declared contract recorded | Recorded formal evidence |
| Proof Path Theory | Selected results recorded | Recorded formal evidence |
| Large Signal Model | Declared contract recorded | Recorded formal evidence |
| Certified Inference | Declared contract recorded | Recorded formal evidence |
| Constructive Repair | Selected results recorded | Recorded formal evidence |
| Komorebi Space | Declared contract recorded | Recorded formal evidence |
| Realization Boundaries | Declared contract recorded | Recorded formal evidence |
| Machine Native Reasoning | Declared contract recorded | Recorded formal evidence |
Reading edition complete (41)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory | Selected results recorded | Recorded formal evidence |
| Paper IV: Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data | Selected results recorded | Recorded formal evidence |
| Paper V: Polyphase Signal Calculus | Inherited / related evidence | Historical formal evidence |
| Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations | Inherited / related evidence | Historical formal evidence |
| Paper VII: Quantum Seed Calculus | Inherited / related evidence | Historical formal evidence |
| Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization | Inherited / related evidence | Historical formal evidence |
| Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation | Selected results recorded | Recorded formal evidence |
| Paper XI: Packets, Arithmetic Realization, and Conditional Comparison | Selected results recorded | Recorded formal evidence |
| Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion | Inherited / related evidence | Historical formal evidence |
| Realization Calculus | Inherited / related evidence | Historical formal evidence |
| Komorebi Methodology | No Lean claim | Recorded written review |
| Special Functions | Selected results recorded | Recorded formal evidence |
| Machine Societies | No Lean claim | Recorded written review |
| Sufficient Resolution | Inherited / related evidence | Historical formal evidence |
| Quantum and Circuits | Selected results recorded | Recorded formal evidence |
| Physics | Selected results recorded | Recorded formal evidence |
| COS Method | Selected results recorded | Recorded formal evidence |
| Self-Improving Intelligence | No Lean claim | Recorded written review |
| Self-Improving Intelligence: visual guide | No Lean claim | Recorded written review |
| Grounded Abstraction | No Lean claim | Recorded written review |
| Machine Understanding | No Lean claim | Recorded written review |
| OSL and Neuralese | No Lean claim | Experimental evidence |
| OSL and Neuralese: reading edition | No Lean claim | Experimental evidence |
| Stratified Recursive Improvement Closure | No Lean claim | Experimental evidence |
| AVOC | Inherited / related evidence | Historical formal evidence |
| Hypergraph Lumpability and Bayesian Refinement | No Lean claim | Recorded written review |
| Certified Bayesian Inference | Inherited / related evidence | Historical formal evidence |
| Stratified Relational Workspace Theory | No Lean claim | Recorded written review |
| ABC: source and evidence reader | Selected results recorded | Recorded formal evidence |
| Beal: source and evidence | Selected results recorded | Recorded formal evidence |
| Catalan Constant: source and evidence | No Lean claim | Recorded written review |
| Collatz and Riemann: source and evidence | No Lean claim | Recorded written review |
| Hilbert 12: cubic divisor development | Selected results recorded | Recorded formal evidence |
| Hodge: source and evidence | Source available, no current pass | Recorded written review |
| Inverse Galois: source and evidence | No Lean claim | Recorded written review |
| Lehmer: source and evidence | No Lean claim | Recorded written review |
| The Possibility for a Machine Native Mathematics | No Lean claim | Unassessed |
| Prime-Contact Coherence Calculus | No Lean claim | Recorded written review |
| Signal Reconstruction | Inherited / related evidence | Historical formal evidence |
| Stratified Universality | Source available, no current pass | Recorded written review |
| Strong Artin: source and evidence | Inherited / related evidence | Historical formal evidence |
Active development (19)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Information Realization | Selected results recorded | Recorded formal evidence |
| KZFC and Residual Reflection | Selected results recorded | Recorded formal evidence |
| Logical Resolution | Selected results recorded | Recorded formal evidence |
| p-adic Canonical Realization | Selected results recorded | Recorded formal evidence |
| Representation Calculus | Selected results recorded | Recorded formal evidence |
| COS Method: formal continuation | Selected results recorded | Recorded formal evidence |
| Machine Native Reasoning: wider continuation | Inherited / related evidence | Historical formal evidence |
| ABC: global RR8 branch | No Lean claim | Recorded written review |
| AddMul Arithmetic Reconstruction | Selected results recorded | Recorded formal evidence |
| Euler Signal Bridge | No Lean claim | Written / finite evidence |
| Hilbert 12: ambient dual slice | No Lean claim | Written / finite evidence |
| Hilbert 12: analytic Fourier branch | No Lean claim | Written / finite evidence |
| Hilbert 12: closure attempt | No Lean claim | Written / finite evidence |
| Hilbert 12: contracting ambient torsion | No Lean claim | Written / finite evidence |
| IUT Valuation Hulls | Selected results recorded | Recorded formal evidence |
| Model-Theory Normalization | Selected results recorded | Recorded formal evidence |
| Resolution Semantics | Selected results recorded | Recorded formal evidence |
| Seeded Two-Axis Calculus | No Lean claim | Written / finite evidence |
| Streaming Polyphase Factor Decomposition / SKAT | No Lean claim | Written / finite evidence |
Experiment / prototype (12)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Agent Dynamics | No Lean claim | Experimental evidence |
| Arithmetic J-Space Training Lab | No Lean claim | Experimental evidence |
| J-Space Causal Lab | No Lean claim | Experimental evidence |
| J-Space Collections | No Lean claim | Experimental evidence |
| Workspace Incubator | No Lean claim | Experimental evidence |
| RRCT multispace convergence protocol | No Lean claim | Experimental evidence |
| RRCT | No Lean claim | Experimental evidence |
| SRIC: external semantic admission | No Lean claim | Experimental evidence |
| SRIC: endogenous semantic witness | No Lean claim | Experimental evidence |
| PRISM-1R | No Lean claim | Experimental evidence |
| PRISM-1 | No Lean claim | Experimental evidence |
| Universal Generative Deformation Calculus | No Lean claim | Experimental evidence |
Reader available, source qualification pending (1)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Gaussian Elimination: collected guide | Not assessed | Unassessed |
Needs assessment (6)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Large Signal Model software | Not assessed | Unassessed |
| Machine Theory Compendium | Not assessed | Unassessed |
| Physics: curvature states | Not assessed | Unassessed |
| Physics: energy and backreaction | Not assessed | Unassessed |
| Physics: origin locking | Not assessed | Unassessed |
| Realization Calculus: twin edition | Not assessed | Unassessed |
Earlier checkpoint (1)
| Project and exact scope | Lean | Confidence basis |
|---|---|---|
| Machine Theory: formal development | Selected results recorded | Recorded formal evidence |
Supporting and earlier material
The 71 supporting collections are listed separately in the evidence catalogue. Their import receipts identify the available files. This guide does not reassess their mathematics or transfer a newer edition's coverage and completion label to them.
| Additional material | Status in this assessment |
|---|---|
| Research Preview 1 | Earlier import, not reassessed here. Consult its own formal records and their stated scope. |
| Quadratic-Form Engine / K-COS (earlier edition) | Earlier import. Use the current COS monograph and separate formal continuation for the current assessment. |
| AM-SPD | Earlier import. The software remains beta / work in progress. No new scientific assessment is reported here. |
| Komorebi Math | Independent Python library in beta / work in progress. Qualification is tracked in that repository. |
| Polyphase Float | Independent C library in beta / work in progress. Qualification is tracked in that repository. |
Maintaining the distinctions
Maintainers can edit the assessments and cited evidence in manifests/project-status.json, then run python tools/update_completion_status.py. Use --check to validate IDs, evidence bindings, and generated pages without writing them. The component index uses the same labels. A changed source, expanded statement or new accepted run requires a reviewed status update. Uploading files alone does not change their completion or confidence status.
To strengthen a formal status, supply the exact claim map, pinned source and environment, accepted compiler and axiom records, appropriate controls, and any required review of how the formal and written statements correspond. To finalize a reading edition, identify its editable source and matching PDF, complete the relevant build and page checks, and preserve its mathematical scope. Wider research and experimental goals remain separate queue items.