Maintain the reader website

Read side by side

On this page

The public site is at https://KomorebiP.github.io/Operation-KOMOREBI/. Its source is in this repository. The site combines maintained collection pages with documentation from two explicitly pinned library revisions.

All twelve core papers have formatted HTML reading editions. Each retains its recorded mathematical scope; companion guides and atlas coverage are described on the individual reading pages.

Sharing and discovery

tools/site_metadata.py adds a page-specific description, an absolute canonical URL, Open Graph fields and a large-image card declaration to each generated page. The home page and principal introductory routes have curated descriptions; other pages use their opening prose or a title-based fallback. Navigation, code and raw equations are excluded from automatic summaries. Metadata is present in the saved HTML, without JavaScript. Directory indexes share their trailing-slash canonical URL. Search, saved reading, the paired reader, the execution launcher and the 404 page use noindex,follow; the 404 has no canonical link.

The branded 1200-by-630 JPEG has a checksum and an accompanying SVG in website/assets/brand/sharing-card.json. To revise it, edit the SVG, rasterize the full source at exactly 1200 by 630 pixels, and update the image and source hashes in that record. A full-page browser screenshot of the standalone SVG preserves its dimensions. The image URL includes its content hash so a changed image has a new cache identity. The artwork is branding, separate from manuscript figures.

sitemap.xml lists exactly the indexable generated HTML pages and is linked in the footer. It excludes query/fragment variants and copied runtime assets. No modification dates are invented from deployment time. CI verifies all metadata, canonical targets, image bytes and dimensions, sitemap coverage and site size. Run python -B -m unittest discover -s tools -p 'test_site_metadata.py' -v.

This project is hosted below /Operation-KOMOREBI/. A project-level robots.txt does not control the host, so the build does not publish one. The sitemap can be submitted through a verified Search Console property; deployment does not claim that a search engine has indexed the pages or that a platform has refreshed its preview cache. See the Open Graph protocol, Google canonical guidance, sitemap guidance and robots.txt location rules.

Search catalogue

tools/search_catalog.py generates the compact catalogue at search-index.json. The browser loads titles, facets, and a shared term dictionary, then fetches postings for matching terms and previews for the visible results. All indexed text remains searchable, including substring and symbol-name matches. Authored math previews and result links are retained. Empty search pages load no catalogue.

The assets use revision-specific paths. Preview requests are shared and bounded in memory; failed requests can be retried. The site checker verifies the complete posting/preview signatures, target links, revision, and payload budgets. These budgets catch a return to sending all source text with the initial search. Run python -B -m unittest discover -s tools -p 'test_search_catalog.py' -v and node --test tools/test_search_engine.cjs tools/test_search_interface.cjs.

Machine-Native Reasoning reading edition

The Reviewed Mathematical Core is available at read/monographs-machine-native-reasoning/. Its start page follows the sensor example through evidence, correction, inquiry, and revision. Thirteen reading pages preserve the two opening sections, nine numbered chapters, and two source and review registers. The authored formal correspondence chapter is available in full from its original input location and the formal-scope page.

The edition retains all 27 selected statements and written proofs, 12 counterexamples, 618 mathematical expressions, six original figures, and ten source descriptions. The statement finder links to proofs and recorded formal scope. That scope connects all 174 mapped declaration endpoints to exact lines in the 79 registered production Lean files. The older map's printed page and line numbers remain linked to the original core source, separately from the refreshed reader's source lines.

tools/machine_native_reasoning_reading.py checks the retained source digest, contiguous reading ranges, printed statement identities, mathematical sequence, and source lines. tools/machine_native_reasoning_scope.py binds the accepted release record to the result map and reader publication record. Figure receipts authenticate the retained PDFs and their browser images; regenerate the latter with python -B tools/render_machine_native_reasoning_figures.py (pypdfium2). Run python -B -m unittest discover -s tools -p 'test_machine_native_reasoning*.py' -v.

The accepted 27/27 selected-core scope remains distinct from the 74-page older continuation and the separately unrecovered expanded 1,155-page monograph. This conversion adds no mathematical proof audit, Lean execution, or empirical validation. The mathematical proofreading self-review concerns presentation and navigation; there are no mathematical-token changes.

Large Signal Model reading edition

The Large Signal Model is available at read/monographs-large-signal-model/. Its Lean inspector includes all 254 mathematical modules and their root import file. Auxiliary rejection controls and test sources remain in the full retained project downloads and on GitHub. The native runner still bundles the complete retained project and its configuration; inspector selection only narrows the displayed file routes. Its start page connects a first reading path, all 100 mathematical sections in eight parts, the statement finder, recorded Lean scope, the reference laboratory, and the separately assessed PR-LASM software work page.

The 109 source-based reading pages preserve all 87 numbered propositions and their written proofs, 2,123 mathematical expressions, two original figures, and 28 references. Every proposition links to its proof and its recorded coverage row. The editable Monograph/source/FOUNDATIONS.md is the source of this HTML edition. The original 174-page publication retains its additional glossary and formal registers in PDF. The theoretical atlas also has a complete HTML guide.

tools/large_signal_reading.py translates the reviewed Markdown wrappers while preserving source lines and mathematical tokens. A pinned source digest and contiguous ranges in tools/large_signal_sections.json reject unreviewed body changes. Figure receipts bind the two browser images to their retained PDFs. Run python -B -m unittest discover -s tools -p 'test_large_signal_reading.py' -v. This conversion adds no mathematical proof audit, Lean replay, or empirical validation. Mathematical proofreading self-review covers only the presentation wrappers and navigation; there are no mathematical-token changes.

The visual guide at read/monographs-large-signal-model/atlas/ contains the orientation and all 17 plates, with 16 original diagrams and 194 selectable mathematical expressions. It adds searchable questions, three reading paths, diagram descriptions, and links to the mapped propositions, written proofs, recorded Lean scope and source modules. The main statements link back to their plates. The original 19-page atlas PDF remains available.

tools/large_signal_atlas.py binds the HTML to the retained TeX, proof map and figure receipts. tools/large_signal_atlas_sources.json pins those inputs and source ranges. Regenerate only the browser images with python -B tools/render_large_signal_atlas.py (pypdfium2 required); normal builds check the source and image hashes without rebuilding the PDFs.

Plate 3 adds a bounded, exact comparison for the atlas's fixed rational matrix. The browser uses BigInt fractions; an independent Python Fraction replay checks all 45 settings, 80 delay forecasts, and the retained 13-state trajectory with its finite delay and memory identities. The causal delay state is withheld until one observation step has elapsed. Run python -B tools/check_large_signal_explorer.py --node PATH_TO_NODE to replay the checks. The declared domain, execution inputs, limits and results are in verification/large-signal-atlas/. These finite checks illustrate the retained example; they add no universal theorem, empirical validation or Lean replay.

Run python -B -m unittest discover -s tools -p 'test_large_signal_atlas.py' -v and node --test tools/test_large_signal_atlas.cjs for source coverage, mathematics, diagram identity, proof routes, navigation and explorer edge cases.

Interactive J-Space laboratory

j-lab.html presents the saved neural-agent experiment with three choices: state edits, message tracing and persistence. It is linked from Browse → Use, interactive mathematics, site search, saved reading and the J-Space Causal Lab work page. The 4.4 MB self-contained instrument loads when requested; inference and JSON trace exports run locally. The full-tab route also works directly and provides the offline download.

tools/jspace_lab.py authenticates the retained 1.4 HTML against its source receipt and copies its bytes to assets/j-space/causal-lab.html. It does not rebuild, rewrite or run the preserved source package. The source record and published asset have independent fixed identity checks. Only that exact, authenticated HTML asset is exempt from reader-site chrome checks; the entry page gets the ordinary structure, navigation, links and labeling checks.

The experiment picker selects the instrument's existing tabs and examples. jspace-workbench.js adds the embedded presentation at runtime, using jspace-workbench.css: duplicate headers and navigation are omitted, optional controls use disclosures, and the iframe follows its content height so the page has one scroll area. Existing DOM controls and handlers are retained. The main outputs, failed references and factual audits remain available; the unadapted full lab and offline download remain direct links. Selecting the current experiment preserves edits; changing experiments or selecting Reset example reloads the instrument with a fresh example, so old measurements cannot be presented as results of the new setup. During message or persistence runs the picker and reset are disabled until the run completes or is cancelled. All inference, grading and JSON exports remain in the saved 1.4 instrument. The embedded presentation adds explanations beside target selection, edit amount, reference comparisons and recall. A sticky three-step bar moves focus and scrolls the parent page to the real controls, predictions or factual checks; it does not apply an edit or start a run. Message-branch and persistence-label keys explain the existing measured comparisons. The entry glossary distinguishes temporary working values, remembered facts, donor references and the candidate J-space. Labels remain presentation only; option values and numerical routines are retained. Mobile controls use readable text and 44-pixel touch targets. The message test's edit-settings button exposes a return path that keeps the current edit instead of choosing a fresh example. On return, a notice asks for a new measurement and identifies earlier results as recorded runs. Result captions use plain terms while retaining the underlying numeric values, failure conditions and exported trace objects. Run python -B -m unittest discover -s tools -p 'test_jspace_lab.py' -v and node --test tools/test_jspace_lab.cjs for publication and loading safeguards. This integration adds no new scientific evaluation or J-space certificate.

The site uses MathJax's tex-svg-full.js entry bundle. Its build retains all extension, output, font and accessibility modules, while omitting eight complete alternative entry bundles to keep the site within its hosting size budget. The fetched package remains complete and verified. Published runtime files keep their original bytes and SOURCE.json; assets/mathjax/PUBLISHED.json records the distribution profile and omitted bundles. tools/reader_runtime.py packages this profile; test_reader_runtime.py checks retained modules and source records.

K-COS reading edition

The complete K-COS monograph is available at read/monographs-cos-method/index.html. Its 24 reading pages retain the preface and reading guidance, four part introductions, twelve chapters, four appendices, and references. The opening guide links the full matrix-to-tail route, the supplied-spectrum route, the visual studies, and four stages of the running example. Each worked section ends with links to the adjacent calculation stages and the complete calculation route. These controls follow the same manuscript labels as the contents guide. The Start-here guide opens directly at the worked enclosure section in Chapter 9.

