Toledo — Equation Library of the Human–AI Readout Programme (v1.4.0): 967 coded entries incl. Economics of Expertise registrations and the Core Epistemic Structure definitions, MCP server, static API, lineage, native and imported Coq, catalogue
Abstract
What this is. Toledo is the programme's single permanent home for equations and their machine checks: a public git repository (https://github.com/morrocwi/toledo) whose tagged releases are deposited under this concept DOI. Scope is equations and Th_coqc only: registries, persistent codes ( / . .v ), parents by code back to a root, an append-only lineage log, Coq 8.20 sources whose file name is the code, an MCP server and CLI for lookup, and a static read API. Founder rules (2026-09-07): every equation is looked up here first and registered here before it is written or cited elsewhere; no AI agent in the programme may use an unregistered equation. Release v1.4.0 (counts computed from the files in the tag). 967 canonical entries (current 876, unverified 52, split 30, not_an_equation 9); 592 root rows. New in this release: (1) 16 readings registered from The Economics of Expertise in the Age of Generative AI v1.0.1 (10.5281/zenodo.22636999) — weld/H.22–29 and weld/W.03–10 — plus 7 occurrences recorded on existing codes, including a note that the paper's knowledge triple is an earlier formulation of weld/E.03.v1; (2) the Core Epistemic Structure definitions from the founder's ruling of 2026-09-07 (Blackbox Log BBL-2026-09-07-217): E_p = ⟨X_p^exp, X_p^int, M_p^AI⟩ (weld/H.30.v1), the set of AI models used (weld/H.31.v1), the unheld interactional role X_p^int = ∅ (weld/H.32.v1), the non-collapse rule Experience-Based Expertise ≠ Interactional Expertise ≠ AI Model (weld/H.33.v1, tier Dr), and the experience-holder decomposition ⟨Exp, Sel, Int⟩ (weld/H.34.v1) — the block every programme document now carries (glosa card P20). Coq status per entry: closed 161, definition 370, wrapped_related 210, mapped_not_wrapped 119, open_prop 37, not_formalisable 70. Catalogue rebuilt (A4, 286 pages); MCP package 1.4.0 (214 tests). Status and limits. K0 working release. Th_coqc / closed certifies the internal consistency of stated finite models, never empirical truth. Open debts are listed in the README's "What is not done". An AI assistant assisted under the author's direction; no AI system is an author or contributor.
