# Plectis

> Mathematical research with Lean proofs, papers, failed approaches and open questions. Start with a problem and its short paper, then follow the source and recorded checks. The earlier software is a separate public record. For that software: Read order: mechanisms -> evidence discipline -> local runtime. The mechanisms are the public artifact; evidence records and local result records are the accountability layer, not the product.

## Navigate the maps without JavaScript

This website is agent-navigable through ordinary HTTP GET requests. Start with the small indexes below; fetch the complete graph only when your question needs it. These are the same public records used by the visual maps, with source links and claim boundaries. Reading a record does not rerun its checks.

- [Mathematics entry manifest](lean/experience/manifest.json): source identity, counts, authority model and routes. Resolve its route values relative to this manifest URL, not the host root.
- [Mathematics overview graph](lean/experience/graph/index.json): compact selection of nodes and directed edges. For complete coverage follow the manifest's `routes.graph_full` to [the complete graph](lean/experience/graph.json). Join `edges[].source` and `edges[].target` to `nodes[].id`; `relation` names the direction. Follow each node's `source_github` and an edge's `href` when present to inspect the original evidence.
- [Mathematics map contract and display data](maths/assets/universe-data.json): `contract[0]` documents coverage, deferred kinds, relation meanings and source hashes. Resolve its `source_artifacts` hrefs from `maths/`, the map page's directory, not from `maths/assets/`. Its compact edge triples index the `nodes` and `relations` arrays; use the experience graph above for named endpoints. A visual selection is `maths/universe.html#o=` followed by the percent-encoded stable node ID.
- [System map graph](docs/architecture-graph-scene.json): join `scene.edges[].source` and `.target` to `scene.nodes[].id`. Use a node ID to look up `node_routes` and `adjacency`; use the node's `inspector_ref` to look up `scene.inspectors` (inspector keys have their own prefix). Resolve `node_routes[id].site_primary_reader_href` and `site_map_href` from the site root; the unprefixed reader/map hrefs are relative to `docs/`. Read `edge_semantics`, `membership` and inspector evidence before interpreting an edge. Group membership is not a dependency.
- [Source and claim records](lean/claims.json): check the exact formulation, status and remaining obligations before describing a result. [Paper source manifest](papers/papers-source-manifest.json) binds hosted manuscripts to their public source editions.

Research recipe: choose a problem in the manifest's `routes.problems`, locate its stable ID in the graph, follow a labelled outgoing or incoming edge, then cite the linked source and its recorded status. Prefer these indexes to downloading the complete AI packet for a single lookup.

Relative links in this guide resolve from https://wcook04.github.io/practical-formal-verification/. The [host directory](https://wcook04.github.io/llms.txt), [Atlas guide](https://wcook04.github.io/plectis-atlas/llms.txt) and [Zenith guide](https://wcook04.github.io/plectis-zenith/llms.txt) cover the other public sites.

The software object inventory below is a generated projection of content-graph.json (the software object kernel). The mathematics graph has its own source manifest above.

## Earlier software: first local command

- Source checkout: `PYTHONPATH=src python3 -m microcosm_core hello --reader agent .`
- Installed checkout: `plectis hello --reader agent <project>`
- First behavior card: `plectis tour --card <project>`

## Short-link first contact