The reader preserves 61 numbered statements, 39 written proofs, 1,443 mathematical expressions, all 50 original production figures, all seven printed table numbers with their captions, and seven references. The three included results files appear in their authored positions, with links to the actual included source lines. The theorem finder, notation lookup, chapter navigation, and site search use the same reading structure as the other monographs. Passage lookup matches both the source file and its retained line spans, so imported results cannot shadow equal line numbers in their parent chapter.

tools/kcos_reading.py checks the source order, statement and figure inventories, mathematical expressions, and the style-file macros. tools/kcos_routes.py resolves introductory routes from manuscript labels. Run python -B -m unittest discover -s tools -p 'test_kcos_reading.py' -v. The published mathematical sources and their recorded scope remain unchanged. Appendix B retains the official finite Gram/enclosure companion; the reading guide links the separately maintained formal continuation.

The K-COS proofreading record records the complete edition review. Four labelled reading notes clarify a stale chapter reference, the precision of a numerical reference, the Python failure flag, and a shared scientific-notation scale. Their text and links are bound to exact retained source lines. The numerical-reference note also records the original CSV hash and its two full-dimensional rows. These notes do not change an authored mathematical expression or assert a new proof review.

Core visual-guide coverage

The Browse → Core visual guides directory at read/visual-guides.html links every core paper's visual material, manuscript and evidence overview. HTML status follows the maintained reading configuration; PDF destinations and hashes come from the existing source receipts. Paper I's visual atlas is inside its main monograph. The other eleven have separate visual-guide PDFs.

The current inventory checks the committed visual sources against their receipts and identifies the complete ports. Counts below describe source units, which vary by guide; they are not counts of theorems or PDF pages. The prior completed-port inventory retains the earlier source-identity snapshot. The initial inventory retains the earlier four-atlas snapshot.

Paper Retained visual source HTML visual coverage
I 22 plates Complete
II 24 plates Complete
III 24 plates Complete
IV 26 plates Complete
V 40 plates Complete
VI 42 plates Complete
VII 40 plates Complete
VIII 32 plates across two inputs Complete
IX 23 sections across two inputs, plus a generated coefficient input Complete
X 30 plates, two opening scope sections and their diagram Complete
XI 47 lessons, opening orientation and two reader-route sections Complete
XII 27 plates, including final claim and evidence records Complete

All twelve core papers now have complete HTML visual guides. Paper XI retains all 47 lessons, 23 original vector figures, three source tables, six recorded-data tables, the opening orientation and both reader-route sections. Its conversion preserves 436 mathematical expressions and 66 manuscript return links. The historical theorem number, open Conjecture 66 and same-candidate H5 comparison remain distinct. Placeholder companion aliases resolve to the actual reader PDFs.

Paper XII retains all 27 plates, 23 drawings (including two embedded directly in the page source), 335 selectable labels and 15 source tables. Its conversion preserves 752 mathematical expressions and 53 manuscript return links. The revised contract, historical original wording and evidence kinds retain their source distinctions. The unused support_rotated drawing stays in the archive.

render_paper_xi_atlas.py checks all 47 lesson titles and three opening pages in the retained 53-page PDF, then renders its original single-page vector figures. render_paper_xii_atlas.py checks all 27 titles in the retained 28-page PDF and renders the original drawing regions. These conversions do not rebuild TeX, run mathematical generators or examples, audit proofs, or replay Lean. The new atlas tests run alongside the existing source and website checks in CI.

Source-page line wrappers use compact HTML attribute syntax. The generated class names and fragment links are safe ASCII tokens; optional quotes are omitted to save six bytes per source line. Original source bytes, whitespace, accessible line labels and browser DOM values remain unchanged.

Run python -B tools/audit_core_visual_guides.py to inspect the current coverage. The report identifies the committed source revision and states that HTML configuration is read from the working tree. test_core_visual_guides.py checks the twelve destinations and distinct integrated/separate PDF routes.

Paper I's complete atlas is at read/paper-i/atlas/. Its 22 plates preserve 20 original monograph drawings, 435 selectable labels, and 699 mathematical expressions, including formulas in the plate headings. Native source theorem references resolve to manuscript passages with return links. The path, cycle, coordinate-ring and evidence plates also link their explicitly selected source sections. Three source tables and the matrix-label transcripts have semantic headers. The first source table has no printed headings; its reading-aid headings retain all three original data rows.

tools/paper_i_atlas.py records the source, macro and figure identities in documents/paper-i-atlas.json. PDF routes keep the integrated monograph's physical pages 83–104. To regenerate only those original drawing views, use python -B tools/render_paper_i_atlas.py with pypdfium2 available. Normal builds need no PDF renderer or TeX engine. Run python -B -m unittest discover -s tools -p 'test_paper_i_atlas.py' -v. This conversion adds no proof audit, mathematical example run or Lean replay.

Papers II and III each have a complete atlas at read/paper-ii/atlas/ and read/paper-iii/atlas/. Each retains 24 plates and 22 original PDF drawings. Paper II preserves 754 selectable labels, 1,043 mathematical expressions, and 40 manuscript routes; Paper III preserves 488 labels, 747 expressions, and 44 routes. Each manuscript destination has a return link. Four source tables and the gridded matrix-label transcripts retain semantic headers. Both PDFs have two front-matter pages, so V1–V24 open physical pages 3–26.

tools/worked_visual_atlas.py implements these two source-bound conversions; tools/core_worked_atlases.py declares the source table schemas. Figure sources, PDF hashes, physical pages and crop bounds are recorded in tools/worked_atlas_sources.py and the per-paper figure receipts. Render the unchanged drawings with python -B tools/render_worked_atlases.py; ordinary website builds use the committed images and need no PDF renderer or TeX engine. Paper II's multiline drawing label retains both formulas, and V24 includes its separate current-scope source verbatim with a source link. Its recorded counts are inherited evidence statements, not a new replay. The verifier reconstructs the numbered manuscript destinations from the published source chapters and rejects reachable-but-wrong destinations. Run python -B -m unittest discover -s tools -p 'test_core_worked_atlases.py' -v. The mathematical proofreading self-review covers the new presentation wrappers, labels, descriptions, source references and tables. No mathematical tokens or imported manuscript bytes are changed; no new proof audit, exact example run or Lean replay is claimed.

Paper VIII's complete standalone guide is at read/paper-viii/atlas/: 32 plates, 30 original PDF drawings, 711 selectable drawing labels, 830 mathematical expressions, three source tables, and 84 manuscript routes with return links. Both standalone source inputs retain their own source-line links. Four literal TikZ loops in the extension drawings are expanded with their original node lines and explicit bindings; unreviewed values or loops stop conversion.

Paper VIII's PDF identity is resolved by a new crosswalk revision at publication/paper-viii-visual-crosswalk/VISUAL_TO_TRADITIONAL_CROSSWALK_v2.json. It binds the retained PDF checksum a78f1c18c7c36cecbaf9484bc6dc643300c3b5054df338f48be6390af5e520c7. All 32 original plate records and manuscript bindings are preserved. All titles, printed locators and page labels were rechecked against physical pages 3–34. The HTML converter also checks stable labels, statement numbers, kinds and titles. The declared fact:cg translation remains: the guide's “Classical input 7.5” is the manuscript's “Standard fact 7.5”. The inherited crosswalk remains unchanged as history. The current conversion reports a matching PDF checksum.

Paper IV uses the explicitly labeled reconstructed visual source at publication/paper-iv-visual-reconstruction/pages.tex. Its complete source package builds a 28-page PDF: all 27 content pages match the selected 16 October PDF after Unicode NFKC and whitespace normalization, while the cover identifies the reconstruction. All pages have a recorded visual review. The online V12 and V26 now include the selected later PDF's branch clarification and evidence table. The atlas exposes the rebuilt PDF and a complete editable-source download. The GitHub maintenance note records the source reconciliation and F04 closeout. Routine repair notes stay in docs/history/ on GitHub; the public reader presents the updated guide in place.

tools/visual_guide_provenance.py validates the new source and crosswalk identities without changing either frozen import. Run it with --pdf to repeat the full PDF text and page checks with pypdfium2.

tools/paper_viii_atlas.py uses the shared worked-atlas renderer and emits documents/paper-viii-atlas.json. tools/paper_viii_atlas_sources.py records the two source inputs, exact crosswalk identity, current PDF and reviewed crop bounds. python -B tools/render_paper_viii_atlas.py rechecks all PDF pages and regenerates the drawing views with pypdfium2; normal website builds need no PDF renderer. For V15, the recipe renders its 48 original resized drawing objects alone to exclude adjacent page prose from the crop. The PDF file and drawing objects are unchanged; no PDF is saved and no TeX is rebuilt. Run python -B -m unittest discover -s tools -p 'test_paper_viii_atlas.py' -v. The mathematical proofreading self-review covers the presentation wrappers, labels, descriptions, references and tables. Mathematical tokens are preserved; this conversion adds no proof audit, mathematical example run or Lean replay.

The Komorebi Methodology also has a complete HTML edition at read/komorebi-methodology/: preface, nine essay chapters, closing reflection, verification notes, and references. Its 12 text pages preserve 164 mathematical expressions, three numbered equations, nine references, and the three original diagrams. The proofreading and conversion record states the review scope and validation. The source package and PDF are unchanged. tools/methodology_sections.json binds the exact source ranges and identities; tools/methodology_reading.py translates only the reviewed print wrappers. Run python -B -m unittest discover -s tools -p 'test_methodology_reading.py' -v to check the complete edition, source drift, numbering, equations, figures, and chapter/citation links. This conversion adds no proof audit or Lean coverage.

Komorebi Space and Realization Boundaries also have complete HTML editions at read/komorebi-space/ and read/realization-boundaries/. Their 52 source sections retain 137 proof blocks, 46 original figures and 4,828 mathematical expressions. tools/foundational_reading.py translates declared print wrappers; tools/foundational_sections.json fixes the source ranges, input order, source identities and accessible table headers. A changed source requires a reviewed selection. Equation and theorem numbers follow each book's printed counters. The statement finder links adjacent written proofs without adding formal claims.

Figure receipts in website/assets/figures/komorebi-space/ and website/assets/figures/realization-boundaries/ identify the retained source and browser image. Space's TikZ diagrams are rendered from the retained book PDF; the receipt records the PDF identity, page and crop. Standalone plots and Boundaries diagrams use their retained figure assets. Captions remain selectable HTML. This presentation adds no mathematical review or Lean execution. tools/render_foundational_figures.py reproduces the images from those receipts with pypdfium2; it is separate from the normal website build.

