Project status and evidence catalogue
Browse the collection · Status guide · Finalization queue
Base assessment recorded 2026-10-27. Each entry summarizes dated evidence for a particular source edition, with later companion checks linked separately. Rendering this catalogue does not run Lean or review proofs. The status guide defines the labels. Each primary entry links back to the work's paper, proofs, Lean, and code. Supporting collections link to their source files and import receipts. File hashes and the assessed Git revision are recorded in project-status.json.
Paper I: Typed Operator Systems, Seed Rank, and Exact Packet Coordinates
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
69 accepted proof-level correspondences in the stated manuscript scope. 108 correspondence records are not 108 theorems.
Next step: Maintain the exact statement map and reproduce the pinned formal contract before a changed release.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · README.txt · RELEASE_REPORT.txt
Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
53/53 proof-level scopes have recorded replay and accepted correspondence. Admissible contour existence remains an application assumption.
Next step: Preserve the contour hypotheses and rerun the recorded contract after any mathematical change.
Return to this work: paper, proofs, Lean, and code
Source directory · RELEASE_STATUS.json · README.md · SERIES_STATUS.json
Paper III: Typed Transfer, Nonlinear Packets, and Obstruction Theory
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Technical reading release is complete. The accepted 16-module core does not cover the expanded monograph. The historical full-coverage count is uncertified.
Next step: Map the expanded packet-Taylor, Stirling/Touchard and later corollaries to explicit missing formal obligations.
Return to this work: paper, proofs, Lean, and code
Source directory · RELEASE_STATUS.json · README.md · tools/README.md
Paper IV: Cyclic Analytic Functions, Reciprocal Families, and Spectral Zero Data
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
68 scoped results have recorded formal acceptance.
Next step: Maintain the scoped release and its reproducible sources.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · Paper_IV_Verification_Closeout_v1.1.0/README.md · Paper_IV_Verification_Closeout_v1.1.0/RELEASE_SCOPE.md
Paper V: Polyphase Signal Calculus
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Publication 1.2.0 closes its stated scope. 20 finite formal core results and 225 theorem targets are inherited evidence, separate from the larger manuscript.
Next step: Replay the inherited formal core with the pinned runtime. Retain the documented E11.1 amendment and current reproduction entry point.
Return to this work: paper, proofs, Lean, and code
Source directory · README.txt · SERIES_STATUS.json
Paper VI: Transfer Semigroups: Stochastic, Bayesian, Fractional, and PDE Realizations
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Publication closeout is complete. The inherited 33-result finite formal contract does not cover all 142 theorem-like statements or the broader analytic program.
Next step: Build a claim-by-claim expansion plan for the ordinary-proof material. Preserve finite-state and common-gap hypotheses.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SERIES_STATUS.json · README.txt
Paper VII: Quantum Seed Calculus
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Prose/proofreading release is complete. 19 inherited finite formal items are separate from the book. All five physical continuum targets remain open.
Next step: Separate the finite formal correspondence from the five continuum research obligations in any next release.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SERIES_STATUS.json · README.txt
Paper VIII: Packet Operator Algorithms, Exact Compilation, and GPU Realization
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Internal publication release is complete. The inherited finite formal contract excludes numerical QR/SVD and canonical singular-value API identification. GPU execution was not performed.
Next step: Choose a bounded numerical or GPU validation target and record actual execution before expanding implementation claims.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SERIES_STATUS.json · README.txt
Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Accepted reading release preserves scoped arithmetic, dyadic and lifting formal work. Broader extensions and the Euler reciprocal endpoint remain open.
Next step: Reconcile the current claim map with the narrowed threshold-free theorem and retain the refuted stronger statement as history.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · publication/README.txt · sources/visual_README.md
Paper X: Universal Residual Seeds and Conditional Occupied-System Completion
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
The amended 20/20 contract is conditional. Transported targets and a summand in a supplied carrier are separate outputs. General arithmetic attachment remains open.
Next step: Keep the amended contract distinct from stronger historical attempts. Supply missing comparison and arithmetic inputs before any stronger promotion.
Return to this work: paper, proofs, Lean, and code
Paper XI: Packets, Arithmetic Realization, and Conditional Comparison
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Finite packet and selected terminal developments have accepted formal evidence. Conjecture 66 and its arithmetic realization obligations remain open.
Next step: Track each Conjecture 66 obligation separately from the accepted finite packet and transported constructions.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · formalization/README.md · publication/source/lean_guide/README.md
Paper XII: Patching Support, Hecke Packets, and Conditional Automorphic Completion
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
49 revised claims map to 291 production targets in historical evidence. Original wording remains 41 complete, seven partial, one unchecked. Arithmetic and automorphic inputs remain explicit.
Next step: Replay the pinned amended contract and preserve the original-versus-amended concordance. Do not promote missing arithmetic premises.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · core/README.md
Realization Calculus
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
The 2,714-page collected book is an editorial assembly. Formal coverage and open endpoints remain chapter-specific.
Next step: Maintain the chapter-to-edition map and verify any rebuilt volume against its component source and page accounting.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · source_v_viii/README.md · source_v_viii/book_edit_baseline/README.md
Proof Path Theory
Scoped release · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Publication 1.8.0 formalizes the finite trace checker and typed JSON exchange on existing proof-field semantics. Arbitrary Python correctness and broader manuscript coverage remain open.
Next step: Define a separate Python-to-Lean refinement target and preserve the distinction between rejected certificates and infeasibility.
Return to this work: paper, proofs, Lean, and code
Source directory · STATUS.md · README.md · evidence/README.md
Komorebi Methodology
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Reviewed essay with written arguments and 40 finite exact-check groups. No new Lean compilation or corpus-wide formal audit.
Next step: Maintain claim-to-evidence links and arrange a focused external review of the unbounded arguments before stronger assurance claims.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · audit/CLAIM_MAP.json · requirements.txt
Large Signal Model
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
87/87 registered propositions have complete formal mappings under explicit model assumptions. Empirical model success is outside that contract.
Next step: Maintain the 87-row map and repeat the accepted build/axiom/replay gates for a changed release.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · Lean/README.md · Monograph/README.md
Special Functions
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Proofread reading volumes plus 465 named theorem declarations: 39 inherited finite-core names and 29, 21, 19, 16, 13, 19, 23, 22, 16, 34, 22, 26, 43, 27, 36, 30, 30 in Blocks01 through 17. Registered F.1-F.3, G.1, guarded G.2, named ancillary F, main H.1 and J mathematical evaluation/normalization/finite arrays are complete. J now also has an exact guarded-majorant algorithm specification with explicit resource failures and abstract validation order; successful returns certify actual bounds and endpoints. Full Python runtime/dictionary refinement remains open. Ordinary type convergence is conditional. Other J/F/H, I and A-E remain; no whole-book percentage is established.
Next step: Compose typed certified-evaluation metadata, tail and endpoint fields from the proved arrays and guarded majorant, then establish actual Python source/runtime/dictionary refinement with explicit assumptions; retain other J/F/H, I and A-E.
Return to this work: paper, proofs, Lean, and code
Latest written review and its scope
Source directory · LEAN_STATUS.md · README.md · lean/README.md
Machine Societies
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
118-page reading edition. Bound self-review records cover 38 of 62 statement/proof pairs: 36 recorded as proved as written, two qualifications (memory domain and computability class), and 24 unreviewed. Coverage is not whole-book certification.
Next step: Review the remaining 24 pairs in bounded batches. In a revised source edition, state the positive finite-index condition for the memory bit bound and the event-emitting compilation premise for the computability theorem and its certificate consequence. Keep empirical and independent review separate.
Return to this work: paper, proofs, Lean, and code
Latest written review and its scope
Certified Inference
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
Finished one-observation, finite-dimensional Gaussian inference contract with exact factor-coded data and checked termination/output certificates. No sampler or universal Python parser refinement.
Next step: Maintain proof-producing instance checks. Treat Python results as provisional until the emitted Lean instance passes.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · RUNTIME_METADATA/README.md · RELEASE_SCOPE.md
Constructive Repair
Scoped release · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Qualified beta distribution of the 1.0.0rc3 Python runtime. Linux x86_64 and Windows Server 2025 x86_64, both with CPython 3.13.5, passed 134 engine tests and 72 installed cases. Linux passed all 100 release tests; Windows passed 97 with the three named POSIX-only skips. Both symlink rejection controls passed on both platforms. The identical wheel's seven runtime files match the 2,254-file imported source. Historical Lean evidence retains its own scope; this qualification performs no new kernel replay.
Next step: Use the qualified beta and its exact source/wheel/receipt record. Rerun the qualification workflow for future candidates. Other interpreters, operating systems, architectures, integration adapters, and fresh Lean execution require their own evidence.
Return to this work: paper, proofs, Lean, and code
Software check and tested scope (separate from Lean evidence)
Source directory · README.md · python_baseline/README.md · docs/LICENSING_STATUS.md
Information Realization
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
The first formal block contains 58 theorem declarations across six production modules. The whole information program is not formalized.
Next step: Choose the next result beyond the checked linear repair and Haar contracts and retain their coefficient assumptions.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · AUDIT_REPORT.md · LEAN_GUIDE.md
Komorebi Space
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
All sixteen principal theorem groups have formal counterparts. The recorded integrated verification covers 166 targets. Application hypotheses remain explicit.
Next step: Preserve the sixteen-group correspondence and repeat the integrated verification for any changed source release.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · lean/README.md · examples/README.md
KZFC and Residual Reflection
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
The depth-zero and multiverse blocks are checked. The arbitrary complete obstruction tower can be vacuous. No model existence follows from the conditional extraction theorem.
Next step: Finish the internal compactness-to-filter-extension converse or specify a nonvacuous constrained tower before proposing a stronger axiom.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · README_v0.10.0_PREDECESSOR.md · verification_v0.3.0_fresh/README_HISTORY.md
Logical Resolution
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
13 checked modules and 112 theorem declarations cover the standard-syntax bridge and relational layer. Arbitrary formula preservation is outside the stated interface.
Next step: Take the bounded target in CONTINUE_HERE and preserve the quantifier-sensitive observation contract.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · FORMALIZATION_COVERAGE.md · source_records/PARENT_FORMALIZATION_COVERAGE.md
p-adic Canonical Realization
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Cross-realization theorem establishes the stated finite linear minimality and uniqueness. Minimum module cardinality is not minimum DFA size.
Next step: Complete the efficient executable compiler refinement separately from the mathematical realization theorem.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · REPORT.md · REPRODUCE.md
Realization Boundaries
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
45/45 registered monograph contracts are complete in the checked companion, with exact documented semantics.
Next step: Maintain the final coverage map and v1.0.0 acceptance pointer. Older verification README labels remain historical.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · docs/MONOGRAPH_COVERAGE.md
Representation Calculus
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
The generic adapter and 202 frozen matrix certificates are checked. The build covered 235 local modules. Most declaration counts include inherited or generated facts.
Next step: Extend the executable refinement only under the stated encoding and coefficient hypotheses. Preserve the nonlinear-encoding boundary.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · FORMALIZATION_COVERAGE.md · source_records/v0.3_README.md
Sufficient Resolution
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Complete publication of v0.16.0 contracts with 93 formal source modules. The publication edition records no fresh Lean run.
Next step: Restore the matching runtime and execute the full pinned formal replay before upgrading the current verification label.
Return to this work: paper, proofs, Lean, and code
Source directory · RELEASE_STATUS.json · README.md · formal/README.md
Machine Native Reasoning
Scoped release · Lean: Declared contract recorded · Confidence basis: Recorded formal evidence
Accepted v1.0.0 admission covers 27/27 selected Reviewed Core results. The separately published reconstructed 97-chapter, 977-page edition retains component-specific assurance; this admission does not certify the whole expanded book.
Next step: Maintain the completed core and reconcile statement-level correspondence with the published expanded reconstruction under F03.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · release/ADMISSION_RECORD.json · release/REPORT.md
Quantum and Circuits
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Complete 344-page publication with explicit open research. 211 named declarations across thirteen formal modules cover selected arithmetic/circuit developments, not the full book.
Next step: Map the remaining ordinary-proof chapters and open physical targets separately from the thirteen checked modules.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · volume/README.md · release_tools/README.md
Physics
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Complete 572-page book with an accepted scoped centered free-field extension. Fixed infinite Fourier-space results do not close sampled-grid, interacting-field or cosmological targets.
Next step: Resolve the spectral-functional-calculus API identification and distinguish current Block 51 receipts from older modular build limitations.
Return to this work: paper, proofs, Lean, and code
COS Method
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Closing 138-page publication with a finite Gram/enclosure Lean companion. Full numerical correctness is outside the official companion.
Next step: Keep the official monograph stable and route end-to-end numerical proof work to the separate continuation.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · lean/README.md
COS Method: formal continuation
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Checked intermediate branch connecting Gaussian/spectral reductions and rational acceptance. Spectral inclusion and COS endpoint enclosures remain premises.
Next step: Prove or certify the numerical spectral inclusion and endpoint enclosure inputs before claiming end-to-end verification.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · docs/COVERAGE.json · CONTINUE_HERE.md
Self-Improving Intelligence
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Theoretical publication with 30 statement/proof pairs and finite reference constructions. No deployed autonomous agent or indefinite acceleration result.
Next step: Obtain focused review of the theorem chain and design a separate empirical evaluation of the integrated architecture.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · visual-guide/README.md · lineage/v0.6.0/README.md
Self-Improving Intelligence: visual guide
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Finished visual companion with focused checks. The original research suite was not rerun for the guide.
Next step: Maintain source locators and guide checks when the parent manuscript changes. Inherit no extra proof or empirical status.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · REVIEW_NOTES.md · READING_NOTES.md
Grounded Abstraction
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
First-edition theoretical manuscript with twenty written statements and exact examples. No agent training campaign or Lean certificate.
Next step: Review the new quantitative extension and keep calibration and learning assumptions visible in subsequent work.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SOURCE_MAP.md · NEXT_THEORY.md
Machine Understanding
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Frozen first-edition theoretical/editorial scope with twenty statements, bounded exact tests and explicit interpreter/resource charges.
Next step: Pursue external proof review and separate empirical acquisition from the supplied observation and recipient models.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · FIRST_EDITION_SCOPE.md · CHANGELOG.md
Agent Dynamics
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Executed illustrative two-agent model with supplied schedule, sensor semantics and reset rule. No learned policy or general self-improvement result.
Next step: Validate any learned or adaptive replacement against a preregistered baseline. Retain the supplied-rule demonstration as its own experiment.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SOURCE_MAP.md · REVIEW_NOTES.md
Arithmetic J-Space Training Lab
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Candidate arithmetic subspace protocol with JSPACE_CLAIM=NOT_ESTABLISHED. Required mediation and native shared-access assays are absent.
Next step: Complete the mandatory causal assays and a locked confirmatory cohort before changing the claim ceiling.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · EXPERIMENT_DESIGN.md · WORKSPACE_PROTOCOL.md
J-Space Causal Lab
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Research instrument for candidate causal states using saved models and retained failed assays. Not a J-space certificate.
Next step: Resolve the recorded relay failures and run matched intervention/mediation checks on fixed settings.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · provenance/v1_2/README.md · provenance/v1_1_README.md
J-Space Collections
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Typed object collections and workspace actions. Programs and proposals are supplied, and no new training was performed.
Next step: Evaluate a learned controller separately from the hand-supplied examples and test the Windows wrapper on its target host.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · PROTOCOL.md · VERIFICATION.md
Workspace Incubator
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Executed adaptive continuation with positive and negative transfer/retrieval outcomes. Native shared-workspace gaps remain open.
Next step: Run a genuinely held-out, balanced cohort and retain repeated-access and no-wire failures in the primary result.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · REPORT.md · requirements-recorded.txt
OSL and Neuralese
Reading edition complete · Lean: No Lean claim · Confidence basis: Experimental evidence
Frozen manuscripts and experiment evidence plus an exact finite interface. Learned results, failures and unspent experiments retain separate statuses.
Next step: Reconcile each learned claim with its own frozen run and keep the supplied finite demonstrator separate from learned-decoder claims.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · interface/README.md · OSL/core05/README.md
OSL and Neuralese: reading edition
Reading edition complete · Lean: No Lean claim · Confidence basis: Experimental evidence
Compact reading edition of OSL/Neuralese. Historical experiments and executable runtime belong to the separate complete edition.
Next step: Maintain links to the complete evidence edition and avoid assigning executable or Lean status from manuscript availability.
Return to this work: paper, proofs, Lean, and code
Source directory · OSL_Neuralese_Manuscripts_v1.0/README.md · OSL_Neuralese_Manuscripts_v1.0/publication/README.txt · CURRENT_READING_EDITION.txt
RRCT multispace convergence protocol
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
The available evidence covers the protocol and numerical smoke checks. The primary multi-family causal campaign is incomplete, and the Qwen runner was not executed in the recorded build.
Next step: Execute the source-locked primary campaign with all required independent estimator families and mediation gates.
Return to this work: paper, proofs, Lean, and code
Reader listing: incubator. Only synthetic estimator execution is recorded. The actual Qwen and primary causal runs are absent.
Requirements for returning to the reading list: Run the frozen-model smoke with authenticated inputs and report its descriptive scope. Any workspace claim additionally requires the full primary causal, mediation, and replication gates.
Source directory · README.md · VALIDATION_REPORT.md
RRCT
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Beta research platform. The single-seed preset passes three diagnostic links and fails planner necessity and recurrence specificity.
Next step: Freeze a replicated holdout campaign and resolve or report the failed later links before claiming the full chain.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · runs/README.md · vendor/README.md
SRIC: external semantic admission
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Source-locked external-model protocol with infrastructure tests. The real Coconut checkpoint has not been executed in this release.
Next step: Authenticate the exact checkpoint and dataset, run the frozen adapter and admission gates, then report the actual result.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · frozen/README.md · REAL_EXECUTION_STATUS.md
SRIC: endogenous semantic witness
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Finite synthetic semantic-witness construction and fake-runtime pilot checks. No external-checkpoint result.
Next step: Lock the real checkpoint digest and execute the pilot without substituting fixture metrics for model evidence.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · REAL_LRM_PILOT_STATUS.md · RESULTS.md
Stratified Recursive Improvement Closure
Reading edition complete · Lean: No Lean claim · Confidence basis: Experimental evidence
Complete finite-fixture publication/evidence package. The real latent-reasoner pilot remains unexecuted.
Next step: Keep the completed synthetic benchmark separate from the external-model campaign and its unfilled source lock.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · SRIC_v2.4_Block23_REAL_LRM_PILOT_STATUS.md · SRIC_v2.4_Block23_BUILD.txt
AVOC
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Complete reading set based on archived formal v0.41.0. Publication checks did not execute Lean or the actual Lean endpoint.
Next step: Restore the exact runtime and replay the archived source and endpoint before labeling the publication as freshly formal-verified.
Return to this work: paper, proofs, Lean, and code
Source directory · AVOC_Publication_1.0/README.md · AVOC_Publication_1.0/source/AVOC_Formal_v0.41.0/README.md · AVOC_Publication_1.0/publication/README.txt
Hypergraph Lumpability and Bayesian Refinement
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Internally complete manuscript and finite certificates. External proof and literature-priority reviews remain pending.
Next step: Complete the independent proof review and systematic comparison to related quotient/lumping theories before journal submission.
Return to this work: paper, proofs, Lean, and code
Source directory · MANUSCRIPT_STATUS.md · README.md · CHANGELOG.md
PRISM-1R
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
The evidence covers the architecture and semantic reference tests. The RTL is an uncompiled interface skeleton with candidate bit packing.
Next step: Compile and simulate the RTL, then synthesize and measure an FPGA prototype before making hardware performance claims.
Return to this work: paper, proofs, Lean, and code
Reader listing: incubator. The hardware is an uncompiled interface skeleton with success tie-offs. No hardware qualification has been run.
Requirements for returning to the reading list: Replace success tie-offs with real generation, certificate, dependency and fault inputs. Compile/simulate the RTL and retain meaningful rejection controls. Hardware performance requires separate measured evidence.
Source directory · README.md · BUILD_STATUS.md
PRISM-1
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Behavioral architecture, planner and cost model. No production RTL, synthesis, timing or measured silicon result.
Next step: Build a bit-accurate FPGA Packet Streaming Multiprocessor and report measured results under a fixed output contract.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · rtl_skeleton/README.md
Certified Bayesian Inference
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Publication companion for the scoped single-observation Gaussian inference contract. Source excerpts and archived formal coverage are not universal Python correctness.
Next step: Link the publication claims to the canonical Certified Inference contract and replay its source-bound proof-producing examples.
Return to this work: paper, proofs, Lean, and code
Source directory · Certified_Bayesian_Publication_1.0/README.md · Certified_Bayesian_Publication_1.0/source/FD_Certified_Inference_Core_v1.0.0_Checked/README.md · Certified_Bayesian_Publication_1.0/publication/README.txt
Stratified Relational Workspace Theory
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Complete preprint monograph with finite regression checks. External mathematical and empirical review remains pending.
Next step: Obtain external review and evaluate empirical claims separately from finite mathematical regression tests.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · audits/README.md · verification/README.md
Machine Theory: formal development
Earlier checkpoint · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Earlier Block 15 checkpoint covers 23/27 selected results. The later Reviewed Mathematical Core admission covers 27/27 in a different source edition.
Next step: Use the newer core for current completion status. Preserve this checkpoint and its original four pending targets as dated history.
Return to this work: paper, proofs, Lean, and code
Current counterpart: Machine Native Reasoning.
Source directory · README.md · REVIEW_NOTES.md · CONTINUE_HERE.md
Machine Native Reasoning: wider continuation
Active development · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
The older 74-page continuation retains its historical 23/27 core map. A separate reconstructed editorial edition now supplies all 97 chapters in thirteen parts, 977 pages, and verified editable TeX. The accepted selected-core contract does not certify the expanded book.
Next step: Use the published reconstruction and its immutable PDF/source identities to reconcile expanded statements with the accepted 27/27 core and assess remaining claims (F03). Historical TeX recovery is not required to build this edition.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · sources/core/README.md
ABC: global RR8 branch
Active development · Lean: No Lean claim · Confidence basis: Recorded written review
Scoped written radical-cost identities and obstructions. The global ABC target and exceptional-prime tail remain open. No new Lean run.
Next step: Address the documented large-exceptional-prime budget or another justified arithmetic comparison. Do not promote local bounds to ABC.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · abc_work/base/ABC_Two_Sided_Radical_Euler_Law_2026-10-25/README.md · abc_work/komorebi_arithmetic/COMPARISON_STATUS.json
ABC: source and evidence reader
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Finished evidence reader with selected formal conditional interfaces. The actual arithmetic/IUT witness and uniform abc inequality are not supplied.
Next step: Keep the missing source-witness theorem and uniform arithmetic estimate explicit before any endpoint claim.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · evidence/FORMAL_STATUS.md · evidence/recovered/KTG_Block03_Preserved_Payload/PROJECT_STATUS.md
AddMul Arithmetic Reconstruction
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Three positive Lean units and exact finite controls cover finite observation, filter budgets and a carry example. No global height mechanism.
Next step: Formulate and prove the next arithmetic comparison beyond the finite reconstruction class before making a global-height claim.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · RESEARCH_NOTE.md · evidence/results.json
Beal: source and evidence
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Finished reader with selected checked algebraic scopes. Neither general Beal nor the recovered signature route is closed.
Next step: Supply the actual arithmetic affine obstruction/realization input and retain the upstream Frey and residual-pattern assumptions.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · evidence/FORMAL_STATUS.md · evidence/computation/contracts/block67_status.json
Catalan Constant: source and evidence
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Finished exposition/evidence set with written recurrence arguments and finite checks. Irrationality of Catalan's constant remains open.
Next step: Establish the missing uniform arithmetic bounds and review external claims at their exact versions before promotion.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · evidence/CURRENT_STATUS.md · MANIFEST.json
Collatz and Riemann: source and evidence
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Finished reader/visual sets with scoped arguments, exact reductions and finite checks. Both conjectures remain open.
Next step: Track each universal endpoint separately from finite orbit checks, models and conditional reductions.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · collatz_visual/README.md · archive/v1.0/README.md
Euler Signal Bridge
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Written identities and bounded exact controls with checked source inputs. The maintained example includes formal-series and local arithmetic derivations, Fibonacci and polynomial operator transport, quartic displacement/period/isometry laws, and finite-mode/logarithmic Euler encodings. Same-assistant reviews and pinned API comparisons are separate evidence. No new formalization, independent review or global classification is asserted.
Next step: Independent mathematical review and any broader arithmetic classification require their own hypotheses and evidence. Keep finite tests, written self-review, externally cited theorem inputs and any future formalization distinct.
Return to this work: paper, proofs, Lean, and code
Source directory · READ_ME.txt · exact_results.json · computation_manifest.json
Gaussian Elimination: collected guide
Reader available, source qualification pending · Lean: Not assessed · Confidence basis: Unassessed
45-page collection compiled 7 October 2026 from four source PDFs and two reflowed arithmetic notes. Edition, source map, and rendered front matter inspected. The compilation explicitly reports no new source-experiment or Lean replay. Mathematical confidence remains unassessed.
Next step: Recover the exact editable assembly and matching source editions, reproduce the PDF, inspect every page, and reconcile source-specific proof and formal records (F07).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only) · Komorebi_Gaussian_Elimination_Collected_Pages.pdf
Hilbert 12: ambient dual slice
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Exact finite algebra and a fixed-point obstruction. The analytic comparison remains open.
Next step: Connect the exact dual-slice construction to a justified analytic comparison without assuming the missing equality.
Return to this work: paper, proofs, Lean, and code
Source directory · H12_Ambient_Dual_Slice_Research_Note.md
Hilbert 12: analytic Fourier branch
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Written algebraic/Fourier reductions and exact checks with floating diagnostics. The gamma-to-class-field equality remains unproved.
Next step: Prove the exact special-value comparison. Use directed enclosures for numerical bounds and keep them separate from equality.
Return to this work: paper, proofs, Lean, and code
Source directory · H12_Analytic_Fourier_README.md · H12_Analytic_Resolvent_Verification_Log.txt · H12_Analytic_Fourier_Resolvent_Research_Note.md
Hilbert 12: closure attempt
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Interval certificate bounds a ratio distance below 10^-60 and resolves a branch condition. It does not establish exact equality.
Next step: Prove the remaining exact analytic identity. Numerical closeness alone cannot close the class-field comparison.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · inherited_seven_replay.txt · inherited_torsion_replay.txt
Hilbert 12: contracting ambient torsion
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Exact 343-point torsion dynamics and written distribution identities. Numerical diagnostics are not interval certificates or gamma algebraicity.
Next step: Complete the analytic/class-field comparison while preserving the full torsion and dual-pairing data.
Return to this work: paper, proofs, Lean, and code
Source directory · H12_Ambient_Torsion_README.md · H12_Full_Ambient_Torsion_Verification_Log.txt · H12_Contracting_Ambient_Torsion_Research_Note.md
Hilbert 12: cubic divisor development
Reading edition complete · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Finished reading set with 42 selected formal modules. Complex divisor arguments and the gamma/class-field equality exceed that formal scope.
Next step: Resolve the polarized reality, periodic descent and principal-norm obligations before claiming the original equality.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · lean/README.md · visual/README.md
Hodge: source and evidence
Reading edition complete · Lean: Source available, no current pass · Confidence basis: Recorded written review
Finished evidence reader with conditional geometric arguments. Current Lean elaboration was blocked before compilation and general Hodge remains open.
Next step: Compile the exact conditional source with pinned dependencies, then address the independent algebraic-cycle realization inputs.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · evidence/formal/FORMAL_STATUS.md
Inverse Galois: source and evidence
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Finished reader with reviewed elementary realizations and regular-projector statements. Universal realization over Q remains open and no Lean certificate is claimed.
Next step: Supply the arithmetic existence input for the specified conditional route. Keep finite examples distinct from all finite groups.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · historical/Resolution_Theory_Galois_Expanded_Journal_Package_extracted/Resolution_Theory_Galois_Expanded_Journal_Package/README.md · evidence/FINAL_STATUS.json
IUT Valuation Hulls
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Checked valuation-hull and structural witness interfaces. SourceWitnessTheorem remains open. No proof or disproof of IUT III Corollary 3.12 or ABC.
Next step: Construct the actual source witness linking the abstract interface to the intended arithmetic objects.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · formalization/lean/README.md · HANDOFF_B05.md
Lehmer: source and evidence
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Finished reader on Ramanujan tau nonvanishing with written and finite evidence. No recovered Lean certificate and no all-prime theorem.
Next step: Prove the remaining actual-prime nonvanishing obligation. Preserve the distinction between local models and the Delta representation.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · evidence/CURRENT_STATUS.md
The Possibility for a Machine Native Mathematics
Reading edition complete · Lean: No Lean claim · Confidence basis: Unassessed
The 25-page reading edition has editable Markdown and TeX, inspected monograph typesetting, and source-reconciled discussions of the current Papers X, XI, XII and selected companion studies. The original PDF is retained. Scientific confidence remains unassessed, with no Lean claim for the essay.
Next step: Independent mathematical review of the full essay and assessment of its broader research and empirical proposals remain separate work. Recovery of the original editable source remains open.
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only) · The_Possibility_for_a_Machine_Native_Mathematics_v10.pdf
Model-Theory Normalization
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
Verified scalar binary backend and finite discovery fixtures. End-to-end discovery bit-cost lowering remains open.
Next step: Prove the universal lowering/refinement bridge beyond the tested discovery fixtures.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · FORMALIZATION_COVERAGE.md · RESULTS.md
Prime-Contact Coherence Calculus
Reading edition complete · Lean: No Lean claim · Confidence basis: Recorded written review
Internally audited final manuscript with exact finite coherence calculations. The abc conjecture is not proved.
Next step: Obtain independent proof review and keep conditional/global-height claims separate from finite coherence results.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · MANIFEST.json · verification/final_pdfinfo.txt
Resolution Semantics
Active development · Lean: Selected results recorded · Confidence basis: Recorded formal evidence
The separate Lean 4.24.0 companion checks 266 theorem declarations. It retains graph reconstruction, exact unpinned/partial-pin counts, and automatic checked traversal. New finite edge indexing counts each undirected edge once. Complete duplicate-free image and actual additive quotient lists have exactly 2^(n-c) and 2^(m+c-n) elements; log2 gives their binary cardinality ranks. Equal derivative fibers and equal cosets are proved before power cancellation, with c<=n and n-c<=m. Nineteen inherited sources are unchanged, and both obstruction theorems remain axiom-free. No external module/basis interface, sparse forest/complexity theorem or wider transport/forcing claim is added.
Next step: Develop a verified sparse spanning-forest implementation and state any proved complexity bounds. If a module/basis interface is introduced, connect its dimension to the established exact cardinalities. Preserve the exhaustive rank and reconstruction references, original source and earlier companions.
Return to this work: paper, proofs, Lean, and code
Separate Lean companion replay and exact scope
Source directory · README.md · THEOREM_INDEX.md · PROOF_BOUNDARY.md
Seeded Two-Axis Calculus
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Working manuscript with 82 ledger targets, written proofs and self-review. No Lean certification or independent review.
Next step: Independently review K72-K82 and retain the unconstrained rank-two scope before adding geometric or Galois conditions.
Return to this work: paper, proofs, Lean, and code
Source directory · STATUS.md · README.md · RESEARCH_LOG.md
Signal Reconstruction
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Finished reading set. Related Paper V formal sources support packet/known-edge infrastructure, not the present unknown-edge and self-calibration theory. Recorded identification failures remain.
Next step: Formalize a selected unknown-edge or self-calibration theorem and keep failed rank/location heuristics visible in qualification tests.
Return to this work: paper, proofs, Lean, and code
Source directory · RELEASE_STATUS.json · README.md · visual/README.md
Stratified Universality
Reading edition complete · Lean: Source available, no current pass · Confidence basis: Recorded written review
Complete amended reading/source package. 75 components have mixed proved/imported/conditional/conjectural status. The reconstructed Lean core has no fresh compiler pass.
Next step: Compile the exact included core, authenticate the separate historical formal package, and preserve the mixed 75-component concordance.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · RELEASE_STATUS.json
Streaming Polyphase Factor Decomposition / SKAT
Active development · Lean: No Lean claim · Confidence basis: Written / finite evidence
Illustrated manuscript v0.8 and package marker 0.8.0, with a later v0.9 synthetic simulation continuation. Written analytic guarantees and bounded simulations. The recorded 31-test pass is historical and was not rerun during navigation cleanup.
Next step: Perform a pinned test/simulation replay, independently review the spectral-tail and simulation contracts, and harden the documented intermediate overflow calculation. External-cohort, logistic-calibration, and GPU qualification remain separate.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · README_V06.md · VERSION · FINAL_MANUSCRIPT.tex · FINAL_MANUSCRIPT.pdf · VERIFICATION_V09.md · PROOF_AND_SIMULATION_AUDIT_V09.md
Strong Artin: source and evidence
Reading edition complete · Lean: Inherited / related evidence · Confidence basis: Historical formal evidence
Finished evidence reader with retained scoped formal results. The publication records zero fresh Lean invocations and global automorphic attachment remains open.
Next step: Restore the exact runtime and replay the current source, then keep the global carrier-existence input as a separate research obligation.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · lean/README.md · lean/CURRENT_REPLAY_STATUS.json
Universal Generative Deformation Calculus
Experiment / prototype · Lean: No Lean claim · Confidence basis: Experimental evidence
Beta executable construction with 50 tests and 18 experiment checks. Closure is relative to a declared grammar, not all mathematics or historical novelty.
Next step: Validate broader grammar families and state a separate completeness theorem before extrapolating finite exploration to infinite branches.
Return to this work: paper, proofs, Lean, and code
Source directory · README.md · CHANGELOG.md · RELEASE_AUDIT.md
Large Signal Model software
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Machine Theory Compendium
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Physics: curvature states
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Physics: energy and backreaction
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Physics: origin locking
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Realization Calculus: twin edition
Needs assessment · Lean: Not assessed · Confidence basis: Unassessed
Source import identity and receipt verified. No new assessment of mathematical soundness, scientific completion, empirical validity, or Lean coverage.
Next step: Identify the exact claims and edition, inspect the written support and any reproducibility records, and assign readiness only after a bounded review (F16).
Return to this work: paper, proofs, Lean, and code
Source directory · import receipt (availability only)
Supporting and historical collections
Every entry below is Supporting / historical, with Lean: Not assessed and Confidence: Unassessed in this catalogue. Its original records may contain accepted results within a narrower scope. An import receipt identifies files and does not establish mathematical correctness. Consult the edition's own statements and run records before reusing its results.