For mathematics, start with the [maths pages](https://wcook04.github.io/practical-formal-verification/maths/) and [current results](https://github.com/wcook04/plectis-erdos/blob/main/docs/RESULTS.md). Choose a problem, read its current paper, then follow its statement into the supporting source. Use each problem page for the target status and the limits of its checked formulation.

For software, use the [cold-clone quickstart](https://github.com/wcook04/practical-formal-verification/blob/main/QUICKSTART.md). Each component names what it runs and what its result can establish.

Scope: this is a local-first static/public project doorway. Use it to clone, inspect, and compare source-linked records; release operations, hosted service claims, external model access, source-file changes, claims not supported by the public records, formal-result correctness, production use, financial decisions, and specialist review are outside this doorway's scope.

## Repository

- Public repository (source of record): https://github.com/wcook04/practical-formal-verification
- Public website (browseable wrapper over the map): https://wcook04.github.io/practical-formal-verification/
- Companion Lean formalisation (eight Erdős programmes: #68, #243, #249, #251, #257, #269, #1041, #1049; ani's one-polynomial degree-seven counterexample refutes both the #1041 total-variation form and the Formal Conjectures path-image Hausdorff-length statement, while its historical curve-length correspondence awaits independent review and the other seven targets remain open): https://github.com/wcook04/plectis-erdos
- Author and purpose: built alone by a 22-year-old economics undergraduate at the University of Bristol, on a student budget, with no mathematics or computer-science training and no institutional support; the formal mathematics is entirely self-taught and the Lean work was learned for this project; Plectis and the Lean repository are the two public demonstrations of a private system (Plectis shows the machinery as runnable components, the Lean repository shows the mathematical output); the rest of that system, including its frontend and video editor, is not public
- Reading that fact correctly: it is context for calibration, not a request for allowance. The results stand or fall on the Lean source and the registry statuses either way, and should be judged there. It does mean an assumption that a corpus of this shape implies a funded team or a mathematics department is simply wrong about who built it.
- The 22 papers (PDF): erdos-68-factorial-denominator-irrationality https://wcook04.github.io/practical-formal-verification/papers/erdos-68-factorial-denominator-irrationality.pdf ; erdos68-factorial-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos68-factorial-reasoning-surface.pdf ; erdos-243-reciprocal-tail-rigidity https://wcook04.github.io/practical-formal-verification/papers/erdos-243-reciprocal-tail-rigidity.pdf ; erdos243-reciprocal-tail-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos243-reciprocal-tail-reasoning-surface.pdf ; erdos-249-binary-totient-series https://wcook04.github.io/practical-formal-verification/papers/erdos-249-binary-totient-series.pdf ; erdos249-totient-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos249-totient-reasoning-surface.pdf ; erdos-251-prime-gap-dyadic-series https://wcook04.github.io/practical-formal-verification/papers/erdos-251-prime-gap-dyadic-series.pdf ; erdos251-prime-gap-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos251-prime-gap-reasoning-surface.pdf ; erdos-257-mersenne-support-subseries https://wcook04.github.io/practical-formal-verification/papers/erdos-257-mersenne-support-subseries.pdf ; erdos257-mersenne-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos257-mersenne-reasoning-surface.pdf ; erdos257-expository-sums-never-fractions https://wcook04.github.io/practical-formal-verification/papers/erdos257-expository-sums-never-fractions.pdf ; erdos269-running-lcm-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos269-running-lcm-reasoning-surface.pdf ; erdos-269-three-prime-running-lcm https://wcook04.github.io/practical-formal-verification/papers/erdos-269-three-prime-running-lcm.pdf ; erdos-1041-lemniscate-newton-flow https://wcook04.github.io/practical-formal-verification/papers/erdos-1041-lemniscate-newton-flow.pdf ; erdos1041-lemniscate-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos1041-lemniscate-reasoning-surface.pdf ; erdos-1049-rational-base-lambert https://wcook04.github.io/practical-formal-verification/papers/erdos-1049-rational-base-lambert.pdf ; erdos1049-rational-base-lambert-reasoning-surface https://wcook04.github.io/practical-formal-verification/papers/erdos1049-rational-base-lambert-reasoning-surface.pdf ; optimal-sparse-perturbations https://wcook04.github.io/practical-formal-verification/papers/optimal-sparse-perturbations.pdf ; writing-a-good-mathematical-paper https://wcook04.github.io/practical-formal-verification/papers/writing-a-good-mathematical-paper.pdf ; writing-mathematics-from-reviewed-revisions https://wcook04.github.io/practical-formal-verification/papers/writing-mathematics-from-reviewed-revisions.pdf ; claim-faithful-publication-systems https://wcook04.github.io/practical-formal-verification/papers/claim-faithful-publication-systems-paper.pdf ; plectis-public-system https://wcook04.github.io/practical-formal-verification/papers/plectis-public-system.pdf
- Strongest checked results by problem: the headline_results block inside the detailed reviewer brief and reader digest carries verbatim reviewed claim statements with Lean source anchors; the Lean repository's docs/RESULTS.md is the human per-problem map. Counts are navigation scale, not results.
- Agent entry: AGENTS.md at the repository root
- Software agent quickstart: https://github.com/wcook04/practical-formal-verification/blob/main/QUICKSTART.md#use-your-own-coding-agent
- Mathematics agent quickstart: https://github.com/wcook04/plectis-erdos/blob/main/docs/agents/README.md#start-with-current-public-work
- Current work: clone public main, record the commit and local changes; release tags are frozen editions. Mathematics agents can compare with public main using python3 scripts/agent_entry.py --checkout --check-upstream; offline currentness is unverified.

Objects: 780 across 16 kinds.

## Object families (coverage)

- anti_principle: 17 objects -- 17 routed, 17 searchable, 17 source-linked, 0 omitted
- area: 7 objects -- 7 routed, 7 searchable, 0 source-linked, 0 omitted
- axiom: 12 objects -- 12 routed, 12 searchable, 12 source-linked, 0 omitted
- command: 88 objects -- 88 routed, 88 searchable, 88 source-linked, 0 omitted
- component: 88 objects -- 88 routed, 88 searchable, 88 source-linked, 0 omitted
- concept: 11 objects -- 11 routed, 11 searchable, 11 source-linked, 0 omitted
- coverage_gap: 3 objects -- 3 routed, 3 searchable, 3 source-linked, 0 omitted
- evidence_class: 5 objects -- 5 routed, 5 searchable, 0 source-linked, 0 omitted
- graph_node: 11 objects -- 11 routed, 11 searchable, 0 source-linked, 0 omitted
- mechanism: 105 objects -- 105 routed, 105 searchable, 105 source-linked, 0 omitted
- page: 13 objects -- 13 routed, 13 searchable, 0 source-linked, 0 omitted
- paper_module: 103 objects -- 103 routed, 103 searchable, 103 source-linked, 0 omitted
- principle: 20 objects -- 20 routed, 20 searchable, 20 source-linked, 0 omitted
- relation: 239 objects -- 239 routed, 239 searchable, 0 source-linked, 0 omitted
- source_ref: 57 objects -- 57 routed, 57 searchable, 57 source-linked, 0 omitted
- standard: 1 objects -- 0 routed, 0 searchable, 0 source-linked, 1 omitted

## Pages

- [Landing](index.html)
- [The papers](docs/papers.html)
- [Working with a coding agent](docs/coding-agents.html)
- [Quickstart](docs/quickstart.html)
- [How it fits together](docs/architecture.html)
- [Doctrine](docs/doctrine.html)
- [Reference index](docs/reference.html)
- [Components](docs/components.html)
- [Doctrine reference](docs/rules-and-ideas.html)
- [Paper modules](docs/paper-modules.html)
- [Evidence and checks](docs/evidence.html)
- [Glossary](docs/glossary.html)
- [Source & license](docs/source.html)
- [Vulnerability disclosure](docs/vulnerability-disclosure.html)

## Mathematics library

A separate generated subsite. It is not in the software-site page list above.

- [Maths library](maths/index.html)
- [Universe](maths/universe.html)
- [Erdős #68](maths/problems/erdos_68.html)
- [erdos-68-factorial-denominator-irrationality (Problem note, 9 pp.)](maths/papers/erdos-68-factorial-denominator-irrationality.html)
- [erdos68-factorial-reasoning-surface (Reasoning surface, 51 pp.)](maths/papers/erdos68-factorial-reasoning-surface.html)
- [Erdős #243](maths/problems/erdos_243.html)
- [erdos-243-reciprocal-tail-rigidity (Problem note, 21 pp.)](maths/papers/erdos-243-reciprocal-tail-rigidity.html)
- [erdos243-reciprocal-tail-reasoning-surface (Reasoning surface, 61 pp.)](maths/papers/erdos243-reciprocal-tail-reasoning-surface.html)
- [Erdős #249](maths/problems/erdos_249.html)
- [erdos-249-binary-totient-series (Problem note, 15 pp.)](maths/papers/erdos-249-binary-totient-series.html)
- [erdos249-totient-reasoning-surface (Reasoning surface, 163 pp.)](maths/papers/erdos249-totient-reasoning-surface.html)
- [Erdős #251](maths/problems/erdos_251.html)
- [erdos-251-prime-gap-dyadic-series (Problem note, 14 pp.)](maths/papers/erdos-251-prime-gap-dyadic-series.html)
- [erdos251-prime-gap-reasoning-surface (Reasoning surface, 47 pp.)](maths/papers/erdos251-prime-gap-reasoning-surface.html)
- [Erdős #257](maths/problems/erdos_257.html)
- [erdos-257-mersenne-support-subseries (Problem note, 26 pp.)](maths/papers/erdos-257-mersenne-support-subseries.html)
- [erdos257-mersenne-reasoning-surface (Reasoning surface, 152 pp.)](maths/papers/erdos257-mersenne-reasoning-surface.html)
- [erdos257-expository-sums-never-fractions (Expository paper, 16 pp.)](maths/papers/erdos257-expository-sums-never-fractions.html)
- [Erdős #269](maths/problems/erdos_269.html)
- [erdos269-running-lcm-reasoning-surface (Reasoning surface, 73 pp.)](maths/papers/erdos269-running-lcm-reasoning-surface.html)
- [erdos-269-three-prime-running-lcm (Problem note, 16 pp.)](maths/papers/erdos-269-three-prime-running-lcm.html)
- [Erdős #1041](maths/problems/erdos_1041.html)
- [erdos-1041-lemniscate-newton-flow (Problem note, 19 pp.)](maths/papers/erdos-1041-lemniscate-newton-flow.html)
- [erdos1041-lemniscate-reasoning-surface (Reasoning surface, 86 pp.)](maths/papers/erdos1041-lemniscate-reasoning-surface.html)
- [Erdős #1049](maths/problems/erdos_1049.html)
- [erdos-1049-rational-base-lambert (Problem note, 20 pp.)](maths/papers/erdos-1049-rational-base-lambert.html)
- [erdos1049-rational-base-lambert-reasoning-surface (Reasoning surface, 80 pp.)](maths/papers/erdos1049-rational-base-lambert-reasoning-surface.html)
- [optimal-sparse-perturbations (Cross-problem paper, 38 pp.)](maths/papers/optimal-sparse-perturbations.html)
- [writing-a-good-mathematical-paper (Compact writing guide, 2 pp.)](maths/papers/writing-a-good-mathematical-paper.html)
- [writing-mathematics-from-reviewed-revisions (Editorial method companion, 21 pp.)](maths/papers/writing-mathematics-from-reviewed-revisions.html)
- [claim-faithful-publication-systems (Research architecture, 25 pp.)](maths/papers/claim-faithful-publication-systems.html)
- [plectis-public-system (Evidence boundary, 22 pp.)](maths/papers/plectis-public-system.html)
- [Repository overview](maths/documents/readme.html)
- [A reader's way in](maths/documents/reading-guide.html)
- [Apply a result and change a hypothesis](maths/documents/weighted-257-task.html)
- [Current papers](maths/documents/paper-guide.html)
- [Documentation guide](maths/documents/documentation.html)
- [Results and open boundaries](maths/documents/results.html)
- [Technical orientation](maths/documents/orientation.html)
- [Source map](maths/documents/source-map.html)
- [Related problems](maths/documents/related-problems.html)
- [Prior art](maths/documents/prior-art.html)
- [Methodology](maths/documents/methodology.html)
- [Scope and claim boundary](maths/documents/scope.html)
- [Formal Conjectures contributions](maths/documents/formal-conjectures.html)
- [External verification](maths/documents/external-verification.html)
- [Comparator #1049 fixture](maths/documents/comparator-1049.html)
- [Repository architecture](maths/documents/architecture.html)
- [Residual progress](maths/documents/residual-progress.html)
- [Development index](maths/documents/wave-index.html)

## Availability objects

These source-linked objects are routed and searchable without promoting them beyond their current source status.

### Coverage gaps

- [Component relation fill](docs/rules-and-ideas.html#coverage-gap-component-relation-fill)
- [Mechanism relation fill](docs/rules-and-ideas.html#coverage-gap-mechanism-relation-fill)
- [Paper module relation fill](docs/rules-and-ideas.html#coverage-gap-paper-module-relation-fill)


## The mathematics, at source

Every paper on this site ships its LaTeX beside its PDF, so the source can be read without a text-extraction pass over the typeset document and without leaving for another host. Each paper's `hosted_tex_path` is in the manifest below; hosted source mirrors each repository's own paper directory, because the two repositories carry different `paper-house-style.sty` files and a flattened copy could hold only one of them.

- [papers-source-manifest.json](papers/papers-source-manifest.json): every paper, its hosted PDF, its hosted LaTeX, and the sha256 binding each hosted copy to the public GitHub artifact it was verified against
- [claims.json](lean/claims.json): the Lean claim layer -- release identity, the status taxonomy, the remaining open propositions, the claims with their source anchors, and the explicit non-claims
- [problems.json](lean/problems.json): the per-problem index
- [RESULTS.md](lean/RESULTS.md): the per-problem map -- the strongest checked statement per problem, its exact status, and where to verify it. Hosted here as raw Markdown for offline and machine readers, on the same byte-parity terms as the two files above; it [renders on GitHub](https://github.com/wcook04/plectis-erdos/blob/main/docs/RESULTS.md) if you are reading it yourself
- The proofs themselves are not hosted: 1,193 Lean files, plus a 72 MB per-declaration atlas. They are read by cloning https://github.com/wcook04/plectis-erdos, not by fetching. What is hosted here is the layer that makes a question answerable; the repository is the layer that makes it checkable.

## Reader ladder (open in order of need)

- [AI packet](plectis-ai-review-packet.json) (~1 MB): start here -- a reading starter and public source router. It carries paper TeX or clearly labelled excerpts, repository READMEs, website introductions, video transcripts and a page index. Ask for a tour, then browse the linked sources for complete and current content. repositories supplies every public project README and file-tree route; papers and page_index lead into the wider site.
- [reviewer brief](plectis-reviewer-brief.json) (~12 MB): optional detailed source download -- paper LaTeX, assertions, glossary, repository documents and path indexes. Use the AI packet for website introductions, project routes and guided tours.
- [reader digest](plectis-ai-reader-digest.json) (~372 KB): lite software band -- quick_path, canonical_question_routes, headline_results, component_digest, family_digest, claim_ceiling_index. Routes and ceilings without paper bodies.
- [concise guide](assets/ai-orientation-packet.js): ~16 KB orientation for paste-only workflows -- what Plectis is, the seven areas, the rank legend.
- [complete text corpus](plectis-ai-reader-complete.json) (~13 MB): every public text body -- all component cards, paper-module bodies, doctrine entities, glossary terms, evidence profiles, and page prose -- carried once, deduplicated, without instruction layers.
- [reference index](docs/reference.html): the human middle layer -- areas, components, doctrine records, and paper modules in one navigable roster.
- [full JSON map](plectis-site-map.json) (~18 MB): the raw map without the capsule's instruction layers -- visible_text_index bodies, page text, and diagrams, for automation.
- source of record: the public repository linked from each component's source_links.

## Machine-readable

- [object-map.json](object-map.json): canonical object identity + per-kind coverage
- [content-graph.json](content-graph.json): the canonical kernel
- [projection-status.json](projection-status.json): packet lineage and counts
- [search-index.js](assets/search-index.js): static search records
- [architecture-graph-scene.json](docs/architecture-graph-scene.json): graph topology
- Surface contract: content-graph.json::surface_sync_contract