Run python -B -m unittest discover -s tools -p 'test_foundational_reading.py' -v to check both complete editions, source changes, formula preservation and HTML structure. The normal site checker also checks their navigation and source links.

Quantum and Circuits has a complete HTML reading edition at read/monographs-quantum-and-circuits/: chapters 1–21, appendices A–F and back matter in 206 topic pages, with 233 numbered statements, 120 written proofs, 82 original scientific figures in 85 manuscript appearances, 61 accessible tables, and 4,200 mathematical expressions. The contents page groups the main chapters, appendices, glossary and sources, with a preface and volume guide retaining the part introductions and general glossary. tools/quantum_reading.py translates the retained print wrappers; tools/quantum_sections.json binds complete source ranges, original identities, chapter groups and table headers. Authored QA labels and source-line links stay intact. tools/quantum_symmetry.py retains the symmetry treatment's chapter-wide statement, equation and figure numbering, its scope panels, and all twelve open questions. The 21 numbered equations remain part of the complete mathematical sequence; identical longtable continuation headers appear once in HTML. tools/quantum_catalytic.py adds the complete catalytic treatment: 28 topic pages, 134 numbered statements, 51 proofs, 32 figures in 34 appearances, 15 tables, six literal listings, and 1,906 mathematical expressions. The six numbered gates in the linear atom appear as separate displays, retaining their original equation numbers and source lines. The eight explicitly named proofs have links from their earlier statements and return links across chapter pages. tools/quantum_circuits.py adds chapters 13–20 in 23 topics and the complete 25-topic circuit visual study: 30 numbered results with written proofs, 12 original figures, ten tables, two literal reproduction listings, and 775 mathematical expressions. It preserves C01–C08 claim labels, five named scope panels, and six printed equation numbers. The binary-field main treatment and general-field visual scope retain their separate macro contexts. The Appendix E.4 citation now opens the HTML evidence ledger. All 54 collected references retain their original numbering. tools/quantum_companions.py completes the reading edition with 58 pages: the volume orientation, appendices A–F, glossary and source notes. The new pages add 314 mathematical expressions, 30 accessible tables, and 157 literal code extracts. All 115 circuit declaration types retain their full Unicode text, source locators, block labels and axiom sets. The arithmetic guide keeps its 96-theorem inventory and its distinct inherited checkpoints. Visible scope notes distinguish retained verification statements from this HTML conversion. The 30-entry circuit result index keeps its printed page column, linking the original PDF at the corresponding physical page; its source digest and page map are in tools/quantum_sections.json. Recheck the PDF map with python -B tools/check_quantum_pdf_pages.py (using the same PDFium dependency as the figure helpers). The volume guide routes all 21 chapters and six appendices to their first HTML topics. Literal code bodies are protected before any print-wrapper translation, and source lines remain unchanged. The complete sequence has 207 pages including references. The former #source-continuations bookmark remains an alias for the complete contents. The shared statement finder links all written proofs without adding Lean correspondences. This presentation adds no mathematical review or Lean replay.

The arithmetic figure receipts and browser images are in website/assets/figures/quantum-arithmetic/; symmetry figures and receipts are in website/assets/figures/quantum-symmetry/; catalytic figures are in website/assets/figures/quantum-catalytic/; circuit figures are in website/assets/figures/quantum-circuits/. Reproduce them from the original single-page PDFs with python -B tools/render_quantum_figures.py and python -B tools/render_symmetry_figures.py, plus python -B tools/render_catalytic_figures.py and python -B tools/render_circuit_figures.py. Normal site builds check their source identities and publish the retained PNGs. Figure receipts default to one use; the symmetry compiler diagram and catalytic Pareto and packet diagrams explicitly record their two appearances. Run python -B -m unittest discover -s tools -p 'test_quantum_reading.py' -v for the complete edition, formula sequence, proof routes, tables and source anchors.

Reading editions keep one complete, native chapter menu in the top navigation. Quantum and Circuits also provides read/monographs-quantum-and-circuits/start.html: three editorial reading paths with prerequisites, chapter links, and checkpoints. The visual tour, four-treatment study route, and formal companion link into the retained edition. Its contents, reading-library card, work overview, and search entry expose the guide without changing the chapter sequence.

The filterable directory at read/start.html offers reading paths for substantial works with both a complete HTML manuscript and an HTML visual guide. The current selection is Papers I–XII, Quantum and Circuits, Large Signal Model, and K-COS: 15 works and 45 paths. PDF-only works, partial HTML selections, software, experiments, and books without an HTML visual companion keep their existing reading routes.

Each guide connects a visual introduction, a full reading sequence, and supporting evidence. The core papers reuse their work-specific questions, examples, setup passages, statements, and written-proof links. K-COS includes its worked enclosure, formal correspondence, and reproduction chapters. Quantum and Circuits and Large Signal Model retain their curated guides. The reading library, contents, work toolbars, catalogue, and search expose the selected guides.

tools/reading_paths.py selects eligible editions from the reading configuration. documents/reading-paths.json records the selection, paths, and destinations. The final site check requires exactly the eligible works, three path anchors per guide, and valid destinations and entry links. Run python -B -m unittest discover -s tools -p 'test_reading_paths.py' -v for selection, source ownership, missing-resource, scope, curated-guide, and navigation checks.

Footers keep previous/next links and a direct Full contents link, avoiding the quadratic storage cost of repeating a second full menu on every topic page. Atlas-specific menus retain their existing behavior. The site-size guard continues to enforce the 1 GiB GitHub Pages ceiling.

The twelve core editions share collection switching, chapter filtering, persistent text size and font choices, and sidebar chapter shortcuts. The control renderer runs after chapter layout and preserves manuscript text and mathematics. Reading tools enhance native links and disclosures; full chapter lists and paper switching remain usable without JavaScript. Text preferences tolerate unavailable or invalid browser storage. Keep these controls in the shared renderer rather than adding separate versions to individual papers. Run python -B -m unittest discover -s tools -p 'test_reader_usability.py' -v along with the reading-navigation and source-preservation checks when changing them.

Inline formulas retain their source and full rendering scale while scrolling within the available text width on narrow screens and with enlarged text. The shared reader adds a named keyboard scroll stop only when a formula overflows, and rechecks after typesetting, resizing, text preferences and live search results. Existing accessible names and author-supplied focus settings are retained. CSS provides touch scrolling without JavaScript; print layout removes the scrolling treatment. Run node tools/test_math_overflow.cjs for the adaptive keyboard behavior and check a real rendered chapter at narrow phone widths with extra-large text.

Direct passage links and in-page navigation correct their scroll position once MathJax and web fonts have finished loading. This correction retains the target and existing browser history. Pointer, touch, wheel and keyboard input cancel the pending correction, as do a newer destination, changed focus or a removed passage. Readers who have already interacted before page load keep their place. Run node tools/test_reader_navigation.cjs for delayed layout, cancellation, safe hashes, disclosure opening and browser-history behavior.

Citation and figure navigation adds native links to the existing figure assets and return links from bibliography entries to their citing HTML passages. Return routes are derived from the rendered canonical chapters after each book is built. They retain the nearest source passage anchor and deduplicate repeated citations within one passage. The site verifier recomputes those routes and checks their placement and targets. Run test_reading_links.py when changing this code. Bibliography search enhances the original entries in the browser; direct links and Back/Forward reveal an entry that a search has hidden. Print styles restore the complete bibliography.

All core chapter statement indexes are rendered from the existing statement nodes and proof routes. Statement matching supports printed numbers, types, source labels and Greek names. Keep proof-link filtering tied to actual rendered links. The statement-index verifier checks complete coverage, source labels, order and agreement with the proof links in each passage. Run test_statement_navigation.py and node --test tools/test_statement_search.cjs when changing these controls.

Each core paper also has read/<paper>/statements.html, linked as Find statements from its shared reading controls. The directory uses the same statement-entry renderer and recorded proof routes, grouped in chapter order. Search hides empty chapter groups; the native full list remains usable without JavaScript, and print styles restore all groups. Switching papers from a finder opens the other paper's finder. The verifier checks every directory entry, chapter context, title and destination against the canonical chapter indexes. Finder filters use q and proof=1 query parameters, updated with replaceState. Page restoration and Back/Forward apply the URL filters after native form-state restoration. Preserve unrelated query parameters and anchors when updating them.

Reference previews audit marked reference and citation links after the canonical chapters and bibliography are rendered. Each paper's lazy-loaded JSON contains inert text/element trees from those destinations. Equation labels are retained as metadata before their print-only TeX commands are removed, so formulas sharing a passage can be selected exactly. Excerpts end at whole blocks and formulas; section excerpts and omitted content are identified in the dialog. The site verifier regenerates every entry and checks it against the published JSON. Do not substitute generated summaries. The browser creates an allowlisted DOM, keeps original hyperlinks, respects text preferences, and guards against stale loads and wrong-paper data. Run test_reference_previews.py and node tools/test_reference_previews.cjs when changing this behavior, then check keyboard, phone, math and passage navigation in real rendered chapters. For same-document Back navigation, previews mark the restored control with data-reading-history-focus containing the current URL. The generic hash handler consumes that marker once, preserving the explicit focus return while continuing to handle ordinary or unrelated fragment navigation.

Inspect Lean

Inspect Lean opens a source directory for the works that already have HTML reading editions and selected Lean resources. It is linked from their reading controls, work overviews, claim routes and the Browse menu. File filtering matches paths and lexical declaration names; q in the address retains the filter. The complete native file list works without JavaScript.

The inspector groups core papers and books separately. File lists show the filename and module folder, with their shared source root under Source locations and editions. Full retained paths remain searchable. Source pages use filename headings and a compact row of reading, download and comparison actions. Coverage labels stay visible; their descriptions and evidence routes use a native disclosure. The original source bytes and line anchors are retained.

Lean source views color comments, strings, keywords, tactics, and numbers while retaining the original text and line anchors. On wide screens a declaration outline stays beside the code; phones and comparison panes use a native disclosure. Its optional name/kind filter changes the outline only. The source verifier extracts rendered code text and compares every line with the original download, independently of its token spans. Colors and declaration names are navigation aids, not a Lean compiler result.

Source rows use their existing L<number> IDs inside the source container for styling, line controls and saved reading positions. Repeated per-line classes are omitted, and Lean token classes are compact. Accessible line labels, source text, direct links and original downloads are unchanged. This reduces the generated site's storage without removing reading or proof material.

The inspector expands only receipt-owned .lean files within the existing Lean resource selections. It excludes package caches, build directories and lakefile.lean. Original source readers retain exact downloads, linked line numbers, existing claim correspondence and SHA-256 provenance. Declaration locations ignore nested comments and strings, and provide navigation only; anonymous, generated or unusually formatted declarations may be omitted. Coverage labels and evidence links retain the current recorded assessment. The viewer does not execute Lean or add claim mappings.

Implementation lives in tools/lean_reader.py and lean-reader.js/.css. The website workflow runs test_lean_reader.py and test_lean_reader.cjs; the full site verifier checks published source identities and declaration locations against lean/index.json.

Sources

Content Source
Work titles and source ownership Source index and import receipts
Completion, Lean coverage, confidence and limits Project status
Selected reading, proof, Lean and code files Browse resources
Introductory terminology and background advice Reader experience
Core-paper questions, scope and first reading paths Paper introductions and guidance renderer
Hand-worked calculations and exercises Example index, tutorial pages and exact arithmetic checker
Statement locations for all 12 core papers and retained Paper I declaration mappings Claim navigation, bound to the retained source records
Library source revisions Website library revisions
Page structure and browser behavior Website assets and site builder
Local PDF and source reading pages Document publisher and receipt-bound source files
Embedded PDF reader Pinned PDF.js fetch and verification

Reading routes, glossary, download guides and work introductions are generated with the collection's normal status command. Edit their source records or templates. Keep each claim's exact recorded scope when changing navigation.

The glossary’s maintained records in manifests/reader-experience.json include alternate names and abbreviations, short excerpts from the worked examples, a first reading route, and comparisons of nearby concepts. Edit those records and regenerate docs/GLOSSARY.md with tools/reader_experience.py through the normal status command. The GitHub reference and website lookup share the same definitions, examples and original term anchors. Both glossary lookup and collection search include the alternate names and short examples. Exact term names rank first in glossary lookup, followed by exact alternate names, name prefixes and definition matches. Subject filters also apply to alternate names. Without JavaScript, the first reading route, comparisons, subject lists, letter groups and complete entries remain available.

The homepage keeps its five research previews in one manually selected panel, with named topic tabs, previous/next buttons, touch swipes, and standard tab-list keyboard controls (Left/Right, Home/End). It never advances automatically. All five sections and their reading links remain visible without JavaScript. The four reading routes and a short tools row stay outside the slides. Homepage content lives in tools/home_page.py; its styles and behavior load only on the homepage from website/assets/home.css and home-slides.js.

The collection keeps title search and discipline selection visible. Completion, Lean coverage, evidence, publication type and page size live under Advanced filters. Shared filter URLs reopen that panel when an advanced selection is active. Work overviews use one reading toolbar, with specialist links under More resources; existing section and return anchors remain available.

HTML chapters use compact previous/next controls and a section contents panel. On wide screens the panel stays beside the text and marks the current section. In narrow windows, including comparison panes, it becomes a sticky Contents disclosure that closes after a section is selected. Contents and resource links remain native disclosures without JavaScript. These controls rearrange the reading interface without changing the manuscript article or its passage IDs.

The section panel keeps Work overview and Full contents links available while reading a chapter, so a link into a definition still has a visible route back to the introduction. They share one compact row with Previous and Next; the core-paper enhancements reuse this row. On narrow screens, anchor spacing follows the actual height of these controls, including wrapped text. The links work without scripting; the site checker verifies that they return to the matching work and reading index.

The twelve core-paper overviews introduce the central question, contribution, assumptions and limits, followed by an example → setup/definition → result → proof route. Edit the paper-introduction manifest for that editorial copy. Each example must already belong to the paper's learning topics. Setup lines are checked against receipt-bound source text; result and proof links use the existing claim index. Where an HTML chapter is available the links open that passage, otherwise they use the on-site source reader.

Notation help opens a chapter-local search dialog and downloads only the current work's compact index when opened. It reuses the notation search's case-sensitive symbol ranking and source contexts. A notation-table result keeps the whole row's subject and meaning together; an occurrence inside a definition is shown as a passage, rather than treated as a definition of every symbol it contains. Closing the dialog returns keyboard focus to its control. Without scripting or dialog support, the ordinary notation-index link remains.

The learning_topics records in the reader experience manifest generate the topic map, the source routes at the end of each tutorial, and return links on the related work pages. Edit tutorial explanations above the learning-navigation marker. The status command replaces the section below that marker. A subject route does not establish a theorem correspondence.

Current formal-source additions

manifests/reader-source-additions.json explicitly selects later committed sources from dated publication inventories. The reader, resource validator, reading ZIPs, and native runner share tools/reader_source_additions.py. It verifies the pinned inventory hash and every selected file, rejects conflicts with original import records, and leaves those records intact. The runner also checks each input against its committed Git blob.

The Special Functions selection includes the seventeen coupled production modules, their audit files, selected controls, declaration registers, and Block17 evidence. The inspector links its current source guide and labels the old Block01 status as historical. Realization Boundaries selects its root and all 66 production modules, with coverage and replay guides. Source pages link exact selected local imports. The execution guide refers to generated catalogue counts instead of repeating a fixed total. These publishing changes perform no Lean replay or proof review.

Saved reading

Browse → Saved reading opens a personal list of pages and passages stored in this browser. Reading pages offer Save page, and section headings have a bookmark control that retains the exact fragment. The list supports title, paper and section search, individual removal, and updates across open tabs. It records explicit saves only. Storage failures leave save controls unchanged and explain how to use browser bookmarks instead. Without JavaScript, the ordinary reading links and browser bookmarks remain available.

The page and controls are built by tools/reading_list.py; browser behavior and styles live in website/assets/reading-list.js and reading-list.css. URL and storage guards keep saved links inside this site's reading pages. The site workflow runs the rendering and browser-state regressions alongside reader tests.

Paper V HTML reading edition

Paper V has 40 reading pages plus contents and bibliography. Its contiguous source ranges retain both manuscript branches, four appendices, 1,219 mathematical expressions, 83 proof bodies, 35 manuscript figures and ten tables. Chapter navigation uses the shared reading controls. All forty visual-atlas plates also have HTML pages at read/paper-v/atlas/, retaining 37 drawings, 550 selectable TikZ labels, 962 mathematical expressions, six semantic tables, original source-line links and 73 manuscript links with return routes. The reused Gibbs plot has a separate text description; its labels remain in the original image and PDF. Historical computation totals retain their source-edition scope and do not describe a new execution during conversion.

tools/paper_v_atlas.py checks plate numbering, source and image identities, the complete equation sequence and both directions of manuscript links. documents/paper-v-atlas.json records those checks. Regenerate the reviewed PDF crops with python -B tools/render_paper_v_atlas.py (pypdfium2 required). Normal builds verify committed images without a PDF renderer or TeX compiler. Run python -B -m unittest discover -s tools -p 'test_paper_v_atlas.py' -v.

The chapter configuration records the original line ranges and E-prefixed numbering. The figure publisher checks the retained PDF sources and their rendered PNG hashes. Normal builds verify those images; the figure renderer is needed only to regenerate them. Run python -B -m unittest discover -s tools -p 'test_paper_v_reading.py' to check the complete equation sequence, statement/proof routes, numbering, tables and figure identities. The wavelet walkthrough and Haar lab link directly to the related HTML chapters. Historical formal and experimental scope remains attached to the edition; this conversion adds no proof review or Lean replay.

Paper VI worked visual atlas

All 42 Paper VI atlas plates have HTML pages. The conversion retains 40 original drawings, 588 selectable drawing labels and 931 expressions, with 76 manuscript passage links and return links. The two evidence-guide plates retain their original wording and link to the work's evidence record. Existing plate URLs and index anchors remain available; the five previously published drawing images are unchanged.

The atlas renderer verifies source correspondence, figure identities, table cells and both directions of the manuscript links. The shared transcript parser also serves Paper VII without changing its retained mathematics. Conversion records are published in documents/paper-vi-atlas.json. To regenerate only the frozen-PDF crops, run python tools/render_paper_vi_atlas.py --pdftoppm PATH. The website build checks the assets and requires no TeX compiler. This conversion adds no mathematical example execution, proof audit or Lean replay.

Paper VIII HTML reading edition

Paper VIII has 23 reading pages, contents and a bibliography: the opening orientation, three exact models, 15 manuscript sections and Appendices A–F. The conversion retains 1,192 mathematical expressions, 56 proof bodies, 25 figures and 12 tables. Numbering is checked against the retained compiled labels. The worked visual atlas remains in the original PDF.

The chapter configuration fixes source ranges, appendix transitions and table reading aids. Tables with grouped columns retain their column groups; tables printed in parallel retain both row-header columns. The shared figure publisher checks the original PDF and rendered PNG digests. Use the figure renderer with --pdftoppm only when regenerating those assets. Normal builds need no PDF renderer.

Run python -B -m unittest discover -s tools -p 'test_paper_viii_reading.py' to check complete source coverage, equation order, printed numbering, statement/proof routes, figure identity, tables and internal links. The website workflow runs these checks before publication. This reading conversion adds no proof assessment, Lean replay or new hardware measurement.

Paper IX HTML reading edition

Paper IX has 56 reading pages and a bibliography. The route covers all 13 main sections, the edition summary and all five mathematical appendices. It retains 5,252 mathematical expressions, 153 proof environments, 14 manuscript figures, 33 tables and all 27 bibliography entries. Historical headings and checkpoint notices keep their source scope.

The complete visual guide has 23 HTML sections, 20 original figures, 278 mathematical expressions, six source tables and 35 manuscript routes with return links. The entrypoint sources/visual.tex includes both visual_body.tex and worked_atlas.tex; the latter includes the generated Newton coefficients. The older retained visual_README.md still describes 15 sections and 12 figures. The audit follows the actual input graph and checks the retained 25-page PDF instead of using that stale inventory. All imported source bytes remain unchanged.

tools/paper_ix_atlas.py preserves source wording, captions, mathematical sequences and line anchors. Figure math labels are read from the retained generator's Python AST without executing it. Other native figure labels are selectable PDF text, with descriptions and semantic data tables for reading order. Tables project the retained exact records, including every residue in the four displayed periods. The 5,490 illustration assertions and 463 worked example checks are inherited records, not executions performed by this port. Manuscript targets are reconstructed using the manuscript reader's own normalization and printed-label map. documents/paper-ix-atlas.json records these bindings and the stale README count.

Run python -B tools/render_paper_ix_atlas.py with pypdfium2 to check all 23 PDF section titles and render the 20 retained vector figures. Normal builds use frozen images and extraction receipts without PDF or TeX dependencies. Run python -B -m unittest discover -s tools -p 'test_paper_ix_atlas.py' -v for source coverage, formula preservation, transcripts, data tables and two-way manuscript links. The mathematical proofreading self-review covers the presentation, captions and labels; this port adds no mathematical proof audit, new example execution or Lean replay.

The chapter map fixes the reading ranges; the conversion module checks the complete input graph and preserves original line anchors through Pandoc and print wrappers. The table aids bind reviewed headers and captions to the retained source. Tables inside proofs remain inside their proof blocks. The bibliography has a separate source-bound mathematical conversion record.

Run python -B -m unittest discover -s tools -p 'test_paper_ix_reading.py' to check input coverage, printed numbering, equation order, tables, figures, bibliography and reading links. No proof assessment or Lean replay is added.

Paper X HTML reading edition

The complete Paper X visual guide has 30 numbered HTML plates and retains both opening scope sections on its contents page. Its 29 drawings include the opening diagram that distinguishes the transported target family from the independently recovered carrier summand. The guide retains 754 selectable labels, 969 mathematical expressions, two source tables and 50 manuscript routes with return links.

The audit follows visual_appendix/appendix.tex, including its opening contract and source/pages.tex. Physical PDF pages 2–3 hold the opening scopes; V1–V30 are pages 4–33. The historical 17/20, checked conditional 20/20 and later unpromoted 19/20 records retain their different input contracts. Conversion checks reconstruct all authored prose and table cells as well as the equations, so changes to conditional scope wording fail verification.

tools/paper_x_atlas.py uses the shared worked-atlas renderer and emits documents/paper-x-atlas.json. The source and crop bindings are in tools/paper_x_atlas_sources.json. Three crops touch adjacent page prose: V11, V19 and V22 render only the original drawing objects at scale 1.18541, with independently checked counts of 104, 83 and 135 objects. No PDF is saved or rebuilt. python -B tools/render_paper_x_atlas.py checks all 32 source section titles and regenerates the 29 drawing views with pypdfium2. Run python -B -m unittest discover -s tools -p 'test_paper_x_atlas.py' -v. Descriptions were checked against the rendered figures. This presentation conversion adds no proof audit, mathematical example execution or Lean replay.

Generated metadata JSON uses compact syntax to keep the reader within the 1 GiB publication limit. Parsing preserves every data value and all whitespace inside source strings. Receipt-bound files under documents/files/ and frozen asset receipts retain their exact bytes. The site-size guard remains active.

Generated browser Lean layer and workspace manifests use the same compact JSON syntax. Their source record is computed after serialization, so its sizes and hashes bind the compact files. The copied upstream core manifest, compiler, binary packs, import selections, and source strings are unchanged.

Per-work notation downloads may use version 2 to store repeated surrounding source text once in a contexts array. Each passage's context then identifies the corresponding array entry. The serialization is used only when it is smaller; version 1 remains valid for other files. The notation decoder restores the complete logical data before source verification, including all whitespace and TeX in the context strings. HTML excerpts, source occurrences, global notation search, and chapter notation search retain their existing data and behavior. This storage change keeps both K-COS and Machine Native Reasoning within the publication budget without removing reading material or weakening the size check.

Paper X has 30 reading pages and a bibliography. It covers all 15 main sections, the algorithms and reproducibility appendices, the dated Block 27 discussion, the residue-counting continuation and the final conditional completion. The conversion retains 1,080 mathematical expressions, all 16 main proof bodies, 16 original figures, three tables and all 23 bibliography entries. The complete visual guide is linked above; its retained PDF also remains available.

The chapter map fixes contiguous source ranges. The conversion module checks every authored input, preserves source-line anchors and expands the continuation's literal notation macros. Headings within proofs remain inside their proof blocks. Equation references retain the published numbering. The bibliography has its own source-bound equation and reference record.

Run python -B -m unittest discover -s tools -p 'test_paper_x_reading.py' to check coverage, numbering, statement/proof routes, figures, tables, bibliography and mathematical order. Historical totals and the independent outputs of the conditional endpoint retain their source qualifications. This conversion adds no proof assessment or Lean execution.

Paper XI HTML reading edition

Paper XI has 38 reading pages and a bibliography. All 19 main sections, 68 main proof environments and fifteen construction appendices are retained. The conversion preserves 1,030 typeset mathematical expressions, 275 literal derivation blocks, 16 original figures, five semantic tables and all 29 bibliography entries. The visual, Lean and research companions remain available as PDFs.

The chapter map fixes contiguous ranges and authored input order. The converter preserves literal derivations, source-line anchors, published numbering and Conjecture 66's open status. Internal companion route keys resolve through the retained reading concordance to actual PDF pages. The bibliography follows the published order and citation numbers, checked against the compiled labels.

The figure renderer produces browser PNGs from receipt-bound single-page PDFs. The shared publisher verifies the original PDF and rendered PNG hashes; normal builds need no PDF renderer.

Run python -B -m unittest discover -s tools -p 'test_paper_xi_reading.py' to check input coverage, numbering, literal and mathematical order, figures, tables, companion routes and bibliography. The HTML conversion adds no proof assessment, arithmetic realization result or Lean execution.

Paper XII HTML reading edition

Paper XII has 16 reading pages and a bibliography, covering all 13 main sections, the reading map and the full verification/revision record. The conversion retains 873 mathematical expressions, 52 proof bodies, all 82 statement environments, 18 original figures, two semantic tables and all 27 bibliography entries. The visual and Lean/evidence companions remain available as PDFs.

The chapter map fixes contiguous source ranges. The converter checks authored inputs, equation order and source anchors. Companion route keys resolve through the retained reading concordance to actual PDF pages. The ring-isomorphism heading keeps its mathematics in the text and uses its plain PDF label in navigation.

The figure renderer produces browser PNGs from receipt-bound single-page PDFs. Normal builds verify the original PDF and PNG hashes without requiring a renderer.

Run python -B -m unittest discover -s tools -p 'test_paper_xii_reading.py' to check source coverage, numbering, mathematical order, proof links, figures, tables, companion routes and bibliography. The conditional arithmetic inputs and separate original/revised claim records retain their source scope. This conversion adds no proof assessment or Lean execution.

Special Functions hub and coupled-function lab

The Special Functions hub connects the current HTML monograph, its five subject families, the five selected reading PDFs, and the coupled recurrence's formal report and claim map. Its chapter links follow the source-bound HTML edition. The preserved scientific figure retains its caption, alternative text and intrinsic dimensions in the shared Markdown renderer.

The special-functions-coupled playground preset uses exact rational coefficients, exports both coefficient lists as CSV, and distinguishes its local series-tail envelope from floating-point plot evaluation. Run python -B -m unittest discover -s tools -p 'test_special_function_python.py' for its independent polynomial, closed-form, export and input controls. The reader tests also check the hub's chapter and selected-source links. This integration adds no formal replay or mathematical completion claim.

Extended factorial-lanes example

The factorial-lanes derivation has an independent exact program in examples/factorial_lanes.py. The factorial publisher provides a checked on-site source reader and source-bound downloads. Its finite output snapshots live in verification/factorial-lanes/. The site checker validates their byte identities, while the workflow re-runs the arithmetic and compares freshly emitted tables against the committed copies.

Extended wavelet and polyphase transfer example

The wavelet-polyphase walkthrough extends the existing four-level Haar lab with exact lifting, weighted detail selection, a circular FIR filter, a complete four-level operator conjugacy, sharp finite stability, operation-order counterexample and boundary correction. The exact program uses rational arithmetic for its mathematical checks. Six CSV tables, a JSON certificate, and two Python-generated SVG figures are stored under verification/wavelet-polyphase/. The publication bridge verifies source-bound downloads and archives without running the program at build time. GitHub Actions separately checks the program, exact output identity and site links.

Extended Stirling, Bell and Fubini example

The partition-transform derivation starts with exact Stirling numbers of the second kind, gives Bell and factorial-weighted Fubini numbers and reverses the triangular transform using signed Stirling numbers of the first kind. It then derives Touchard polynomial evaluation, scaled exponential moments and the Fubini reciprocal EGF, a general reversible Stirling substitution, coupled residue transfers and a precise boundary between recoverable polynomial data and noninjective row summaries. The standard-library checker independently enumerates small partitions, verifies surjection counts, triangular inverse matrices and formal series coefficients, and generates seven CSV tables, a Python SVG figure and JSON checks. The publication bridge rebuilds every record from the retained program, binds the source identities and checksums, and publishes a reproducible reader and download archive.

Extended roots-of-unity and falling-factorial example

The roots-of-unity / Newton walkthrough takes the ordinary power x^5 through a primitive-cubic-residue projector, the Stirling/Newton coordinate isomorphism, finite-difference transfer, refinement and an induced multiplication law. It distinguishes transported projectors from raw ordinary-degree filters using a concrete failed control. The standalone exact checker uses standard-library rational arithmetic, an exact cyclic permutation trace for root-of-unity orthogonality, direct enumeration of function images, rational spectral polynomials in the backward-difference number operator, filtered formal generating functions, general cross-packet translation blocks, and independent matrix coefficients. The degree-operator spectral formula's characteristic-three failure is an explicit control rather than a theorem inferred beyond its rational coefficient scope. The publication bridge regenerates eleven CSV tables, three accessible Python SVGs, JSON checks, and a deterministic source-and-results archive. Tests include reproducible bytes and deliberately corrupted downloads.

The quantum phase and measurement derivation adds exact Gaussian-rational matrix calculations, three-setting tomography, partial dephasing, coherent records, and packet refinement. Its standalone program generates two CSV tables, a labelled SVG, and a JSON case summary. The publication bridge binds the source, walkthrough, and records to their SHA-256 identities in a deterministic ZIP. Pages CI checks the arithmetic, expected output, reproducible bytes, and corruption detection. The physics-dephasing playground preset exports editable exact data. These finite teaching checks do not replay Lean. The collection extension adds amplitude damping, a rational modulus-12 Ramanujan projector and phase family, and three-qubit bit-flip recovery. Three additional CSVs and the physics-arithmetic-phase preset expose the exact data. The expanded program checks 1,917 finite cases, including the difference between syndrome measurement and full address measurement.

Build locally

Use a complete collection checkout and separate checkouts of the two libraries at the revisions in manifests/reader-site-libraries.json. Python 3.13 is used by the website workflow. Choose fresh output directories for each build.

python -m pip install -r website/requirements.txt
python -B tools/claim_navigation.py --check
python -B tools/update_completion_status.py --check
python -B tools/fetch_reader_runtime.py --output ../reader-runtime
python -B tools/fetch_pdf_runtime.py --output ../pdf-reader-runtime
python -B tools/fetch_python_runtime.py --output ../python-reader-runtime
git clone https://github.com/live-codes/browser-lean.git ../browser-lean
git -C ../browser-lean checkout a8aed095534e67061e2626b94e8e69193099091d
python -B tools/prepare_lean_wasm.py --source ../browser-lean --output ../lean-browser-runtime
python -B tools/build_reader_site.py --math-root ../komorebi-math --polyphase-root ../polyphase-float --mathjax-root ../reader-runtime --pdfjs-root ../pdf-reader-runtime --python-root ../python-reader-runtime --lean-wasm-root ../lean-browser-runtime --revision FULL_COLLECTION_COMMIT --output ../reader-site
python -B tools/check_reader_site.py --site ../reader-site
python -m http.server 8765 --directory ../reader-site

Replace FULL_COLLECTION_COMMIT with the output of git rev-parse HEAD. The runtime fetches verify pinned digests before installing MathJax, PDF.js and Python. The finished site serves both runtimes and its selected documents locally. Source receipt mismatches or missing reading files fail the build. The ZIPs identify their selected files and do not claim to be standalone build environments.

The PDF catalogue includes the main papers, visual guides and formal companions listed in the browse resources. The document publisher also renders edition Markdown, shows source files with line links, and follows explicit local TeX inputs. It never executes the manuscripts or programs. PDF page bookmarks and Markdown line references retain their destinations. Documents without a PDF keep their available source formats.

The build writes documents/index.json with the published file paths and source identities. The site checker verifies those copies, embedded reader targets, linked images and runtime integrity, in addition to HTML links and reading ZIPs.

Readable chapters

Paper VII has 25 reading pages: the opening orientation, three exact finite models, fifteen focused Part I topics, and all eight later source parts. Measurements, Kraus channels and error correction have separate reading pages. The chapters preserve the I, II and III numbering, original counter resets, 107 proof environments, and the same 1,820 mathematical expressions in order. The complete Part I page retains its earlier URL and passage anchors. All 38 original manuscript figures appear as inline PNGs with source captions, reviewed text descriptions, full-size links and the original PDFs. The asset record binds every PNG to its retained PDF with SHA-256 hashes and intrinsic dimensions. All 40 worked visual-atlas plates also have HTML pages, with 38 original drawings, 547 selectable drawing labels, and 945 source expressions. Each plate links to the manuscript passages it illustrates; those passages link back to the plates. The atlas retains its wording and evidence limits. This presentation adds no proof assessment or Lean execution.

The atlas renderer checks the prose and drawing math sequences, finite label loops, source hashes, image sizes, and both directions of the manuscript links. documents/paper-vii-atlas.json records the conversion. Drawings are reviewed crops of the frozen monograph PDF; rebuild them with python tools/render_paper_vii_atlas.py --pdftoppm PATH. The web build verifies the checked-in assets and requires no TeX compiler.

The chapter renderer publishes the main chapters of Papers I, II, III, IV and VII as readable HTML alongside their original source pages. Paper II's current verification snapshot has its own reading page. Each paper has a chapter index and bibliography, with links between chapters and recorded claim locations. Paper IV's atlas also has HTML plates; the original visual atlases remain available as on-site PDFs.

Paper IV's single source is divided into contiguous, checked line ranges for 17 main sections, the opening orientation and the atlas introduction. These ranges preserve original source lines and resolve claim links to the correct chapter. The 68 proof bodies, 95 numbered records and all 1,041 mathematical expressions in the main document are retained. Six receipt-bound figures are included. Source changes that shift section boundaries require a review of the chapter configuration.

The atlas renderer publishes all 26 Paper IV plates, including their retained prose and tables, 24 drawings, text descriptions and structured label transcripts. Integer references in the reading aids select original TikZ labels; mathematical values are not retyped. Each label must appear exactly once. The reader validates references to manuscript sections and statements, preserves original source-line links, and records the atlas and drawing mathematical input sequences in documents/paper-iv-atlas.json. The site checker re-derives those sequences from the published source files and verifies the rendered HTML.

Atlas manuscript references also generate return links at their exact section or statement. These links stay visible with proof navigation when optional source links are hidden. No relation is inferred from matching keywords. manuscript_backlinks in the conversion record stores the source-derived connections; the site checker verifies both directions for every plate.

Drawing PNGs and their source/image receipts are committed under website/assets/atlas/paper-iv/. To rebuild only these images, use python tools/build_atlas_figures.py --tectonic PATH_TO_TECTONIC --pdftoppm PATH_TO_PDFTOPPM --stage EMPTY_DIRECTORY. This compiles the unchanged TikZ in an isolated directory and renders 24 cropped pages. It does not execute the mathematical model generator or checker. The ordinary website build verifies the committed assets without requiring TeX. Evidence notes are explicitly attributed to the retained source edition; new reading descriptions do not extend its proof or formal-verification scope.

The renderer handles the selected manuscripts' prose, statement environments, references, equations, tables, code listings and receipt-bound figures. Its book configuration is explicit. The build checks chapter order against the main TeX file. Unsupported prose commands and unresolved references stop the build. It does not execute TeX. Mathematical macros and formal scope labels come from the retained main manuscript, with the first definition preserved for providecommand. Bibliography links use citation keys from each current BibTeX source so that they do not depend on a historical compiled bibliography.

The build compares the full sequence of mathematical expressions with the source and writes documents/readable-chapters.json with source identities, locations, macro definitions and conversion counts. The site checker also compares every rendered math input with its source expansion. The original pilot's documents/readable-paper-ii.json remains available. Original line URLs and claim records are preserved. Search includes chapter passages and equation excerpts. Extend the selected books only after checking syntax, source fidelity, figures, navigation and rendered mathematics. Passing these checks does not establish mathematical correctness or new Lean coverage.

The diagram guides cover all chapter figures in Paper I, Paper II, Paper III and Paper IV: 10, 13, 6 and 6 figures respectively. Each book's website/paper-*-figure-descriptions.json supplies concise image alternatives and guide anchors. Each description is bound to the reviewed PNG checksum; changed, missing or unused figures stop the build for review. Original captions remain unchanged, and description links stay visible in the quieter reading view. The first three guides also describe their 22, 24 and 24 atlas pages. Paper IV's guide links to the existing 26 HTML plates and their complete label transcripts.

Proof Path Theory reading edition

The Proof Path Theory HTML edition follows the retained manuscript from the preface through five parts, its theorem ledger, source-bound tables, and the final reproducible example. Chapter navigation, original TeX line links, selectable mathematics, original figures, PDF and visual sampler links, and routes to Lean, code and evidence are retained. Source expressions are checked against the unchanged TeX. The reading presentation adds no proof or formal verification assessments.

The converter also reads the five part-opening figures and four explanatory paragraphs from the manuscript's preamble macro. All 25 figure numbers follow the printed sequence. Captions, including their nine mathematical expressions, are included in the source and HTML checks. Plain references retain their authored numbers, the tagged condition links as (SC), and the nine bibliography entries retain their numeric citation order. The complete HTML edition contains 1,051 mathematical expressions and 51 proof environments.

Run python -B -m unittest discover -s tools -p 'test_proof_path_reading.py' -v to check manuscript boundaries, formula preservation, readable syntax and source illustrations. The normal website checker verifies published equations, chapter links and all reading ZIPs.

Publication

The reader website workflow builds and checks the site on pushes and pull requests. Only a successful build on main can deploy it through GitHub Pages. Pull requests receive build checks without publication. Library revisions are pinned so a rebuild cannot silently adopt unreviewed changes from another repository.

Update library pins deliberately after reviewing their changes and checks. Record qualifications in the existing publication metadata only after those runs finish successfully. A website build confirms its own navigation and packaging scope, not new mathematical or formal verification.

The workflow also runs the documented introductory Python and C examples. It checks the 26 hand-worked examples with exact rational, modular and finite-set calculations. The library workflows retain their broader platform and release checks.

Accessibility and known limits · Repository maintenance

The project overview, project map and three demonstrations introduce the collection as a whole. The map labels reading suggestions separately from documented source uses. It does not generate or certify a theorem dependency graph.

The website publishes examples/komorebi_demonstrations.py as a readable source page and an identical download. Its source record includes the collection revision and SHA-256. The site checker compares the download and displayed source. python -B tools/check_demonstrations.py runs each demonstration and compares its output with the corresponding guide. The website workflow runs this check alongside the existing hand-worked example checks. Demonstration pages also participate in the related work's search filter.

Run python -B tools/claim_navigation.py to regenerate the manuscript index, then run the normal status command to refresh the claim guide. --check compares the index with the receipt-bound source texts. Paper I keeps its existing correspondence records. The other core papers use literal statement environments and TeX inputs. The extractor does not expand macros, index historical environments or infer Lean coverage. Proof links identify immediately following proof blocks. A missing link does not assert that a proof is absent elsewhere.

Site search includes individual claim and glossary links, with filters for result type and repository. Search addresses preserve filters. Results load in groups of 40, and the next group remains reachable through the Show more results button. The claim index has separate paper and statement-type filters. Direct claim links reveal their paper even when an earlier filter would otherwise hide it.

The document publisher supplies the same reading routes on work pages and source readers. Indexed statement and proof lines have return links to the exact claim. Lean module return links use only the declaration paths already recorded in the claim index. These are navigation overlays. Downloaded source files remain byte for byte identical to their import receipts.

Search entries carry explicit work_ids. Reading files use their receipt owner, claims and proof locations use their recorded paper, and examples use the learning topic relationships. Glossary entries inherit the works linked by those topics. General guides and library pages stay outside a work filter unless a relationship is recorded. Work section results provide routes to proofs, Lean coverage and code instructions even where no individual source file has been selected for on-site reading.

The site checker validates search work identifiers and every result’s local page and fragment. Claim types and existing evidence assessments are unchanged.

Browser Python

The Python playground runs the three teaching demonstrations and the pinned Komorebi Math introductory example. A labelled preset dropdown loads the selected editor, source routes and expected output. Choices retain their page fragments, and switching presets keeps edits in the current page. The original example links remain available without JavaScript. Python starts on demand in a disposable module worker. Stop terminates the worker, including an infinite loop. Reset also restores the selected source. Each run uses a fresh namespace. A two minute timeout and an output limit keep ordinary mistakes manageable. The plain text editors support keyboard navigation.

website/python-runtime.json pins Pyodide, Python and the NumPy wheel with byte counts and SHA-256 checksums. tools/fetch_python_runtime.py verifies those files before the build copies them to the site. Pass their directory as --python-root to the site builder. Runtime files load from the same site. The reader does not upload editor contents or selected data files. Save draft explicitly stores code in this browser. Restore draft and Delete saved draft control that stored copy. Edited Python can still use browser networking, so this is not an isolated service for untrusted code.

tools/browser_python.py extracts the teaching functions without rewriting their bodies. It checks every library file against the pinned Git tree and produces a deterministic ZIP containing the package and its license. The worker verifies the ZIP checksum before loading it. downloads/python-playground.json records the sources, expected output and library revision. The static checker validates this record, the runtime and all source links. The workflow checks the extracted examples against their published output.

The tested browser library scope includes packet reconstruction, exact rational coordinate changes, and the finite reciprocal and Fubini sequence experiments described in Komorebi sequence shapes. NumPy is included. Optional packages, native backends and the rest of the library have not been qualified in the browser. A passing example does not establish a general theorem, execute Lean or change any proof status.

Plotting and data in the playground

The preset menu includes interactive 2D signals, a 3D surface, a 3D helix, a Matplotlib figure, symbolic SymPy calculations, SciPy integration and CSV/JSON data plotting. These are software tutorials, not new proof or novelty claims. NumPy, Matplotlib, SymPy and SciPy load on demand from the pinned runtime files. Direct imports of those packages also trigger loading. Dynamic imports may need an explicit import first. Interactive 3D uses WebGL through the pinned Plotly.js runtime. It includes front, top and default view buttons, image downloads, CSV and JSON downloads, and a table of the first 100 plotted samples.

website/python/komorebi_browser.py supplies the browser display bridge. show_plot(data, layout, description=...) accepts Plotly-style dictionaries for scatter, bar, heatmap, surface and scatter3d traces. show_matplotlib and ordinary plt.show() produce PNGs. export_file offers CSV, JSON or text downloads. The helper is separate from the Komorebi Math package and is included in the site source record with a checksum. Downloaded browser plotting scripts can be opened again through the playground's Python file control.

Upload controls read up to five UTF-8 CSV/JSON files locally, at most 2 MB each and 4 MB in total. The run receives a snapshot in uploaded_files. A run report records the executed code, output, package and collection revisions, figures, and input-file checksums. It omits the uploaded file contents. Edited code, printed output and individual results have separate download controls. Draft saving is explicit and local to this browser. Code runs locally.

The helper limits interactive figures to 50,000 samples, messages to 2 MB and combined figures and exports to 8 MB per run. Unsupported graphics or unavailable WebGL leave a visible error and downloadable data. Source-linked mathematical examples retain their existing evidence labels. The broader Komorebi Math library remains outside the tested scope except for the documented introductory operations and sequence experiments.

Komorebi sequence experiments

The playground opens with the source-linked sequence research group. It includes reciprocal coefficient growth, labelled 2D and 3D comparisons after factorial normalization, and the factorial-weighted Stirling rows from the Special Functions sequence atlas. General plotting tutorials remain available further down the menu.

tools/sequence_presets.py defines the programs, parameter bounds, expected output, related works and reading links. Reciprocal presets call the pinned library's reciprocal_coefficients. The factorial preset checks its row sums against fubini_sequence. Exact exports use integer and rational text to avoid losing large integer digits through JavaScript numbers. Charts use ordinary counts or floating-point logarithms as labelled. The 3D sequence views preserve the discrete parameter domains. They do not interpolate a continuous family.

Plot titles wrap above the chart. Larger labels, point shapes, patterned bars and keyboard-accessible series checkboxes help distinguish the data. The Enlarge plot control gives figures more height. PNG downloads retain titles and legends. The factorial weights preset includes a 2D map before its 3D view.

tools/test_sequence_python.py compares 448 reciprocal coefficients with independent ordinary rational-series inversion and 190 weighted Stirling entries with inclusion-exclusion. It also checks preset outputs and exact export normalization. The existing website workflow discovers these tests. Source records and proof assessments retain their previous scope.

Notation reference

The notation index provides symbol search and a source inventory for every work. Entries link to exact source lines and retain the paper’s own context. When an occurrence belongs to a rendered chapter passage, entry previews, expanded occurrence lists, and global search also offer Read passage. Its JSON downloads record every detected occurrence in the selected TeX, Markdown and text sources, with an optional reading_url resolved from the actual source file and line spans. Occurrences without a rendered destination keep their source link. PDF and image notation remain explicit coverage limits.

tools/notation_index.py builds the reference. manifests/notation-sources.json declares additional manuscript entrypoints. The reader follows their literal includes and checks source receipts before indexing. Parser regression tests and the site checker validate extraction, source positions, counts and links.

Unbraced letter arguments retain the separator after their TeX control word. For example, \mathbb R and \widehat T remain valid symbol spellings in the index. Braced arguments and arguments that are commands retain their existing entry keys. Complete source expressions and their positions remain unchanged. Unambiguous legacy fragment anchors remain available for previously joined spellings. They open the corrected entry without changing its canonical ID.

Display permits the reviewed standard mathematical commands and literal braced roman labels such as \mathcal D_{\rm spectrum}. The exact TeX spelling remains available for copying and source comparison. Unfamiliar macros, parameterized macros, incomplete commands, and unsupported declaration forms remain source-TeX fallbacks. The K-COS display audit uses the pinned MathJax runtime.

Search excerpts omit recognized layout commands and source bookkeeping such as Needspace and RecordID. Balanced arguments keep nested metadata out of the preview while preserving section titles, literal set braces and escaped text characters. These previews remain reading aids: the downloadable occurrence records and linked source passages retain the exact original text and positions.

Word searches can use the source's explicit definition title as the result heading, with a direct link to its reading passage. Names follow the enclosing definition scope, including long definitions; unnamed definitions keep a generic label. Symbol searches keep the matched symbol visible and identify its source definition separately. Matching symbol spellings remain available in a disclosure. The build checks title metadata against the source; comments and code examples cannot supply a definition name.

Source-bound proofreading notes

The 1 November 2026 proofreading record covers the main online chapter text of Papers I and II. Two labelled editorial reading notes clarify Paper II's abbreviated Fourier hypotheses and the two uses of t in its walk-series subsection. The retained manuscripts, mathematical expressions, statement numbering and proof bodies are unchanged.

tools/reader_proofreading.py binds the review to 17 source-file hashes and exact source passages. Notes link to the existing HTML definitions and publish their record at documents/reader-proofreading.json. The build rejects stale source bindings, moved reference targets, missing notes and duplicate placements. This is a proofreading record, with no new proof audit, Lean replay or external citation verification. Visual atlases and PDF layout are outside its coverage.

The Papers III and IV proofreading record covers Paper III's four main chapters and Paper IV's eighteen non-atlas reading sections, plus their abstracts, notation, preambles and bibliography syntax. No objective routine correction was identified in that scope. The record binds eight retained source files and reports the scoped syntax checks. The same exclusions apply; the manuscripts and mathematical statements are unchanged.

The Papers V and VI proofreading record covers 88 non-atlas reading sections, their abstracts, notation, preambles and bibliography syntax. It recommends two wording corrections for a later edition: “minimum cost among all admissible prunings” in Paper V's best-basis theorem, and “potential weight” in Paper VI's alternating-product theorem. Both adjacent interpretations already explain the intended meaning. The record binds four source files and reports the syntax checks. The retained text and mathematics are unchanged; the same review exclusions apply.

The Paper VII proofreading record covers its 25 main reading sections, front matter, notation, cross-references, figure captions, preamble and bibliography syntax. The finite core, strengthened development, six supplements and three retained alternative derivations were reviewed. No objective routine correction was identified in that scope. The record binds twelve source files and reports the syntax checks. The retained text and mathematics are unchanged; the same review exclusions apply.

The Paper VIII proofreading record covers its 23 main reading sections: the orientation and abstract, three exact models, fifteen manuscript sections and Appendices A–F, together with notation, cross-references, captions, preamble and bibliography syntax. No objective routine correction was identified in that scope. The record binds ten source files and reports the syntax checks. The retained text and mathematics are unchanged; the same review exclusions apply.

The Paper IX proofreading record covers its 56 main reading sections, front matter, notation, cross-references, captions, preamble and bibliography syntax. The five mathematical appendices, continuation notes, checkpoint supplements and recovered historical text were included. One grammar correction is recommended for a later edition: the singular subject in “The full exact classification … are” requires “is.” The record binds 39 source files and gives the exact source and reading passage. The retained text and mathematical tokens are unchanged; the same review exclusions apply.

The Paper X proofreading record covers its 30 main reading sections, front matter, notation, cross-references, captions, preamble and bibliography syntax. The algorithms and reproducibility appendices, retained checkpoints, residue-counting continuation, final conditional completion and atlas introduction were included. One punctuation correction is recommended for a later edition: the smooth-chart digit-stream display ends its sentence with a comma and should end with a period. The record binds six source files and gives the exact source and reading passage. The retained text and mathematical tokens are unchanged; the same review exclusions apply.

The Paper XI proofreading record covers all 38 main reading sections, the fifteen construction appendices, literal derivation blocks, front matter, notation, references, captions, tables, preamble and both bibliography files. Two corrections are recommended for a later edition: clarify the tensor example's carrier-dimension wording and protect German title capitalization in the generated bibliography. The record binds 19 source files and gives the exact source and reading passages. The retained text and mathematical tokens are unchanged; the same review exclusions apply.

The Paper XII proofreading record covers all 16 main reading sections, including the reading map, abstract, publication scope, thirteen manuscript sections and complete verification/revision record, plus notation, references, captions, tables, preamble and both bibliography files. One bibliography typography correction is recommended for a later edition: use “pp.” before the Mazur entry's page range. The record binds four source files and gives the exact source and reading passage. The retained text and mathematical tokens are unchanged; the same review exclusions apply.

Recovery Laboratory

recovery-lab.html extends the introductory shared-summary diagram to exact linear measurements on 2–4 real input coordinates. Readers edit up to four measurement rows and three question rows, using integers from −99 to 99 or fractions whose numerator is in that range and whose denominator is 1–99. Checkboxes select the available measurement rows. Six starters distinguish recoverability, partial loss, redundancy, fractional rules, and full recovery.

The four-step guided investigation introduces information loss, a recoverable combination, partial recovery, and minimal repair. Each step loads a tested starter, gives a prediction with explanatory feedback, and suggests a concrete experiment. A changed-workspace note distinguishes edited settings from the guide's starting example. The guide is optional and can be collapsed.

website/assets/recovery-lab-guidance.mjs supplies these explanations and consumes the existing exact model. Worked substitutions use the actual enabled measurement values. Obstruction examples use a separating pair at t = 1 even when the exploration slider is zero. “Read the rows as equations” connects matrix coefficients to weighted sums and values at the current base input.

For two-coordinate inputs, the fiber picture distinguishes a line, a point, and the whole plane according to nullity. For every supported dimension, the answer-versus-t graph compares the selected answer with its base value. All nine integer samples are recomputed by the exact model and available in a captioned table. The description explicitly distinguishes a single flat trace from the certificate's check of every invisible direction. Neither graph changes the audited core or the scope of the recovery claim.

Graphs have visible descriptions, exact tables, and shape/line distinctions. Motion controls have keyboard instructions, value descriptions, and step buttons. Overflowing table regions are named and keyboard-focusable. Changes announce concise results on committed edits and slider changes; full certificates are outside live regions. Native controls, visible focus, forced-color styles, wrapping formulas, and layouts at 320 CSS pixels support access. These checks do not establish screen-reader compatibility or WCAG conformance. The descriptions and status behavior follow the approaches in WAI's complex image guidance and status message guidance.

tools/recovery_lab.py publishes the page and search entry. Its model, website/assets/recovery-lab-core.mjs, uses reduced BigInt fractions throughout row reduction, kernel construction, recovery weights, and rank-based repair. The model and controller imports use content versions. A successful question shows weights giving its row exactly; an unsuccessful one shows a vector w with Rw = 0 and Fw ≠ 0. The input and summary plots approximate the exact values in the adjacent table. A zero motion parameter makes the displayed points coincide without changing the global obstruction certificate.

The repair retains an independent subset of enabled measurement rows, removes redundant and disabled rows, and adds independent question rows until every question is recoverable. The additional row count is rank([R; F]) − rank(R). Undo restores the original settings. Versioned share links retain all matrices, selections, base inputs, and inspection settings; malformed links are rejected. JSON downloads contain settings and recomputed exact certificates. Invalid matrix edits keep the last valid result visible and disable sharing and repair until the entries are complete.

Run node --test tools/test_recovery_lab.cjs and python -B -m unittest discover -s tools -p 'test_recovery_lab.py' -v. tools/audit_recovery_lab.py independently checks 1,604 cases with Python Fraction arithmetic and ranks from determinants of minors. These comprise 1,354 exhaustive two-coordinate cases and 250 seeded rational cases, including coefficients at the supported bounds. The checks verify recovery products, kernel bases, obstruction witnesses, row-operation matrices, collisions, and minimal sufficient repairs. The page explains the general linear-algebra argument separately; finite software checks add no manuscript proof review or Lean coverage. The bounded run manifest binds the audited model and oracle bytes; its result records the tested case and certificate counts. Recovery-specific line-ending rules live in tools/.gitattributes, website/assets/.gitattributes, and verification/recovery-lab/.gitattributes. The root attributes file is retained byte for byte because the Euler publication record binds it. The recovery tests check both that binding and the scoped attributes.

Signal Laboratory

signal-lab.html is a larger known-reference signal experiment with 16–256 samples. Its maintained interface is in tools/signal_lab.py; the model and browser controller are website/assets/signal-lab-core.mjs and website/assets/signal-lab.js. The shared site builder publishes it and adds its search entry. Both the page script and model import use content versions.

signal-lab-workspace.mjs supplies bounded sample strokes, a 32-edit history, and validated notebook serialization. Its import and the model import both use content versions, including nested module references. Drawing fills crossed sample addresses and commits a stroke on release; cancellation restores the previous reference. The precise sample editor provides keyboard access.

The notebook keeps at most 12 labeled settings records in local browser storage and falls back to the current tab if storage is unavailable. JSON imports append atomically within that limit. All metrics are recomputed from settings; stored result fields are ignored. Saved reconstructions are overlaid only when both reference and observed arrays match exactly. Resetting the active lab retains the notebook. Its JSON and results CSV are separate from the active experiment's exports and share link. node --test tools/test_signal_lab_workspace.cjs checks stroke/history behavior, import boundaries and comparison eligibility.

The four starter experiments append two compatible runs and open their comparison. They preserve existing notebook entries and require two free slots. The comparison inspector switches among reconstructions, signed errors (reconstruction minus reference), and differences (B minus A). Its pointer and keyboard sample selection is independent of the active experiment's inspector. The largest-difference action chooses the first address attaining the maximum absolute separation. A numeric comparison CSV and sample table retain both reconstructions and all signed values. Mismatched data disables these views and exports. The workspace tests cover starters and an exact zero-versus-full sample-coordinate fixture for the comparison values and CSV signs.

Comparison links use a bounded, versioned UTF-8 payload in the #compare= fragment. The payload contains exactly two validated named settings records, one of the three plot views, and an in-range comparison address. Results are recomputed and the data-compatibility guard is checked on restoration. The preview is separate from notebook storage and works even when the notebook is full. Saving both runs is an explicit append action and requires two free slots. Closing a preview restores notebook selection; ordinary experiment links omit the comparison fragment. Malformed comparison links preserve the current valid experiment and notebook. Clipboard failure exposes a selectable link field.

The comparison region inspector accepts inclusive integer addresses, including a single sample. compareRegion derives local RMS error, mean signed error, maximum absolute error and its first address from the existing full-signal reconstructions. The chart rescales both axes, while sample selection, the largest-difference action, sample table and CSV stay within that region and retain original addresses. Maximum-error buttons inspect each run's worst local sample. Invalid edits keep the last applied region. Selecting another pair or a starter resets the region to the full signal.

Version-1 comparison links optionally include region: [start, end]; links without it retain the full-signal behavior. A linked selected address must be inside the region. Opening a preview leaves notebook storage unchanged; saving its runs keeps the current region in the open comparison. Notebook JSON stores run settings, so use a comparison link to preserve the selected region. Exact sample-coordinate fixtures check regional metrics, CSV boundaries, single samples, and ties; regional partitions recover whole-signal squared errors across all supported sizes and bases.

The quality-target finder uses the active experiment's existing error curves. It scans every budget in order, including zero, for either observed-energy retention (0–100%) or reference RMS error (0–64). Reference error need not be monotone; no qualifying budget is reported when the entire curve misses the target. Threshold checks allow 1e-10 * max(1, relevant signal energy) in squared-error units. Zero observed energy satisfies retention targets at zero budget. Applying a result changes the active basis and budget. Saving qualifying runs appends the reachable settings as one group within notebook capacity; it does not replace saved entries. The finder controls are an analysis aid; saved experiments and links retain the resulting applied basis and budget.

The lab compares averaging-normalized Haar wavelets with their support weights, an orthonormal DCT-II, and sample coordinates. Seeded bounded integer noise, equal coefficient budgets, three selection policies, full budget/error curves, component inspection, CSV/JSON import/export, and shareable settings are supported. Imported samples become the known reference before simulated noise is added. The minimum-budget action uses this reference and a stated numerical tolerance. It is not an estimator for an unknown clean signal.

The website workflow runs node --test tools/test_signal_lab.cjs and python -B -m unittest discover -s tools -p 'test_signal_lab.py' -v. The model tests include every mask of one 16-sample benchmark in each basis. For an independent bounded numerical check, run python -B tools/audit_signal_lab.py --node node --output signal-lab-report.json with NumPy installed and a fresh report filename. This checks 180 explicitly specified configurations and 54,108 budget cases using NumPy FFT/IFFT and explicit Haar support vectors. Its report records the tested range and numerical errors; it does not change manuscript or proof status.

Interactive Lean workspace

The collection-wide native runner at lean/run.html extends execution beyond the single-file pilot. Every displayed Lean source links to its selected workspace and command. See Running the retained Lean sources for the source bundle, manual GitHub workflow, retained/reconstructed environments, compiler receipts and dedicated-server export path.

The homepage's Lean workspace card opens lean/browser/index.html without selecting a paper or source file in the URL. This is our local WebAssembly compiler: visitors choose a published workspace, edit source, and run Lean in their browser. Inspect Lean and source pages use this compiler too. See Browser Lean for the prepared workspaces, runtime delivery, supported imports and current limits.

The former lean/playground.html address remains as a compatibility alias. Its local script replaces the old history entry with the general workspace; a visible link also works without JavaScript. Old query strings and fragments do not select a paper. lean/playground.json records the local target and retired-route status. The hosted editor and its Paper XII starting file have been removed. Site builds do not run Lean or assign new verification status.

CI runs test_browser_lean.py and test_browser_lean.cjs. The site verifier checks the alias target, build revision, local content routes and absence of external frames. The route tests also cover the homepage link and redirect behavior under both root and repository-subpath hosting.

Paper navigation

Paper, source and PDF pages keep the overview, chapter contents, visual atlas and main reading format together. Supporting destinations are grouped under More resources. Overview pages also expose the visual atlas directly when a work has one. Existing URLs and source passage anchors are retained.

Chapter and atlas reading bars share previous/next controls, position markers, an overview link and a complete jump menu. Paper VI's contents and chapter menu group the reading sequence by its four parts and references. The current part opens in the chapter menu. Contents groups, plate pickers and resource menus use native disclosures, so they remain usable without JavaScript. Both complete visual atlases use the chapter sidebar for their on-page contents and keep PDF and source options in a separate disclosure. Paper IV's visual atlas uses the same controls and sidebar.