Components

cold_reader_route_map makes Microcosm's first ten minutes executable. It validates a public route map whose rows bind the first-run sequence to runnable commands, docs refs, result record refs, and scope limits.

Purpose

A cold technical reader should not have to infer the product path from a long README or raw result record tree. The route map answers one question: what should I run first, and what evidence proves that path is wired?

The unusual part is how the validator checks that proof. It does not merely confirm that each route row carries the right fields. It replays every route against real source: each row's command, its docs refs, its result record refs, and the human-readable signals it claims to show are matched against the actual text of copied source modules and public docs. A command whose material tokens do not appear anywhere in that source corpus is blocked, as is a docs ref that does not resolve to a real heading and a result record ref that does not open a pass-status result record. So a route cannot promise a command the system does not actually run, which is the failure mode a hand-written quick-start guide drifts into the moment the commands change underneath it.

The evidence contract is source-open by default: public route cards, route result record bindings, route policy, exported bundle refs, and generated result records carry the system, while secret_exclusion_scan excludes only private source bodies, model-output data, account or browser material, secrets, and account secret-equivalent live-access data. Result record bodies are not inlined; they are represented by body_in_receipt: false plus public runtime refs.

Shape

flowchart LR subgraph Entry["First-screen entry"] Project["Public project path repo -> .microcosm"] First["First-screen card claim frame, first command, evidence legend, exit rule"] end subgraph Accounting["Route-map accounting"] Route["Ordered route rows command, result record ref, evidence class"] Ceiling["Scope boundary and scope limit attached to each row"] end subgraph ReaderBranch["Reader branch"] Branch["Reader branch choose one first action"] Safety["Safety/evals status, authority, workingness"] Hiring["Hiring reviewer first-screen card, legibility scorecard"] Developer["Peer developer tour, observe, explain or compile"] end subgraph Boundary["Proof boundary"] Drilldown["Drilldowns tour, status, explain, observe, compile, serve"] Result record["Result records and route refs public refs only; body_in_receipt false"] end Project --> First First --> Route Route --> Ceiling Route --> Branch Branch --> Safety Branch --> Hiring Branch --> Developer Safety --> Drilldown Hiring --> Drilldown Developer --> Drilldown Ceiling --> Result record Drilldown --> Result record

Reader Evidence Routing

Start with core/paper_module_capsules.json::paper_modules[13:paper_module.cold_reader_route_map], then read the generated JSON projection for the resolved relationships. A diagram view is generated for this module and an atlas card entry is available. The route-map fixture, exported bundle, source-module manifests, and temporary result records are evidence for replay shape. This Markdown gives cold readers the interpretation order, source-linked only.

Prior Art Grounding

This component is grounded in documentation systems that treat reader state and task shape as first-class. Diataxis separates tutorials, how-to guides, reference, and explanation so readers are not forced through one undifferentiated documentation pile. Knuth's literate programming is an older anchor for the idea that executable systems should be written for human comprehension as well as machine execution.

Microcosm borrows the reader-route pattern: first command, result record ref, evidence class, scope boundary, scope limit, and next drilldown are ordered for a cold reader. It does not make the route map source authority or substitute documentation sequence for validator evidence.

Reader-Specific Evidence Routing

The route map should make the evidence-count frame visible before the reader chooses a drilldown. Honest counters are not progress badges:

• A safety/evals engineer follows microcosm status --card, microcosm authority --card, and microcosm workingness --card first. The useful question is whether each claim names its evidence class, validator, failure mode, and scope limit.
• A hiring reviewer follows the first-screen card and legibility scorecard first. The useful question is whether small verified counts are framed as honest proof boundaries instead of hidden or inflated.
• A peer developer follows microcosm tour --card, microcosm observe --card, and then full microcosm observe, microcosm compile, or microcosm explain as drilldowns. The useful question is whether a fresh clone can reproduce the route/work/event/evidence chain locally without opening full event rows first.

The route map must therefore preserve both the command order and the evidence interpretation order: command, result record ref, evidence class, scope boundary, scope limit, then deeper route. Reader-specific branches may hide other branches, but they may not hide the accounting frame that prevents "1 verified import" from being read as either failure or marketing.

One-Screen Handoff Contract

The route map consumes the first-screen card as the handoff, not as another route row. A cold reader should see this sequence:

1. First-screen card: claim frame, microcosm hello <project>, shared proof, evidence legend, structural join, reader rail, and exit rule.
2. Route map: the accepted command order, with result record refs and scope limits attached to each command.
3. Reader branch: one audience-specific first action, one proof surface, one success criterion, and one next drilldown.

The handoff fails when the first screen turns into a complete route inventory, or when the route map assumes the reader already understands evidence classes. The first screen should compress; the route map should sequence; the reveal should demonstrate the path against public result records.

Comparison-Backed Route Rows

Each route row should make the unusual discipline visible by naming the normal failure mode it is avoiding. The route map is not just a command list; it is a sequence of claim-boundary checks:

Rows that omit the comparison cue are still technically navigable, but they make the rigor invisible to a cold reader. The validator should prefer a shorter row with command, result record, class, scope boundary, and failure mode over a longer row that lists more components without explaining what each boundary prevents.

Observable Drilldown Order

Browser-first readers follow the same route map as terminal-first readers. The route order is compressed, not replaced:

1. First-screen card or compact browser board.
2. microcosm tour --card <project> as the shared behavior proof.
3. Selected route plus work/event/evidence refs.
4. Compact observatory view for the same route.
5. Full route map, result records, standards, and raw JSON drilldowns.

The compact observatory row must carry the same command ref, result record ref, evidence class, scope boundary, and scope limit as the terminal route row. If the browser board cannot show those fields, it is a preview only and cannot serve as the cold-reader route handoff.

readme_onboarding_route is the selected route only for projects with a README; folders without one still get a route/work/event/evidence path through the selected route emitted by tour and compile.

Each route card must include a command and public docs refs. Each route id must also resolve to at least one result record ref. The sequence must be ordinal sorted so the public entry does not drift into a bag of impressive but unordered components.

Validation

The fixture observes negative cases for missing command refs, missing result record refs, route sequence gaps, launch/provider overclaims, and private source body fields. The exported bundle omits negative cases and validates the real runtime shape used by microcosm run, with synthetic result record stand-ins explicitly disallowed as product evidence. If focused validation reports an exact-copy source-module body mismatch, route that repair through microcosm_exact_copy_refresh; do not treat this Markdown projection as the authority for copied source bodies.

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary result records:

The focused pytest file is the proof consumer for this Markdown section. It asserts the fixture status, ten-route command and result record-ref counts, front-door route order, expected negative cases, route-source replay support, exported bundle shape, copied source-module digest and anchor matches, source-open fixture-manifest counts, no source bodies in public result records, streamed line-count and digest handling, and fresh exported-bundle card reuse. The corpus check verifies that this page remains in the 98-module paper-module set and that the JSON bundle, generated Mermaid, Atlas card, and Markdown projection stay mutually consistent.

These result records validate the route-map fixture, exported bundle result records, copied cold-entry evidence, and paper-module corpus membership only; they do not grant route registry control, external model service, source-file changes, launch-scope decision, private-data equivalence, financial decisions, publishing-scope decision, hosted readiness, or whole-system correctness.

public_reveal_walkthrough is the accepted component that makes Microcosm's public reveal executable instead of descriptive.

It validates a ten-minute cold-reader path:

1. Compile a project into .microcosm/.
2. Inspect catalog, patterns, and routes.
3. Explain one route through patterns, standard pressure, work, events, and evidence.
4. Open the observatory causal chain before raw JSON drilldown.
5. Run microcosm intake to see the source projection intake cells connected to spine, reveal, and runtime evidence.
6. Read the result records and scope limit.

The component reads public fixtures from fixtures/first_wave/public_reveal_walkthrough/input/ and exported runtime input from examples/public_reveal_walkthrough/exported_public_reveal_bundle/.

It emits:

• receipts/first_wave/public_reveal_walkthrough/public_reveal_walkthrough_result.json
• receipts/first_wave/public_reveal_walkthrough/ten_minute_reveal_board.json
• receipts/first_wave/public_reveal_walkthrough/public_reveal_validation_receipt.json
• result records/sign-off/first_wave/public_reveal_walkthrough_fixture_acceptance.json

The reveal path treats microcosm intake as a runtime bridge rather than a private planning note. The command exposes runtime_reveal_import_bridge, keeps formal_math_readiness_extensions visible as a public replacement when its extension board exists, and points back to the source projection intake board without copying private source bodies.

Purpose

A cold reader meeting Microcosm for the first time needs one thing the README cannot give them on its own: proof that the first ten minutes are real and not a tour of screenshots. This component answers a single question. Can a reader who has never seen the system run a short, fixed path from a command to local state, to a route, to the result record and source boundary behind it, with nothing on that path that the system does not actually run?

The validator enforces that path as an accounting floor rather than a narrative. A reveal only passes if it carries at least five steps, four distinct runnable commands, and four evidence refs, and if four overclaim fixtures stay rejected: a launch or hosting claim, a private-data equivalence claim, a step with no evidence ref, and marketing copy with no command behind it. The floor exists because a walkthrough drifts towards a hero pitch the moment it is allowed to. Removing the commands and the result record refs is the easiest way to make a reveal look more impressive and prove less.

The part worth noting is the real-lane witness. The fixture run does not pass on its own paperwork. It is gated on the exported reveal bundle actually running, with its copied source bodies present and digest-verified. If that backing run is missing or blocked, the fixture is marked blocked too, with real_runtime_receipt set to false. So the reveal cannot describe a runnable path while the runnable path is broken underneath it, which is the quiet failure mode of every quick-start guide that says more than it can execute.

Shape

Public Reveal Walkthrough is the source-backed entry membrane for a cold technical reader. It turns the local Microcosm first-run path into a runnable accounting exercise: commands produce local state, routes point at work and events, evidence refs point at result records, and scope limits keep the visual or browser layer from becoming a product or public-sharing claims.

flowchart TD Bundle["JSON bundle paper_module.public_reveal_walkthrough"] Fixture["First-wave public reveal fixture 10-minute route + negative cases"] Bundle["Exported public reveal bundle 5 copied source bodies"] Runtime["Runtime component public_reveal_walkthrough.py"] Shell["Runtime shell bridge microcosm intake + public reveal view"] Result records["metadata-only result records result, board, validation, sign-off"] Reader["Cold reader route command -> route -> evidence refs -> ceiling"] Ceiling["Scope limit no launch, hosting, provider, or private-system claims"] Bundle --> Runtime Fixture --> Runtime Bundle --> Runtime Runtime --> Result records Runtime --> Shell Shell --> Reader Result records --> Reader Reader --> Ceiling

The runtime shape has five bounded inputs:

• the public reveal fixture under fixtures/first_wave/public_reveal_walkthrough/input;
• the exported reveal bundle under examples/public_reveal_walkthrough/exported_public_reveal_bundle;
• the source-module manifest for copied source bodies;
• the component source and focused tests that enforce command, evidence, and negative-case behavior;
• the standard and JSON bundle that bind the paper module to the mechanism, source locus, and scope limit.

The proof shape is route-first rather than dashboard-first. A valid reveal shows a command, a selected route, the route explanation through work/events/ evidence, result record refs, evidence-class counts, and the scope boundary beside any impressive total. Generated cards, observatory views, and browser/video boards are presentation layers over that accounting path.

The negative-case shape is part of the floor. launch or hosting overclaims, private-data equivalence, missing evidence refs, and marketing-only reveal material must remain rejected. If those refusals stop appearing, the reveal is no longer bounded enough for a cold reader.

The source-open shape is also bounded. The exported bundle carries five copied public bodies, and the manifest verifies exact-copy relation, digests, material classes, and metadata-only result records.

Evidence/accounting:

• Bundle authority: core/paper_module_capsules.json::paper_modules[paper_module.public_reveal_walkthrough] sets source_authority: json_capsule, binds the component, binds mechanism.public_reveal_walkthrough.validates_public_reveal_walkthrough, and resolves src/microcosm_core/organs/public_reveal_walkthrough.py.
• Generated instance: paper_modules/public_reveal_walkthrough.json reports source_authority: json_capsule, Mermaid available_from_capsule_edges, Atlas linked_from_capsule_edges_after_atlas_binding, 20 relationship edges, and a resolved paper_module.depends_on.paper_module edge to paper_module.first_screen_composition_root because the reveal path spends the first-screen composition contract before deeper route/evidence drilldown.
• Runtime and shell consumers: src/microcosm_core/organs/public_reveal_walkthrough.py exposes run, run_reveal_bundle, _source_module_manifest_result, _source_open_body_import_summary, EXPECTED_NEGATIVE_CASES, AUTHORITY_CEILING, and PUBLIC_SAFE_SOURCE_BODY_CLASSES. src/microcosm_core/runtime_shell.py routes the exported reveal bundle through public_reveal_walkthrough.run_reveal_bundle and publishes the public_reveal_view runtime lens.
• Result record and test floor: receipts/first_wave/public_reveal_walkthrough/public_reveal_walkthrough_result.json, ten_minute_reveal_board.json, public_reveal_validation_receipt.json, and result records/sign-off/first_wave/public_reveal_walkthrough_fixture_acceptance.json are metadata-only evidence. tests/test_public_reveal_walkthrough.py checks the fixture path, exported-bundle path, source-module digest validation, negative cases, and public-relative result record posture.
• Claim boundary: standards/std_microcosm_public_reveal_walkthrough.json, the generated structured source record, and this page limit the module to public reveal walkability, route/evidence accounting, exact-copy public source-body import evidence, negative-case rejection, and metadata-only result records. They do not include launch operations, hosted deployment, public sharing, recipient work, external model access, secret export, private-system equivalence, source-file changes, Lean/Lake execution, or whole-system correctness.

Source-Backed Mechanism

The source mechanism is mechanism.public_reveal_walkthrough.validates_public_reveal_walkthrough in core/mechanism_sources.json.

The runtime locus is src/microcosm_core/organs/public_reveal_walkthrough.py. The source symbols that matter for cold-agent drilldown are:

• run
• run_reveal_bundle
• _source_module_manifest_result
• _source_open_body_import_summary
• EXPECTED_NEGATIVE_CASES
• AUTHORITY_CEILING
• PUBLIC_SAFE_SOURCE_BODY_CLASSES

The governing standard is standards/std_microcosm_public_reveal_walkthrough.json. Its paper_module_contract binds this Markdown module to core/paper_module_capsules.json#paper_module.public_reveal_walkthrough and to the mechanism row above.

The atlas source row is intentionally not claimed as complete in this pass: core/organ_atlas.json is the source surface that must later receive paper_module_ref, mechanism_refs, and code_loci for this component. The re-entry capture is cap_quick_public_reveal_atlas_edge_population_wait_147e39c7a896.

Source-Open Body Imports

The exported reveal bundle carries five copied source bodies under examples/public_reveal_walkthrough/exported_public_reveal_bundle/source_modules/. The authority manifest is examples/public_reveal_walkthrough/exported_public_reveal_bundle/source_module_manifest.json.

The copied materials are:

All five rows are exact-copy imports, body_in_receipt=false, and digest checks must pass before the exported reveal bundle can count as source-backed. Result records may name refs, hashes, counts, and verdicts; they do not embed copied body text.

First Commands

From microcosm-substrate/, the first fixture command is:

The exported bundle command is:

PYTHONPATH=src python3 -m microcosm_core.organs.public_reveal_walkthrough run-reveal-bundle --input examples/public_reveal_walkthrough/exported_public_reveal_bundle --out receipts/runtime_shell/demo_project/organs/public_reveal_walkthrough --card

Focused regression:

PYTHONPATH=src ../repo-pytest tests/test_public_reveal_walkthrough.py -q --basetemp=/tmp/microcosm-public-reveal-pytest --ignore-host-pressure

Evidence Counts In The Reveal

The reveal board should not ask a cold reader to decode evidence-class numbers from context. When the walkthrough shows source-open body material counts, verified import counts, subprocess witnesses, algorithmic projection counts, or rows with source imports, it should pair each number with the evidence class and the scope boundary:

• Counts prove that the public route exposes an inspectable accounting surface.
• Counts do not prove launch-scope decision, whole-system correctness, or equal evidence depth across every component.
• A small high-authority count is stronger than a large low-authority count for the claim it actually covers.
• Generated or projected rows are reveal handles; source files, validators, result records, and scope limits remain the proof surfaces.

This keeps the public reveal from becoming a dashboard of impressive totals. The first reveal task is to show how a reader can move from number to result record to source boundary without crossing into private bodies, model-output data, account or browser state, or launch claims.

Reveal First View

The reveal board should open with the same compression grammar as the first-screen card, then widen only after the reader has a route to inspect:

1. Restate the bounded claim frame.
2. Show the command that produced the local state.
3. Show one route explanation with result record refs.
4. Show the evidence-count legend beside the result record refs.
5. Show the scope limit before any totals, drilldowns, or observatory links.

This gives video-first or browser-first readers a visible artifact without turning the reveal into a marketing hero. Motion, screenshots, and observatory views are allowed presentation layers only when the same evidence legend, scope boundary, and result record refs remain on the first view.

Discipline In The Reveal

The reveal should make discipline legible as prevented failure, not as a wall of policy labels. Before showing totals or motion, the board should pair each impressive-looking artifact with the boundary that keeps it honest:

If the reveal cannot show those boundaries on the first view, it should defer the visual flourish and keep the compact result record-backed route visible instead.

Prior Art Grounding

The public reveal path is grounded in first-run CLI and progressive-disclosure practice. The Command Line Interface Guidelines motivate a single runnable command, examples, discoverable next steps, and machine-readable output. Nielsen Norman Group's progressive disclosure pattern motivates showing the bounded first route before expanding into full observatory or JSON drilldowns.

The reveal's evidence walk also borrows from provenance and tracing patterns: W3C PROV for moving from artifact to source and result record, and OpenTelemetry traces for representing causal chains as inspectable linked work. Microcosm applies those patterns to a local walkthrough so the visual board remains evidence accounting, not a launch or maturity claim.

Browser/Video Reveal Board

The reveal board is the public visual candidate for a 60-second walkthrough. It must therefore be more than raw JSON, but it must still be less than a product claim. The first browser/video frame should show:

1. The command that produced the local state.
2. The selected route and one-line route reason.
3. The route explanation through work, events, evidence, and result record refs.
4. The evidence legend, including evidence class and scope boundary.
5. The compact observatory or first-screen endpoint used for the board.
6. The scope limit before totals, motion, or full-model drilldown.

Motion is allowed to make the causal order easier to inspect: command to local state, local state to selected route, selected route to work/event/evidence, and evidence to result record or validator. Motion is not allowed to displace the command, result record/evidence ref, scope boundary, or scope limit from the first view.

The board should end by offering exactly three next steps: reader-specific branch, result record drilldown, and full observatory JSON. That keeps the visual surface from expanding into a second README while still making the public reveal inspectable by readers who will not start in the terminal.

The validated claim is narrow:

> Microcosm turns a repo into a local operating system: patterns, routes, > work transactions, events, evidence, and explanations.

Negative fixtures reject launch or hosting overclaim, private-data equivalence, missing evidence refs, and marketing-only reveal material without runtime commands.

Reader Evidence Routing

• Start with the first commands and the JSON Bundle Binding to identify the fixture, exported bundle, source record, mechanism row, standard, and result record surfaces.
• For behavior questions, read src/microcosm_core/organs/public_reveal_walkthrough.py and tests/test_public_reveal_walkthrough.py before trusting this prose.
• For source-open body questions, read the exported bundle's source_module_manifest.json; it is the evidence for exact-copy relation, digest match, material class, and metadata-only result record posture.
• For visual or browser walkthrough questions, read the evidence legend, result record refs, scope boundary, and scope limit before reading totals, observatory links, or motion as meaningful.
• Treat generated atlas docs, generated coverage projections, generated result records, copied-body presence, and browser/video boards as navigation or validation projections. They do not become source authority for launch, hosting, provider, private-system-equivalence, or whole-system claims.

Validation Result record Path

PYTHONPATH=src ./repo-pytest tests/test_public_reveal_walkthrough.py -q --basetemp=/tmp/microcosm_public_reveal_walkthrough_pytest --ignore-host-pressure
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

Teleology

pattern_binding_contract is the public root component that binds pattern rows to source-available source bundles, public runtime refs, authority-chain handles, scope boundaries, and secret-exclusion result records. Synthetic rows are allowed only as regression controls or negative cases; they are not product evidence.

Purpose

A mined engineering pattern is a tempting thing to publish on its own. It reads like a self-contained insight, so it is easy to lift a single row out of a private ledger and present it as a finished public claim. This component exists to stop that. It answers one question: can a given pattern row be admitted to the public surface, and if so, under exactly what evidence and what ceiling?

The check is binding rather than display. Every pattern row must name a source bundle that points at a real public runtime ref or regression-harness ref, a governing standard, and an scope boundary. A row that lacks any of these, duplicates another row's id, or claims to be a standalone public leaf is rejected. The same validator runs deliberate negative cases alongside the positive control, so the result record proves not only that good rows pass but that each known failure mode is still caught.

The less obvious idea is truth accounting. When an exported bundle is validated, the component separates rows that merely describe runtime metadata from rows that represent a real pattern-ledger import, and records that a high accepted-row count is not the same as system progress. This guards against the quiet inflation where counting accepted rows starts to read like a measure of how much real work has landed. The route-readiness layer closes the matching gap on the selector side: a row can look selectable in isolation, but it is only admitted through the component that owns it, its fixture contract, and a gate that refuses to let hard no-standalone rows appear as selectable targets.

Public Contract

The validator checks required binding fields, duplicate pattern conflicts, unsupported authority-chain handles, unresolved reference bundles, secret/provider/operator body sentinels, and public-leaf overclaim failures. It emits command-owned result records under receipts/first_wave/pattern_binding_contract/.

The exported system bundle also carries the source route-readiness selector overlays as public source-open bodies: examples/pattern_binding_contract/exported_route_readiness_bundle/. The validator recomputes the selector contract against the imported pattern ledger, route-readiness audit, row-to-component router, route cards, fixture specs, decision matrix, dependency DAG, internal routing graph, and copied source validation report. This closes the old gap where a mined pattern row could look selectable without opening the component bundle that owns it.

Cold readers should use microcosm pattern-route-readiness validate-bundle against examples/pattern_binding_contract/exported_route_readiness_bundle/ when the question is selector admission rather than generic pattern binding. The older pattern-binding validate-route-readiness-bundle action remains a compatibility route to the same validator.

Shape

flowchart LR subgraph Inputs["Pattern-binding inputs"] Patterns["Pattern rows id, governing standard, scope boundary, source refs, projection posture"] Bundles["Source bundles metadata-only refs to public runtime or regression harness"] Handles["Authority-chain handles resolver result records"] end Validator["pattern_binding_contract required fields, duplicate ids, bundle resolution, secret-exclusion scan"] subgraph Negative["Refusal floor"] Dup["Duplicate id rejected"] Leak["Private body leak rejected"] Overclaim["Public-leaf overclaim rejected"] Unsupported["Unsupported authority handle not upgraded"] end subgraph Bundle["Exported-bundle path"] Truth["Truth accounting runtime-metadata rows vs real pattern-ledger import"] RouteReadiness["Route-readiness selector component-first admission, fixture contract, hard no-standalone gate"] end Result records["Result records refs, digests, counts, verdicts; body text omitted"] Patterns --> Validator Bundles --> Validator Handles --> Validator Validator --> Negative Validator --> Bundle Truth --> RouteReadiness Negative --> Result records Bundle --> Result records

Evidence Binding

Accepted component row: core/organ_registry.json::implemented_organs[pattern_binding_contract]. Evidence class: core/organ_evidence_classes.json::organ_evidence_classes[pattern_binding_contract] with rank 5 semantic-validator authority. The runtime locus is src/microcosm_core/organs/pattern_binding_contract.py, with focused coverage in tests/test_pattern_binding_contract.py.

Paper bundle authority: core/paper_module_capsules.json#paper_module.pattern_binding_contract. Mechanism source: core/mechanism_sources.json#mechanism.pattern_binding_contract.validates_public_pattern_bindings.

Reader Evidence Routing

Read this module as a public binding membrane for pattern rows, not as a private pattern-ledger certificate or a standalone public-leaf selector. Start with paper_modules/pattern_binding_contract.json for the bundle payload, then open standards/std_microcosm_pattern_binding_contract.json to check the required fields, public/private boundary, source-open body import floor, route-readiness rules, and result record expectations.

Use core/fixture_manifests/pattern_binding_contract.fixture_manifest.json before inspecting fixtures or exported bundles. The manifest and the source_module_manifest.json files name the copied source body floor; result record payloads should carry source refs, digests, anchors, counts, verdicts, and omission result records rather than inlining body text.

Treat route-readiness selection as component-first evidence. A mined pattern row can be selectable only through the route-readiness bundle, selector contract, and result records that keep duplicates, unknown refs, private leakage, missing fixture contracts, dependency cycles, hard no-standalone rows, and companion-overlay gaps rejected.

Prior Art Grounding

This component follows the software pattern-language tradition of making reusable engineering structures explicit, named, and reviewable. The Hillside patterns library is the direct prior-art family for treating patterns as shared vocabulary rather than loose implementation notes.

The binding layer also borrows from provenance and supply-chain attestation patterns. W3C PROV motivates the source/ref/evidence relation shape, while SLSA and in-toto motivate digest-bound artifact claims and step-level metadata. Microcosm applies those ideas to pattern rows and route-readiness selectors, not to launch certification.

Re-entry condition: if copied source bodies, route-readiness overlays, or negative-case rules change, rerun the three first commands above and update this paper module plus standards/std_microcosm_pattern_binding_contract.json from the new result record fields. Do not raise the scope limit from selector and binding validation to launch, public sharing, private-data equivalence, or standalone public-leaf authority.

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary result records:

These checks validate public pattern-binding fixtures, system-bundle result records, route-readiness selector result records, and metadata-only authority handles only; they do not certify the private pattern ledger, hosted readiness, launch, external model access, private-data equivalence, or whole-system correctness.

The current authority is the runtime result record set under receipts/first_wave/pattern_binding_contract/; do not cite a separate pattern-specific sign-off result record unless an sign-off-lane artifact is actually present. Cold readers should inspect result record fields rather than markdown constants: status, secret_exclusion_scan, source_open_body_imports, truth_accounting, route_readiness_summary, selection_contract, and source_manifest.

pattern_assimilation_step is the public completion-learning contract for landed components. It validates that every component recorded as landed in a fixture set carries exactly one same-lane completion decision, and that the decision resolves to a result record that can be inspected rather than to a phrase.

Purpose

When a development pass claims that local work taught the system something, that claim is usually prose: a note that the run "improved the fixture" or "found nothing to refine". Prose is easy to assert and impossible to check. This component answers a single question: did each landed component actually deposit an inspectable completion decision, or is the learning claim unbacked?

The decision is forced into one of two typed shapes. Either a concrete refinement result record that names the owner surface it changed and the artifact it touched, or a typed nothing_to_refine result record that proves stewardship was checked, the next-best lane was considered, and a re-entry condition was recorded. A landed component with no completion, or with a completion that points at a result record that does not exist or does not match, is rejected. So is a duplicate result record id that would let one lesson be counted twice.

The interesting constraint is the one the component refuses to relax. A local lesson may route to the owner surface that owns the affected artifact, but it may not promote itself into global doctrine. A refinement row that sets claims_global_doctrine_authority is blocked outright. The point is that learning has to land on a specific board with a named steward, not become a free-floating rule, which is the failure mode that turns a useful local note into unsupported general advice.

Route Card

• Component id: pattern_assimilation_step
• JSON bundle authority: core/paper_module_capsules.json::paper_module.pattern_assimilation
• Accepted-component evidence class: semantic_validator
• Standard: standards/std_microcosm_pattern_assimilation_step.json
• Validator authority: src/microcosm_core/validators/sign-off.py
• Fixture manifest: core/fixture_manifests/pattern_assimilation_step.fixture_manifest.json
• Fixture input: fixtures/first_wave/pattern_assimilation_step/input
• Runtime bundle: examples/pattern_assimilation_step/exported_assimilation_bundle
• Primary result records: receipts/first_wave/pattern_assimilation_acceptance.json, receipts/first_wave/pattern_assimilation_receipt.json, and receipts/first_wave/pattern_assimilation_step/exported_assimilation_bundle_validation_result.json
• Projection posture: the JSON bundle is the paper-module source authority. This Markdown is the cold-reader explanation.

Shape

flowchart TD landings["Landed component rows organ_landing_summaries.jsonl each names a completion result and result record ref"] refinement["Refinement result records owner_surface, changed artifact"] nothing["Nothing-to-refine result records stewardship, next-best lane, re-entry"] validator["sign-off.py validate_pattern_assimilation"] filter["Pre-filter valid result records refinement: named owner, no doctrine upgrade nothing: all three fields present"] match{"Per landed component: exactly one completion, ref resolves to a matching row?"} pass["Accepted typed, owner-routed completion learning"] negatives["Negative cases recorded MISSING_PATTERN_ASSIMILATION_Completion MISSING_REFINEMENT_OWNER_SURFACE DUPLICATE_REFINEMENT_RECEIPT_ID LOCAL_LESSON_AUTHORITY_UPGRADE RAW_SEED_BODY_IN_ASSIMILATION_FIXTURE"] result records["metadata-only result records result records/first_wave/pattern_assimilation_*"] ceiling["Scope limit public fixture metadata, no doctrine changes"] landings --> match refinement --> filter nothing --> filter filter --> match validator --> filter match -->|resolved| pass match -->|missing, dangling, duplicate, upgraded| negatives pass --> result records negatives --> result records result records --> ceiling

The bundle is present, so the cold-reader path starts from core/paper_module_capsules.json::paper_module.pattern_assimilation, not from a legacy-only boundary. That bundle binds this Markdown to the accepted pattern_assimilation_step component, the sign-off.py validator locus, the standard, first-wave fixture manifest, exported assimilation bundle, focused tests, metadata-only result records, and generated Mermaid/Atlas navigation status.

Read the diagram as the validation flow, not an authority upgrade. The validator pre-filters the refinement and nothing-to-refine result records, then walks each landed component row and checks that its declared completion resolves to a matching valid result record; unresolved, missing, duplicate, or doctrine-upgraded rows become recorded negative cases. The ceiling remains public fixture and exported-bundle metadata plus metadata-only result records, with no live ledger mutation, source-file changes, source note ingestion, private-system equivalence, global doctrine changes, launch or publishing-scope decision, behavior-change proof, or whole-system correctness.

First Command

From microcosm-substrate:

Use the exported bundle validator when the question is whether the public source-open body imports still match their declared source bodies:

What It Proves

Pattern assimilation is the public completion-learning contract for landed components. It validates that each landed component in the fixture set has exactly one same-lane completion decision: either a concrete refinement result record naming the owner surface and changed artifact, or a typed nothing_to_refine result record with stewardship checked, next-best-lane checked, and a re-entry condition.

A cold agent should use this component when a pass claims that local work taught the system something. The validator makes that claim inspectable: it checks owner-surface evidence, duplicate result record ids, off-lane completions, missing completion decisions, residual lifecycle posture, and attempts to promote a local lesson into global doctrine authority without the governing lane.

Bundle-Bound Reader Shape

The paper-module bundle binds this Markdown to two explained subjects: pattern_assimilation_step and mechanism.pattern_assimilation_step.validates_public_pattern_assimilation_step. It also carries the route-contract concept concept.architecture_and_navigation_route_contract_bundle.

The executable locus is src/microcosm_core/validators/sign-off.py, specifically validate_pattern_assimilation, run_assimilation_bundle, validate_source_module_manifest, _write_jsonl_upsert, EXPECTED_NEGATIVE_CASES, PATTERN_ASSIMILATION_AUTHORITY_CEILING, and main.

Its law edges are bounded to the local completion-learning scope limit: P-1, P-2, P-3, P-5, P-6, P-7, P-8, P-9, P-12, P-13, P-15, AX-1, AX-4, AX-5, AX-6, AX-7, AX-8, AX-11, and AX-12. Its paper-module neighbors are cold_reader_route_map, pattern_binding_contract, and voice_to_doctrine_self_improvement_loop.

If the generated JSON instance disagrees with the bundle or validator source, the bundle and validator win; refresh the projection rather than editing it.

Source-Backed System

This component is more than a prose rule. The exported assimilation bundle imports four bodies by manifest:

• macro_pattern_autonomy_process_contract_body_import from state/microcosm_portfolio/reconstruction/macro_pattern_autonomy_process_contract_v1.json
• macro_pattern_assimilation_fixture_manifest_body_import from state/microcosm_portfolio/reconstruction/fixture_manifests/pattern_assimilation_step.fixture_manifest.json
• pattern_assimilation_retracted_adapter_receipt_body_import from state/microcosm_portfolio/reconstruction/pattern_assimilation_step_real_substrate_adapter_receipt_v1.json
• pattern_assimilation_acceptance_validator_source_body_import from src/microcosm_core/validators/sign-off.py

The manifest is examples/pattern_assimilation_step/exported_assimilation_bundle/source_module_manifest.json. It must keep body_in_receipt: false, exact source and target digests, required anchors, and validation refs. The copied validator body anchors validate_pattern_assimilation, run_assimilation_bundle, and PATTERN_ASSIMILATION_AUTHORITY_CEILING.

Result record Floor

A passing fixture run emits:

• receipts/first_wave/pattern_assimilation_acceptance.json
• receipts/first_wave/pattern_assimilation_receipt.json
• state/microcosm_portfolio/reconstruction/macro_pattern_autonomy_process_runs_v1.jsonl

A passing exported-bundle run emits:

• receipts/first_wave/pattern_assimilation_step/exported_assimilation_bundle_validation_result.json

The first-wave result records must include public-relative paths, no private root paths, no copied body text, a redacted non-public-state scan with zero blocking hits, observed negative cases, error codes, scope limit, scope boundary, and the exact result record paths. The bundle result record must show source_module_manifest_status: pass, body_copied_material_count: 4, the four body-material ids above, body_in_receipt: false, body_text_in_receipt: false, and only public replacement refs.

Reader Evidence Routing

A cold reader should inspect the evidence in this order:

1. Open the JSON source record to confirm subject ids, dependency ids, principle and axiom refs, and code locus.
2. Run the focused sign-off test or fixture command to prove the completion learning shape still accepts valid fixture rows and rejects the required negative cases.
3. Run the exported bundle validator when source-module digest, anchor, copied body, or replacement posture is the question.
4. Treat generated JSON, Mermaid, Atlas, and coverage as projection evidence only; if they drift, refresh them through the doctrine-lattice builder.
5. Use the result record floor to check public-relative paths, metadata-only source verification, source note exclusion, and local-lesson scope limits.

Negative Cases

The current negative-case floor is:

• MISSING_PATTERN_ASSIMILATION_CLOSEOUT for a landed component without a refinement or typed no-op completion.
• MISSING_REFINEMENT_OWNER_SURFACE, MISSING_STEWARDSHIP_CHECK, and MISSING_REENTRY_CONDITION for refinement result records that cannot route the lesson to an owner surface and re-entry condition.
• DUPLICATE_REFINEMENT_RECEIPT_ID for duplicate refinement result records.
• LOCAL_LESSON_AUTHORITY_UPGRADE for local lessons that claim global doctrine authority.
• RAW_SEED_BODY_IN_ASSIMILATION_FIXTURE for source notes or private source note bodies in the public fixture.
• ASSIMILATION_BUNDLE_SOURCE_MODULE_INVALID for exported source-module digest or anchor mismatch.

These are not ornamental checks. If a run stops observing them, the module can no longer support the claim that Microcosm learns from landed work without turning local notes into unsupported global doctrine.

Prior Art Grounding

Pattern assimilation is grounded in software pattern-language practice: recurring engineering lessons should be named, bounded, reviewed, and connected to the context where they apply. The Hillside patterns library is the direct prior-art family for treating patterns as a shared engineering vocabulary rather than one-off notes.

The result record and trace shape also borrows from provenance and observability practice. W3C PROV informs the requirement that each refinement cite its owner surface and evidence relation, while OpenTelemetry traces are a useful analogue for linking spans of work into an inspectable causal chain. Microcosm uses those inspirations for completion learning only; a local lesson still needs the owning lane before it can become broader doctrine.

Validation Result record Path

From microcosm-substrate, keep validation result records outside tracked first-wave paths unless the owning result record lane intends to refresh them:

The fixture and bundle result records prove same-lane completion-learning shape over the public fixtures and copied body imports only; they do not promote a local lesson to global doctrine authority. Source-copy or result record drift is an owning validator/manifest lane issue, not Markdown source authority.

Focused pytest re-entry is:

PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider tests/test_pattern_assimilation_step.py -q --basetemp=/tmp/microcosm_pattern_assimilation_pytest

Use an isolated /tmp basetemp for focused pytest runs so result record scratch paths do not rewrite source-run rows inside the checkout.

Validation Anchors

Focused coverage lives in tests/test_pattern_assimilation_step.py and checks:

• streamed JSONL loading and upsert behavior;
• required negative-case observation;
• public-relative redacted result records;
• source result record field floors from the fixture manifest;
• exported assimilation bundle runtime shape;
• source-module digest mismatch rejection;
• exported bundle result records;
• exact copied source body imports.

Purpose

Doctrine in most systems is prose convention. A standard says a rule should hold, a paper module says a section should be present, and nothing checks whether the claim is actually true. This component exists to make doctrine shape a thing a program can pass or fail. It answers one question: does a standard row or a paper-module fixture carry the structure that doctrine here requires, or is it just text that looks the part?

What it checks is deliberately structural rather than semantic. A standard row must declare a teleology, a governing standard, result record expectations, and an scope boundary. A paper module must carry the matching sections by heading. The validator does not judge whether the prose is good. It judges whether the load-bearing fields are present, so a row cannot quietly drop its result record expectations or its scope boundary and still pass.

The less obvious part is that the failures are first-class. Five negative cases are part of the contract: a row missing its required fields, a prose-only standard that tries to claim executable authority, a source doctrine body copied into a public fixture, a duplicate standard slug, and a grammar pass that overclaims doctrine completeness. A run that does not observe each of these classes is blocked, so the checker is held to demonstrating that it can reject, not only that it can accept.

The component also imports copied source bodies, but only through a source-module manifest with declared SHA-256 digests, and never inlines a body into a result record. The result record reports refs, hashes, counts, and verdicts; the bodies live in the bundle. The point is to make the doctrine shape checkable without turning the public surface into an export of the private standards engine.

Teleology

executable_doctrine_grammar turns toy public standards and paper-module fixtures into deterministic grammar result records. It makes doctrine-shape claims checkable while importing copied, source bodies only through source-module manifests, digests, and result record boundaries.

Shape

flowchart TD A["Public doctrine fixtures fixtures/first_wave/executable_doctrine_grammar/input"] --> B["Executable grammar validator src/microcosm_core/components/executable_doctrine_grammar.py"] C["Exported standards bundle examples/executable_doctrine_grammar/exported_standards_bundle"] --> B D["Source-module manifest examples/executable_doctrine_grammar/exported_executable_grammar_metabolism_bundle/source_module_manifest.json"] --> B B --> E["metadata-only deterministic result records result records/first_wave/executable_doctrine_grammar/"] E --> F["Bundle and atlas evidence core/paper_module_capsules.json::paper_modules[18]"] F --> G["Bounded reader claim doctrine-shape validation, not launch-scope decision"]

Reader Evidence Routing

Reader evidence routes through the executable-grammar runtime, fixture inputs, exported standards bundle, executable-grammar metabolism bundle, source-module manifests, public result records, and focused tests. The Mermaid diagram and Atlas card are generated navigation projections; this page is the cold-reader explanation of the proof boundary.

Public Contract

The validator checks standard slugs, teleology, governing standard refs, result record expectations, scope boundaries, paper-module sections, source-body sentinels, duplicate slug conflicts, prose-only authority claims, and doctrine-completeness overclaims. It also validates the imported public executable-grammar specimen, standards registry, standards type-plane, lattice registry, kind-atlas runtime, and standards option-surface runtime as exact copied source modules.

Prior Art Grounding

This component is grounded in schema validation, parser generators, and executable semantics traditions. JSON Schema anchors the idea that document shape can be validated by a shared machine contract, Tree-sitter shows the practical value of generated grammars for inspectable source structure, and the K framework is a close reference point for turning semantic rules into executable artifacts.

Microcosm borrows the executable-contract pattern: doctrine shape, result record expectations, duplicate slugs, imported source bodies, and scope boundaries are checked by a validator instead of left as prose convention. It does not claim source doctrine completeness or launch-scope decision.

First Commands

From microcosm-substrate/, a cold agent can prove the fixture path:

PYTHONPATH=src python3 -m microcosm_core.organs.executable_doctrine_grammar validate --input fixtures/first_wave/executable_doctrine_grammar/input --out receipts/first_wave/executable_doctrine_grammar --card

The exported public standards bundle uses the same component with a narrower input:

PYTHONPATH=src python3 -m microcosm_core.organs.executable_doctrine_grammar validate-standards-bundle --input examples/executable_doctrine_grammar/exported_standards_bundle --out receipts/first_wave/executable_doctrine_grammar --card

The source-open source-body floor is the executable-grammar metabolism bundle:

PYTHONPATH=src python3 -m microcosm_core.organs.executable_doctrine_grammar validate-executable-grammar-metabolism-bundle --input examples/executable_doctrine_grammar/exported_executable_grammar_metabolism_bundle --out receipts/first_wave/executable_doctrine_grammar --card

Source-Backed Mechanism

The mechanism row mechanism.executable_doctrine_grammar.validates_public_doctrine_grammar_bundle points at validate, validate_standards_bundle, validate_executable_grammar_metabolism_bundle, validate_source_module_imports, validate_standard_registry, validate_paper_module_shape, result_card, EXPECTED_NEGATIVE_CASES, and GRAMMAR_AUTHORITY_CEILING.

Those symbols are the runnable floor:

• validate writes the fixture standards, paper-module, group-index, and sign-off result records.
• validate_standards_bundle validates the exported public standards bundle and keeps result record paths public-relative.
• validate_executable_grammar_metabolism_bundle validates the copied executable-grammar metabolism specimen, standards registry/type-plane, lattice registry, kind-atlas, and standards option-surface bodies.
• validate_source_module_imports requires source_module_manifest.json, copied_non_secret_macro_body, exact_copy, allowlisted source refs, body-in-result record exclusion, and SHA-256 digest matches.
• result_card compresses result record evidence without duplicating body text.

Negative Cases

The fixture must keep these failures executable rather than prose-only:

• invalid_standard_and_module: missing teleology, result record expectations, governing standard, and scope boundary.
• prose_standard_claims_runtime_authority: prose cannot claim executable runtime authority.
• macro_doctrine_body_copied_into_fixture: source doctrine body sentinels are rejected from public fixtures.
• duplicate_standard_slug_conflict: duplicate slugs are rejected deterministically.
• grammar_index_pass_overclaims_doctrine_complete: grammar pass is not doctrine-completeness authority.

Atlas Binding

• paper_module_ref: core/paper_module_capsules.json#paper_module.executable_doctrine_grammar
• mechanism_refs[].ref: mechanism.executable_doctrine_grammar.validates_public_doctrine_grammar_bundle
• code_loci[]: src/microcosm_core/organs/executable_doctrine_grammar.py with the mechanism symbols named above.

Validation Result record Path

./repo-pytest tests/test_executable_doctrine_grammar.py -q --basetemp=/tmp/microcosm_executable_doctrine_grammar_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

Purpose

A large codebase has a recurring failure: the agent or reader that lands in it starts from whatever browse surface is nearest to hand, treats that surface as the authority, and acts on a stale or partial view. The route plane exists to make the first move legible and to stop a browse row from being mistaken for the thing it describes. It answers one question: given a control entry, what is the safe ordered path into the browsable route projections, and what proof says that path is wired rather than asserted?

The unusual part is that the component never asserts a route is correct from prose. It treats every browse row as a projection and demands a coupling result record before that projection is allowed any authority. Source coupling is a plain SHA-256 over the route rows: the manifest carries an expected fingerprint and an expected row count, and if either disagrees with the rows on disk the projection is denied current authority. A route summary that claims to be current while its coupling is stale is rejected outright.

The other half of the design is what it refuses to do. First contact must begin at the control entry, not at a drilldown projection, so a request that tries to start from a browse row is replaced with the entry route. Compaction of the entry packet may not drop a required control field. An affordance row whose passport carries an anti-trigger is demoted before similarity search can ever select it. None of these are stylistic preferences; each is a named negative case the fixture must keep catching, so the route plane is defined as much by the eight things it blocks as by the path it permits.

Teleology

The navigation route plane gives a public clone a typed way to move from a control entry to browseable route projections without treating browse rows as authority.

Public Contract

The component runs in two modes against the same checks. The fixture mode loads a set of synthetic inputs, builds a toy option-surface from the rows (a cluster-flag summary plus one selected card), and then runs the negative-case validators that prove each guard still fires. The exported-bundle mode runs the same kind of checks against a real copied bundle: it validates the route rows, the source-coupling fingerprint, the source-module manifest, the route-lease policy, the entry-packet floor, the affordance passports, and the code-architecture projection packet, and only reports a pass when the secret scan is clean, a card row is selected, and every component validator passes.

The source-coupling gate is the spine. It hashes the route rows with SHA-256 and compares that against the fingerprint and row count declared in the manifest; a mismatch denies the projection any current authority, and a summary that claims current authority while coupling is stale is recorded as an overclaim. The source-module manifest names five exact copies of source route and control bodies. Each is checked by digest and by required navigation anchors, and each must declare that its body is copied but never written into the result record, so the evidence is reproducible without exposing the source text.

Shape

flowchart TD Entry["Control entry first browse row that claims first contact is replaced with the entry route"] subgraph Gates["Route-plane gates"] Couple["Source coupling SHA-256 over route rows vs manifest fingerprint + row count"] Rows["Route rows surface role, actionable command, no source-authority claim, omission result record when required"] Modules["Source-module manifest 5 copied source bodies digest + required anchors, body never in result record"] Lease["Route-lease policy selected lane, permitted actions, source authority rejected"] Floor["Entry-packet floor required control fields survive compaction"] Pass["Affordance passports anti-trigger rows demoted before similarity can select them"] end Verdict{"Coupling current, all gates pass, card row selected?"} Entry --> Couple Couple --> Rows --> Modules --> Lease --> Floor --> Pass --> Verdict Verdict -->|yes| Result records["metadata-only result records cluster flag, card, coupling, route lease, entry admission, affordance, code-architecture packet"] Verdict -->|no| Blocked["Blocked stable error codes, findings, bodies redacted"] Negative["Negative-case floor BANNED_FIRST_CONTACT_ROUTE, SOURCE_COUPLING_STALE, and 7 more"] -.-> Gates Result records --> Ceiling["Scope limit projection evidence only; no live route freshness, source authority, or launch"] Blocked --> Ceiling

Source-Backed Doctrine Packet

• core/organ_registry.json::implemented_organs[navigation_hologram_route_plane] is the accepted component authority. It records status accepted_current_authority, evidence class semantic_validator, evidence strength rank 5, scope limit validates declared public contract only, and validator command python -m microcosm_core.organs.navigation_hologram_route_plane run --input fixtures/first_wave/navigation_hologram_route_plane/input --out receipts/first_wave/navigation_hologram_route_plane.

• core/organ_atlas.json::organs[navigation_hologram_route_plane] gives the cold-reader gloss: control entry comes first, browse rows stay projections, eight route-plane negative cases are detected, exact copied navigation source modules validate, and result records omit body text.

• standards/std_microcosm_navigation_hologram_route_plane.json governs the standard authority boundary public_navigation_route_plane_runtime_and_copied_source_body_validator_not_live_source_authority. It requires route rows, option-surface contracts, source coupling, source-module manifests, route leases, entry-packet floors, affordance passports, code-architecture packets, body-import verification, scope limit, and scope boundary.

• src/microcosm_core/organs/navigation_hologram_route_plane.py is the runtime source for fixture validation, route-plane bundle validation, secret-exclusion scan, route-lease checks, entry-admission floor checks, affordance-passport demotion, code-architecture packet result records, and source-module digest/anchor validation.

• core/fixture_manifests/navigation_hologram_route_plane.fixture_manifest.json binds fixture expectations: body_copied_material_count=5, body_material_status=copied_non_secret_macro_route_substrate_with_provenance, body_in_receipt=false, and negative cases tied to stable error codes.

• examples/navigation_hologram_route_plane/exported_route_plane_bundle/source_module_manifest.json names five exact copied source route-control bodies: navigation_route_plane_intervention_source_body_import, navigation_route_plane_context_pack_source_body_import, navigation_route_plane_entry_packet_source_body_import, navigation_route_plane_option_surface_source_body_import, and navigation_route_plane_navigation_contract_source_body_import.

• tests/test_navigation_hologram_route_plane.py is the regression floor for fixture result records, exact source-source digest matches, source-module anchors, result record redaction, exported bundle validation, digest-mismatch rejection, and this source-backed paper-module packet.

• receipts/first_wave/navigation_hologram_route_plane/*.json carries public result records for cluster/card output, source coupling, route lease, entry-payload admission, affordance-passport selection, code-architecture packet, and exported bundle validation.

Source-module body floor:

Registry result record refs:

• receipts/first_wave/navigation_hologram_route_plane/affordance_passport_selection_receipt.json
• receipts/first_wave/navigation_hologram_route_plane/code_architecture_projection_packet_receipt.json
• receipts/first_wave/navigation_hologram_route_plane/entry_payload_admission_receipt.json
• receipts/first_wave/navigation_hologram_route_plane/route_lease.json
• receipts/first_wave/navigation_hologram_route_plane/source_coupling_result.json
• receipts/first_wave/navigation_hologram_route_plane/toy_kind_card.json
• receipts/first_wave/navigation_hologram_route_plane/toy_kind_cluster_flag.json

First command from microcosm-substrate/:

PYTHONPATH=src python3 -m microcosm_core.organs.navigation_hologram_route_plane run --input fixtures/first_wave/navigation_hologram_route_plane/input --out receipts/first_wave/navigation_hologram_route_plane

Runtime bundle command from microcosm-substrate/:

PYTHONPATH=src python3 -m microcosm_core.organs.navigation_hologram_route_plane validate-route-plane-bundle --input examples/navigation_hologram_route_plane/exported_route_plane_bundle --out receipts/runtime_shell/demo_project/organs/navigation_hologram_route_plane

Standard-declared runtime bundle validator: python -m microcosm_core.organs.navigation_hologram_route_plane validate-route-plane-bundle --input examples/navigation_hologram_route_plane/exported_route_plane_bundle --out receipts/runtime_shell/demo_project/organs/navigation_hologram_route_plane.

Atlas scope limit restated: It validates only the declared public toy route-plane contract and its regression fixtures (plus exact copied navigation source modules in the bundle path); it does not establish live route freshness, grant source authority, authorize any later component, run any provider/live-kernel call, or certify the whole wave.

The negative-case floor is part of the doctrine, not incidental test trivia. Across the eight negative cases, the fixture must keep detecting these stable error codes (one case carries two codes, so the list runs to nine):

• BANNED_FIRST_CONTACT_ROUTE
• SOURCE_COUPLING_STALE
• MISSING_OMISSION_RECEIPT
• ATLAS_PROJECTION_NOT_CONTROL_ENTRY
• ROUTE_CARD_PRIVATE_BODY_LEAK
• ROUTE_SUMMARY_OVERCLAIMS_FRESHNESS
• DUPLICATE_ROUTE_ID_CONFLICT
• ENTRY_ADMISSION_CONTROL_FLOOR_DROPPED
• AFFORDANCE_PASSPORT_ANTITRIGGER_IGNORED

Reader Evidence Routing

Reader evidence starts at the generated JSON instance, then routes through the route-plane runtime, fixture manifest, source-module manifest, public result records, and focused regression. The browse rows, Mermaid diagram, and Atlas card are derived projections; they are not control-entry or source authority.

Prior Art Grounding

The route plane is grounded in information-architecture and graph-navigation patterns. The first-contact rule follows the same usability pressure as progressive disclosure: show the control entry and immediate affordances before deeper browse rows. The CLI-facing surface is also informed by the Command Line Interface Guidelines, especially the emphasis on discoverable commands, examples, and clear next actions.

The graph side maps to established directed-graph tooling. NetworkX documents topological sorting as an ordering over dependency edges, and graph-ranking algorithms such as PageRank show the older pattern of computing route salience from graph structure. Microcosm keeps those ideas below authority: route cards, leases, and browse rows are projections unless source-coupling and entry-admission result records agree.

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary result records:

PYTHONPATH=src ../repo-python -m microcosm_core.organs.navigation_hologram_route_plane run --input fixtures/first_wave/navigation_hologram_route_plane/input --out /tmp/microcosm-navigation-hologram-route-plane
PYTHONPATH=src ../repo-python -m microcosm_core.organs.navigation_hologram_route_plane validate-route-plane-bundle --input examples/navigation_hologram_route_plane/exported_route_plane_bundle --out /tmp/microcosm-navigation-hologram-route-plane-bundle
../repo-pytest tests/test_navigation_hologram_route_plane.py
PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

These checks validate the public fixture and exported route-plane bundle only; they do not grant live route freshness, source authority, provider/live-kernel execution, later-component authorization, launch-scope decision, or whole-wave certification.

standards_meta_diagnostics is the terminal public coverage diagnostic for the Microcosm runtime spine. It checks that accepted adapter-backed components remain mapped to standards, runtime contracts, result records, and explicit scope limits before a cold reader trusts the spine as coherent.

It consumes public standards_inventory.json, organ_runtime_contracts.json, and diagnostic_policy.json inputs backed by registry refs, runtime commands, sign-off result records, and the exported diagnostics bundle. Its result record contract is source-open by default: secret_exclusion_scan proves that secrets, account or browser material, model-output data bodies, raw operator bodies, and account secret-equivalent live-access material are excluded, while public_runtime_refs point at the real standards, component, sign-off, fixture, bundle, and paper-module system. Bodies are not inlined into JSON result records, so the positive evidence uses body_in_receipt: false, real_runtime_receipt: true, and synthetic_receipt_standin_allowed: false.

The component rejects five boundary failures:

• accepted component rows without standard_id or standard_ref
• accepted components missing from the standards inventory
• accepted component rows without result record refs
• launch, provider, public sharing, secret export, trading/advice, or whole-system correctness overclaims
• private source bodies or model-output data bodies in public diagnostics

Purpose

A spine of accepted components is only coherent if each component is still attached to the things that make it accountable: a standard that describes it, a runtime contract that runs it, a result record that records its last verdict, and an explicit statement of what it is not allowed to claim. As the spine grows, those four attachments drift out of step one component at a time, and the drift is silent. A new component can be accepted into the runtime while its standard file, registry row, or result record ref is never added. Nothing breaks; the gap just sits there until a reader trusts the spine and finds a hole.

This component answers a single question: does every accepted component still resolve to a standard, a runtime contract, a result record, and an scope limit, with no extra and no missing entries? It treats the answer as a graph-closure check rather than a written audit. The accepted-component list, the standard rows, the runtime-contract rows, and the result record refs must agree on exactly the same set of components. Any component that appears in one surface but not another becomes a structured finding with a named error code, not a paragraph of prose.

The unusual choice is that the diagnostic refuses to grow its own authority. It projects its positive coverage from the live registry rather than a checked-in list, so a stale example cannot quietly become the thing the spine is measured against. It carries five negative fixtures that must each surface their expected failure, so the checker is itself falsifiable. And its result records deliberately hold refs, counts, hashes, and verdicts rather than the bodies they describe, so a coverage report can be read in the open without exporting private source.

Technical Mechanism

standards_meta_diagnostics is a public consistency validator over three finite surfaces: a standards inventory, component runtime contracts, and diagnostic policy. The positive path either reads those exported JSON inputs or projects them from the live public registry, then requires the accepted-component list, the standard rows, the runtime-contract rows, and the result record refs to agree on the same component set. This is a graph-closure check, not a narrative audit: an accepted component without a standard ref, registry-backed standard row, runtime step, validator command, or result record ref becomes a structured finding.

The mechanism has four guarded stages:

1. run loads standards_inventory.json, organ_runtime_contracts.json, and diagnostic_policy.json, or projects the positive rows from live public registry state when the caller asks for live positives.
2. The validator checks every accepted component row against a resolving std_microcosm_<organ_id> standard, the standards registry entry, the runtime shell step, a non-empty validator command, and non-empty result record refs with body_in_receipt: false.
3. Five negative fixtures exercise the expected boundary failures: missing_standard_ref, unmapped_accepted_organ, missing_receipt_ref, release_overclaim, and private_source_leakage.
4. The exported-bundle path revalidates the same shape through source_module_manifest.json, exact source-module digest checks, source-open body-import accounting, secret_exclusion_scan, and the projection-only AUTHORITY_CEILING.

The output card deliberately omits the covered-component list, findings, secret-exclusion detail, source refs, public runtime refs, scope boundary, scope limit, and source-module summary from the compact payload. Those keys remain in the full result record, which keeps the reader-facing card inspectable without turning it into a private-body export.

Shape

flowchart TD bundle["paper_module bundle: subjects + code_loci + scope limit"] inventory["standards_inventory.json"] contracts["organ_runtime_contracts.json"] policy["diagnostic_policy.json"] negatives["negative fixtures: missing standard, unmapped component, missing result record, overclaim, private source"] runtime["standards_meta_diagnostics.run / run_diagnostics_bundle"] scan["secret_exclusion_scan + public_runtime_refs"] result record["sign-off result record: counts, error codes, scope boundary"] projections["generated navigation projections: mermaid + atlas card"] bundle --> projections inventory --> runtime contracts --> runtime policy --> runtime negatives --> runtime runtime --> scan scan --> result record runtime --> result record

Evidence/accounting:

• core/paper_module_capsules.json::paper_modules[29:paper_module.standards_meta_diagnostics] is the JSON authority row. It names the component and mechanism subjects, the resolved code locus src/microcosm_core/organs/standards_meta_diagnostics.py, and the projection-only scope limit.
• paper_modules/standards_meta_diagnostics.json::paper_module_payload.source_authority is json_capsule; generated_projections.mermaid.status is available_from_capsule_edges; generated_projections.atlas_card.status is linked_from_capsule_edges; relationships.edges currently has 11 edges.
• organs/standards_meta_diagnostics.json::organ_payload.source_registry_row records status: accepted_current_authority, the validator command, and the generated result record refs; its claim_ceiling keeps the diagnostic scoped to the declared public contract.
• src/microcosm_core/organs/standards_meta_diagnostics.py names INPUT_NAMES, NEGATIVE_INPUT_NAMES, EXPECTED_NEGATIVE_CASES, PUBLIC_RUNTIME_REFS, and AUTHORITY_CEILING, which are the runtime contract this reader section summarizes.
• tests/test_standards_meta_diagnostics.py asserts the fixture and exported bundle paths, the five expected negative cases, source-module digest checks, body_in_receipt: false, real_runtime_receipt: true, and synthetic_receipt_standin_allowed: false.
• result records/sign-off/first_wave/standards_meta_diagnostics_fixture_acceptance.json records status: pass, accepted_organ_count: 77, standard_mapping_count: 77, runtime_contract_count: 77, five expected error codes, secret_exclusion_scan.blocking_hit_count: 0, and the scope boundary that the diagnostic excludes launch, providers, registry mutation, formal-result correctness, or whole-system correctness.

Reader Evidence Routing

• Start with the JSON Bundle Binding to identify the source record and the projection-only scope limit before treating the diagnostic as evidence.
• Use Structured Lattice Bindings to understand which wiring is resolved and which dependencies remain pending. Pending dependencies are honest residuals, not hidden failures.
• Use Validation Result record Path for reproducibility: focused pytest exercises the diagnostic policy and negative cases; the corpus check verifies paper-module parity.
• Treat secret-exclusion and public-runtime refs as result record evidence about public projection consistency. They do not mutate standards, include launch operations, expose private source material, or prove whole-system correctness.

Named Proof Consumers

• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_observes_negative_cases is the fixture consumer. It proves that the positive public inputs cover the accepted component set and that the five expected negative cases surface their named error codes.
• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_bundle_validates_runtime_shape is the exported-bundle consumer. It checks the bundle id, covered component set, source-module manifest status, source-open body-import counts, body_in_receipt: false, and the false scope limit flags.
• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_rejects_source_module_digest_mismatch, ::test_standards_meta_diagnostics_rejects_partial_source_module_digest_mismatch, and ::test_standards_meta_diagnostics_rejects_partial_target_module_digest_mismatch are the digest-drift consumers. They make copied source-module bodies falsifiable instead of relying on manifest prose.
• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_source_modules_are_exact_macro_body_imports is the exact-copy consumer for the three public source-body imports named in the exported bundle.
• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_receipts_use_secret_exclusion is the public/private boundary consumer. It checks that result record evidence uses the secret-exclusion lane and keeps private bodies out of public diagnostics.
• tests/test_standards_meta_diagnostics.py::test_standards_meta_diagnostics_input_builder_tracks_live_registry and the live-positive projection tests are the registry-freshness consumers. They keep fixture inputs tied to public registry state instead of allowing a stale checked-in example to become silent authority.

Prior Art Grounding

This component is grounded in schema- and contract-validation practice rather than in a claim that diagnostics create authority. JSON Schema treats a schema as a machine-readable vocabulary for validating structured JSON data, and OpenAPI uses interface descriptions so consumers can understand an API without reading source code or observing traffic. The component imports that pattern into Microcosm's launch boundary: standards, adapter contracts, result records, and scope limits are checked as public projections, while the diagnostic remains bounded evidence about consistency rather than a new source of truth.

Prior-art anchors:

• JSON Schema validation and structured-data constraints: https://json-schema.org/
• OpenAPI interface descriptions and conformance expectations: https://spec.openapis.org/oas/latest.html

Validation Result record Path

./repo-pytest tests/test_standards_meta_diagnostics.py -q \
  --basetemp=/tmp/microcosm_standards_meta_diagnostics_pytest
./repo-python scripts/build_doctrine_projection.py \
  --check-paper-module-corpus

This module is the public Microcosm projection of the source system's recursive self-improvement metabolism. It is not a synthetic result record layer. It imports the real source shape from recursive_self_improvement_operating_loop, doctrine_population_loop, and local_to_general_propagation: local pressure is sensed, classified, assigned to an owner surface, mutated or captured there, validated, closed out, and given a concrete re-entry condition.

The exported bundle also carries exact copies of the source bodies that make this loop real: recursive self-improvement, doctrine population, local-to-general propagation, the plane-home decision table, work log metacontrol, work log skill doctrine, and the work log standard. Result records report only source refs, hashes, counts, and scan status; the body text lives under examples/.../source_modules/ai_workflow/.

Purpose

The component answers one question: did a declared lesson actually change a named owner surface and pass that surface's own validation, or did it only produce a result record that says so? "The system learned from its work" is an easy claim to assert and a hard one to back. Without a check, a log entry, a closed ticket, or a confident summary all read as progress. This validator refuses that shortcut.

Each lesson row must name the surface it changed (a skill, a paper module, a standard, or a captured Work item), the action it took there, and the validation and completion refs that show the change held. Every ref must resolve to a real file in the exported bundle, the copied source modules, or the public Microcosm tree. A lesson then lands in exactly one of four outcomes: refined_existing_surface (a surface changed and was validated), workitem_captured (deferred work, but only with a concrete re-entry condition), nothing_to_refine (a typed null result that still required stewardship and a next-best-lane check), or already_propagated_verified. Anything that does not fit one of these is a finding, not an outcome.

The unusual part is the defence against self-grading. A lesson row may carry an expected_label or expected_status field, but the validator ignores it and recomputes the verdict from the evidence. If the row is not genuinely backed, its own asserted label cannot rescue it, and the case is recorded as VOICE_DOCTRINE_BAKED_EXPECTED_LABEL_IGNORED. A fixture cannot pass by declaring its own success. The same instinct runs through the negative floor: source notes, private thread bodies, model-output data, direct edits to doctrine nodes, and global promotion without owner validation are each rejected, keeping "the system improves itself" separate from "this public artifact may rewrite doctrine or export private voice."

Shape

flowchart LR Signal["Local pressure mistake, route gap, validation finding, residual"] Classify["Classify owner surface + action"] Owner["Owner surface skill, paper module, standard, Work item"] Refused["Refused raw voice, private body, direct node edit, result record-only, unvalidated promotion"] subgraph Outcome["One of four typed outcomes"] Refined["refined_existing_surface changed ref + validation"] Captured["workitem_captured with re-entry condition"] Null["nothing_to_refine stewardship + next-lane checked"] Already["already_propagated_verified"] end Recompute["Recompute verdict from evidence expected_label ignored"] Validate["Validation owner evidence + completion ref; every ref must resolve"] Source["Exact source bodies 8 manifest rows: hashes, anchors"] Result records["metadata-only result records result, board, validation, fixture sign-off"] Signal --> Classify Classify --> Owner Owner --> Refused Owner --> Outcome Outcome --> Recompute Recompute --> Validate Source --> Result records Validate --> Result records Refused --> Result records

Public Mechanics

• Local lessons carry source pattern refs, evidence refs, owner-surface ids, owner actions, validation refs, completion refs, and outcomes.
• Owner surfaces are explicit: skills, paper modules, standards, and residual captures each retain their own mutation authority.
• refined_existing_surface requires a changed owner surface and validation.
• workitem_captured requires a concrete re-entry condition.
• nothing_to_refine requires stewardship and next-best-lane checks.
• source notes, private thread bodies, model-output data, live work log bodies, direct doctrine-node edits, and global promotion claims are rejected by negative cases.
• Exported bundle validation requires source_module_manifest.json, verifies each copied body hash/line/byte/anchor contract, and scans copied bodies for forbidden public material.

Reader Evidence Routing

Read this module as a lesson-propagation validator, not as a general doctrine mutation license. The fixture proves that local pressure must choose a named owner surface, perform an owner-authorized action, carry validation and completion refs, and either refine an existing surface, capture a Work item with a re-entry condition, record a typed nothing_to_refine, or verify an already-propagated result.

Read source-open evidence through the exported bundle manifest. It carries eight copied source bodies: three paper modules, four skills or skill companions, and the work log standard. Each manifest row records byte and line counts, exact source and target hashes, required anchors, and body_in_receipt: false. The source bodies make the source loop inspectable, while result records remain refs, hashes, counts, scan status, and scope limits.

Read the negative floor as equally load-bearing. source notes bodies, private thread bodies, model-output data bodies, direct doctrine-node edits, result record-only progress, live work log mutation, and unvalidated global promotion are rejected. Those rejections keep "the system learns from work" separate from "this public artifact can mutate doctrine or export private state."

Prior Art Grounding

This component is grounded in after-action review, lessons-learned, and pattern language practices. NASA's Lessons Learned Information System is a public example of preserving operational lessons so future work can reuse them, while pattern-language practice gives a vocabulary for turning repeated local solutions into named, reusable forms. Microcosm adopts that direction without collapsing operator voice into doctrine: a local lesson only becomes durable when it has evidence, an owner surface, a validation result record, and a bounded re-entry path.

Prior-art anchors:

• NASA Lessons Learned Information System: https://llis.nasa.gov/
• Pattern language background: https://hillside.net/patterns/

Runtime

PYTHONPATH=src python -m microcosm_core.organs.voice_to_doctrine_self_improvement_loop run \
  --input fixtures/first_wave/voice_to_doctrine_self_improvement_loop/input \
  --out receipts/first_wave/voice_to_doctrine_self_improvement_loop

The exported bundle uses the same validator without negative-case inputs:

PYTHONPATH=src python -m microcosm_core.organs.voice_to_doctrine_self_improvement_loop run-bundle \
  --input examples/voice_to_doctrine_self_improvement_loop/exported_voice_to_doctrine_bundle \
  --out receipts/runtime_shell/demo_project/organs/voice_to_doctrine_self_improvement_loop

Validation Result record Path

Run from microcosm-substrate:

A green fixture or bundle result record proves only the public lesson-propagation boundary above; it does not grant source-file changes, live work log mutation, global doctrine-promotion, launch, or whole-system authority.

cognitive_operator_registry is the public contract diagnostic for the source system's typed cognitive-operator system. It checks that each public operator row carries the required operator-shape fields, that every active operator is backed by a dogfood result record proving it changed a live decision, and that the registry policy declares explicit scope limits before a cold reader trusts the operators as real reusable cognition rather than inspirational prose.

Purpose

A team that writes down its reusable thinking moves as a registry tends to accumulate entries faster than it can prove any of them help. The single question this component answers is: which of these listed operators has actually changed a live decision, and which is just a tidy description of one? An entry may only call itself active if it points to a dogfood result record, and that result record must carry cognition_delta_evidence recording a concrete decision that came out differently because the operator was applied.

The unusual part is that the check refuses to take a row at its word. Where a result record cites evidence surfaces, command paths, or task-ledger handles, the validator resolves each one against the public system (see _dogfood_receipt_ref_resolves and _record_dogfood_evidence_resolution_findings in the source). A row whose prose says it was dogfooded but whose evidence does not resolve is recorded as a failure, not a pass. A second check, the anti-sprawl case, flags two operators that share a slug or a near-identical claim unless an accretion decision was recorded, so the registry cannot quietly grow two near copies of the same idea.

The evidence contract is source-open by default. The validator emits refs, hashes, counts, and verdicts; secret_exclusion_scan proves that secrets, account or session material, model-output data bodies, source notes, and account secret-equivalent access material are excluded. Operator bodies are never inlined into the JSON result record, so the positive evidence carries body_in_receipt: false, real_runtime_receipt: true, and synthetic_receipt_standin_allowed: false.

Prior Art Grounding

This component borrows from cognitive work analysis, provenance, schema validation, and policy-gated registries. Useful anchors include:

• Cognitive Work Analysis, summarized in this information-systems design overview, as prior art for analyzing cognitive work in complex sociotechnical systems.
• W3C PROV, for connecting operator claims to activities, agents, and evidence used to evaluate trustworthiness.
• JSON Schema, for the required-shape validation pattern behind public operator rows.
• Open Policy Agent, as a precedent for policy evaluation that remains distinct from the registry data being evaluated.

Microcosm borrows the cognitive-work, provenance, shape-checking, and policy registry patterns, but keeps this component to a public contract diagnostic. It does not mutate operators, prove operator correctness, expose private operator bodies or source notes, authorize providers, or include launch operations.

It consumes public operator_registry.json, operator_standard.json, and dogfood_index.json inputs that project real source operator rows and dogfood result records. Its result record contract is source-open by default: secret_exclusion_scan proves that secrets, account or browser material, model-output data bodies, source notes, and account secret-equivalent live-access material are excluded, while public_runtime_refs point at the real standard, component, sign-off, fixture, bundle, and paper-module system. Bodies are not inlined into JSON result records, so the positive evidence uses body_in_receipt: false, real_runtime_receipt: true, and synthetic_receipt_standin_allowed: false.

The component rejects seven boundary failures:

• operator rows missing required operator-shape fields
• active operators with no backing dogfood result record
• dogfood result records missing cognition_delta_evidence
• near-duplicate operators (identical slug or near-identical claim) with no recorded accretion decision (the anti-sprawl governor case)
• launch, provider, source-file changes, registry-mutation, or operator-correctness overclaims
• operator rows that claim operator-voice or source note authority
• private operator source bodies or model-output data bodies in public inputs

The exported bundle also imports three verbatim source bodies behind an import membrane: the cognitive-operator registry (codex/doctrine/cognitive_operators.json), the cognitive-operator standard (codex/standards/std_cognitive_operator.json), and the registry projection/validation tool (system/lib/cognitive_operator_registry.py). Each is copied byte-for-byte with a sha256 digest and required anchors; result records carry refs, hashes, counts, and verdicts only.

Shape

flowchart LR Registry["Public operator registry operator ids, roles, runtime refs"] Standard["Operator standard required fields, scope limit"] Dogfood["Dogfood result records cognition-delta evidence"] Validator["cognitive_operator_registry validator"] Source["Copied source bodies registry, standard, validator tool"] Negative["Negative floor missing fields, no dogfood, sprawl, overclaim, private leakage"] Result record["Result records refs, hashes, counts, verdicts; body text omitted"] Registry --> Validator Standard --> Validator Dogfood --> Validator Source --> Validator Validator --> Negative Validator --> Result record

Reader Evidence Routing

Read this module as a public contract diagnostic, not as a glossary of operators or a live execution surface. This page explains the shape a reader should verify; the structured data lives in the JSON files below.

Start with paper_modules/cognitive_operator_registry.json for the full module record, then use standards/std_microcosm_cognitive_operator_registry.json to check required fields, forbidden authority, public/private boundary rules, and result record expectations. Open core/fixture_manifests/cognitive_operator_registry.fixture_manifest.json before inspecting fixtures or copied source modules, because the manifest names the source-open body floor and the body-omission contract.

Read dogfood result records as evidence that an active operator changed a live decision; do not read them as proof that the operator is generally correct. Read negative cases as part of the positive claim: missing roles, missing dogfood, missing cognition-delta evidence, duplicate/sprawl pressure, operator-voice claims, authority overclaims, and private-source leakage must remain rejected.

Technical Mechanism

The runtime mechanism lives in src/microcosm_core/organs/cognitive_operator_registry.py. run() loads the first-wave public fixture inputs: operator_registry.json, operator_standard.json, and dogfood_index.json. _positive_findings() checks that operator rows have required ids, slugs, roles, claims, runtime refs, evidence refs, and scope limits, then requires each active operator to resolve to a dogfood result record with cognition-delta evidence. The dogfood evidence resolver follows public fixture refs and copied bundle handles rather than accepting a row because its prose says it was dogfooded.

Negative pressure is source-declared in EXPECTED_NEGATIVE_CASES. _negative_findings() exercises missing required fields, active operators without dogfood result records, dogfood rows without cognition-delta evidence, operator sprawl without accretion decisions, operator-voice authority claims, provider/source/launch/correctness overclaims, and private source or model-output data leakage. A pass is therefore not only "the positive rows parsed"; it also means the expected refusal classes were observed and recorded.

run_registry_bundle() is the body-floor consumer. It executes the same registry contract against examples/cognitive_operator_registry/exported_cognitive_operator_registry_bundle and makes _source_module_manifest_result() mandatory. The manifest must prove exact copied source bodies for codex/doctrine/cognitive_operators.json, codex/standards/std_cognitive_operator.json, and system/lib/cognitive_operator_registry.py; _source_open_body_import_summary() then records body ids, classes, line counts, hashes, and body_in_receipt: false. AUTHORITY_CEILING keeps those result records below registry mutation, operator correctness, provider authority, source-file changes, launch, and whole-system correctness.

Named Proof Consumers

• microcosm_core.organs.cognitive_operator_registry.run is the first-wave fixture consumer. It reads the public registry, standard, and dogfood index, writes the result, board, validation, and sign-off result records, and checks the expected negative floor.
• microcosm_core.organs.cognitive_operator_registry.run_registry_bundle is the exported-bundle consumer. It proves the copied source registry, standard, and validator bodies through source-module manifest equality while keeping copied body text out of result records.
• tests/test_cognitive_operator_registry.py::test_cognitive_operator_registry_observes_negative_cases is the public-contract regression. It asserts that all expected negative cases are observed and that all fixture operators have dogfood result records.
• tests/test_cognitive_operator_registry.py::test_cognitive_operator_registry_bundle_validates_runtime_shape is the bundle-shape regression. It checks operator counts, source-module manifest status, body-material ids, and the metadata-only result record boundary.
• tests/test_cognitive_operator_registry.py::test_cognitive_operator_registry_source_modules_are_exact_macro_body_imports is the exact-copy proof consumer. It byte-compares every manifest source ref with the copied target and verifies the recorded sha256 digests.

Validation Result record Path

Run the first-wave fixture into disposable result records from the Microcosm root:

Run the exported bundle through the same component:

cd microcosm-substrate
PYTHONPATH=src ../repo-python -m microcosm_core.organs.cognitive_operator_registry run-registry-bundle --input examples/cognitive_operator_registry/exported_cognitive_operator_registry_bundle --out /tmp/microcosm_cognitive_operator_registry_bundle

cd microcosm-substrate
../repo-pytest tests/test_cognitive_operator_registry.py -q
cd ..
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

The source atlas row carries the matching paper_module_ref, mechanism_refs, and code_loci entries.

routing_anti_patterns_registry is the public contract diagnostic for the source system's typed navigation failure rows. It validates the copied codex/doctrine/routing_anti_patterns.json registry as runnable Microcosm system: the input must declare kind: routing_anti_patterns, carry a positive version, and expose stable anti_patterns rows with unique ids and plain explanatory text.

The positive fixture imports the real source registry body. The exported bundle also carries a source module manifest and a byte-for-byte copy under source_modules/codex/doctrine/routing_anti_patterns.json, with sha256 hashes and anchors for kernel_before_grep, bridge_before_scope, and mode_in_chat_only. Result records carry refs, hashes, counts, and verdicts only; they do not inline the copied body.

The component rejects five boundary failures:

• missing kind
• duplicate anti-pattern ids
• anti-pattern rows missing explanatory text
• launch, provider, source-file changes, route-policy mutation, maturity, or whole-system-correctness overclaims
• private routing bodies, source note bodies, model-output data bodies, or secret values in public inputs

Purpose

A navigation system can fail quietly. An agent reaches for grep when a kernel route would have narrowed the space first, or changes execution mode in chat without updating the disk contract, and nothing complains until the work is already off the rails. This component answers one question: does the public registry of known routing failures hold its declared shape, and does the copied source body that backs it stay byte-honest? It names recurring navigation mistakes as typed rows so they can be recognised, not rediscovered.

The registry is treated as a checked artifact, not as authority. A page describing routing failures is easy to read as a router or as policy. The component refuses both: a row may project a public anti-pattern, but it may not declare source_authority, route_authority, or any internal control role, and the validator rejects rows that try. So the document can describe how navigation goes wrong without itself becoming the thing that decides how navigation should go.

One design choice sits in how each row's route-repair state is decided. Rather than trust a label baked into the row, the checker derives the repair state from the row's own id and explanatory text: kernel_before_grep only earns kernel_first_navigation if its text actually mentions grep, kernel, and route. A row carrying a pre-written expected_route_repair_state is flagged, and baked_expected_labels_sufficient is fixed to false. The point is to stop a registry from grading itself by self-asserted labels, and to keep the meaning grounded in the text a reader can see.

Shape

This module is a projection over a bundle-backed public routing diagnostic, not route source authority. Cold readers should read it as a bounded chain: the JSON bundle and standard name the contract; the runtime component validates fixtures and an exported source bundle; result records preserve hashes, counts, verdicts, and negative cases; generated Mermaid and Atlas rows expose the bundle edges; the scope limit remains projection-only.

flowchart TD Bundle["core/paper_module_capsules.json paper_module.routing_anti_patterns_registry"] Standard["standards/std_microcosm_routing_anti_patterns_registry.json"] Markdown["paper_modules/routing_anti_patterns_registry.md reader projection; not route authority"] Runtime["src/microcosm_core/components/routing_anti_patterns_registry.py run / run-bundle / result record writer"] Fixture["fixtures/first_wave/routing_anti_patterns_registry/input registry + negative cases"] Bundle["examples/routing_anti_patterns_registry/exported_routing_anti_patterns_bundle source_module_manifest + exact copied body"] Tests["tests/test_routing_anti_patterns_registry.py"] Result records["result records/.../routing_anti_patterns_registry*.json refs, hashes, counts, verdicts"] structured source record["paper_modules/routing_anti_patterns_registry.json 22 edges; Mermaid available; Atlas linked"] Ceiling["Scope limit no route authority, mutation, external model access, launch, or whole-system proof"] Bundle --> Markdown Bundle --> structured source record Standard --> Runtime Fixture --> Runtime Bundle --> Runtime Runtime --> Tests Runtime --> Result records Tests --> Result records structured source record --> Ceiling Result records --> Ceiling Markdown --> Ceiling

Technical Mechanism

The component is a contract checker around a public routing-registry copy, not a router. run loads the first-wave fixture and asks _build_result to validate the positive routing_anti_patterns.json payload, all declared negative cases, the secret-exclusion scan, and the metadata-only result record bundle. The positive path requires kind: routing_anti_patterns, a positive integer version, stable anti-pattern ids, explanatory text, and the named source anchors kernel_before_grep, bridge_before_scope, and mode_in_chat_only.

The failure lattice is explicit. _payload_findings records typed evidence for missing kind, non-positive version, missing rows, missing ids, duplicate ids, missing text, forbidden authority-role masquerade, private-source fields, and overclaims about launch, external model access, source-file changes, route-policy mutation, maturity, readiness, or whole-system correctness. A pass is admitted only when every expected negative case appears with its expected error code and missing_negative_cases is empty. That makes the negative cases proof obligations rather than illustrative examples.

The exported-bundle path adds source-copy accountability. run-bundle calls run_routing_anti_patterns_bundle, which requires bundle_manifest.json, source_module_manifest.json, and the copied body under source_modules/codex/doctrine/routing_anti_patterns.json. The manifest checker streams sha256 over the copied target, verifies sha256, source_sha256, and target_sha256, checks required anchors, classifies the material as copied_non_secret_macro_body, and rejects any body-in-result record claim. The source body is available in the exported source-module tree; result records keep only refs, hashes, counts, verdicts, and omission fields.

The governing lattice is deliberately narrow. The bundle binds this mechanism to concept.architecture_and_navigation_route_contract_bundle, P-1, P-2, P-3, P-5, P-6, P-8, P-9, P-12, P-15, and AX-1, AX-4, AX-5, AX-7, AX-8, AX-11, but the checker consumes those refs as a scope limit: evidence must be replayable, typed, public-safe, and below projection authority. It also depends on navigation_hologram_route_plane, agent_route_observability_runtime, and cold_reader_route_map, so the registry can describe navigation failure shapes without becoming the internal control route source.

Reader Evidence Routing

Read this module through the following source-to-proof route:

1. Start at the source record core/paper_module_capsules.json::paper_modules[58:paper_module.routing_anti_patterns_registry]. It is the source authority for source_authority: json_capsule, the component subject, mechanism subject, runtime source locus, concept, principles, axioms, dependency modules, and the projection statuses.
2. Read the generated structured source record paper_modules/routing_anti_patterns_registry.json only as a projection from that source record.
3. Follow the runtime proof path through src/microcosm_core/organs/routing_anti_patterns_registry.py, fixtures/first_wave/routing_anti_patterns_registry/input/, and examples/routing_anti_patterns_registry/exported_routing_anti_patterns_bundle/. Those surfaces carry the public registry fixture, negative cases, source_module_manifest.json, copied body target, required anchors, and digest checks.
4. Confirm the public result record floor with the named fixture command, bundle command, focused regression, and corpus check below. Result records may carry ids, refs, hashes, counts, verdicts, and omission fields, but not private routing bodies or model-output data.
5. Treat generated diagram, Atlas, search, object-map, and site cards as reachability projections from the same source row. They help a public reader find the module; they do not outrank the bundle, runtime, manifest, tests, or metadata-only result records.

Named Proof Consumers

• First-wave fixture consumer: PYTHONPATH=src ../repo-python -m microcosm_core.components.routing_anti_patterns_registry run --input fixtures/first_wave/routing_anti_patterns_registry/input --out /tmp/microcosm-routing-anti-patterns-registry/fixture --sign-off-out /tmp/microcosm-routing-anti-patterns-registry/sign-off.json --card consumes the public registry fixture, six expected negative-case families, private-source rejection, secret-exclusion scan, metadata-only result record writer, and command-card omission boundary.
• Exported-bundle consumer: PYTHONPATH=src ../repo-python -m microcosm_core.organs.routing_anti_patterns_registry run-bundle --input examples/routing_anti_patterns_registry/exported_routing_anti_patterns_bundle --out /tmp/microcosm-routing-anti-patterns-registry/bundle --card consumes the source-module manifest, exact copied source registry body, sha256 digest floor, required anchors, material class, and source-open summary while keeping body text out of result records.
• Focused regression consumer: PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider tests/test_routing_anti_patterns_registry.py -q pins negative-case coverage, source-authority masquerade rejection, digest mismatch blockers, exact copied-body imports, secret-exclusion result record policy, and fresh-card reuse behavior.
• It is a read-only result record for this Markdown slice, not permission to hand-edit generated projections.

Prior Art Grounding

This registry follows the same family as pattern and anti-pattern catalogs: name recurring failure shapes so future operators can recognize and avoid them. The Hillside patterns library is the positive pattern-language ancestor, and the software anti-pattern literature supplies the inverse move: documenting repeated practices that look useful but produce bad outcomes.

The routing-specific presentation also borrows from CLI usability practice. The Command Line Interface Guidelines emphasize discoverability, clear errors, and suggested next actions; this component applies that pressure to navigation failures by requiring stable ids and explanatory text while keeping the registry projection below route-source authority.

Validation Result record Path

From microcosm-substrate, validate the public routing-registry diagnostic without writing tracked result records:

Passing validation proves the public anti-pattern registry fixture and copied-body digest floor only. It does not make this registry route source authority, and it excludes route-policy mutation, external model access, launch, or whole-system correctness.

doctrine_fact_claim_audit is a Crown Jewel import component with real runnable system and a strict public scope limit. It consumes synthetic public fixtures, copied source source bodies, and source manifests that verify sha256 digests, line counts, required anchors, secret-exclusion status, and result record body omission.

What it proves: fact assertion, code-loci, DAG, and numeric claim binding fixture truth gate only.

Purpose

Documentation about a living system rots. A page states that there are forty-seven of something, or cites a function in a file, and both claims quietly go stale as the code moves underneath them. A reader cannot tell a current count from a number that was true once and never rechecked. This component exists to answer one question: which of a page's factual assertions can be re-derived from source right now, and which have become untracked drift?

The approach treats a documentation claim like a cached value that needs an invalidation strategy. A bare number is not enough; the claim is admissible only when it is bound to a fact assertion that records how to recompute or revalidate the value. The same pass resolves every cited code locus on disk and checks that the quoted anchor text is actually present, so a plausible-but-dead file reference becomes a typed finding rather than inert prose. The interesting move is that nothing here asks a model whether the prose reads as true. The component recomputes a bounded relation over public fixtures and reports only what that relation supports.

The second design choice worth naming is how the checks are proved. The negative floor is semantic, not label-trusting: the test harness overwrites the declared failure fixtures with bogus pass rows and confirms the evaluator still derives the expected stable error codes itself. That keeps the proof attached to the mechanism rather than to the fixture filenames. The honesty of the page rests on that: the component is a narrow claim-audit gate over copied public fixtures, not a comprehension engine, a minimum-read-graph proof, a source-file changes lane, or any launch-scope decision.

Prior Art Grounding

This component borrows from provenance modeling, structured fact-check metadata, schema validation, and supply-chain attestation. Useful anchors include:

• W3C PROV, which models entities, activities, and agents so readers can assess the quality, reliability, and trustworthiness of derived information.
• Schema.org ClaimReview, as a web metadata pattern for recording a reviewed claim and its fact-checking context.
• JSON Schema, for declaring expected structure and rejecting malformed or incomplete claim records.
• SLSA provenance, for the software-supply-chain pattern of tracing artifacts back to source and build metadata.

Microcosm borrows the provenance, claim-review, schema, and attestation shapes, but keeps this component to public fixture fact counts, code-loci existence, anchor presence, DAG references, and synthetic volatile numeric binding cases. It is not a comprehension engine, private-doctrine export, launch-scope decision, or a minimum-read-graph proof.

Technical Mechanism

The runtime mechanism is a public fixture evaluator in src/microcosm_core/organs/doctrine_fact_claim_audit.py. The component declares a CrownJewelSpec with four required inputs: fact_assertions.json, fact_dag.json, numeric_claims.json, and projection_protocol.json. The shared crown-jewel runner handles source-manifest validation, result record writing, negative-case execution, and scope limit attachment; this module supplies the domain evaluator and the semantic negative-case mutator.

evaluate first loads the fact assertion table and compares expected_fact_count to the number of fact rows. Each fact must carry at least one code locus. The evaluator resolves every relative code-locus path against the copied source-module bundle, then checks that the declared anchor text is present in the copied body. The DAG pass builds the set of audited fact ids and rejects any edge whose from or to endpoint is not in that set. These checks convert plausible documentation references into result record-backed paths, anchors, and graph edges.

Numeric claims are checked by importing the copied source_modules/system/lib/derived_fact_hologram.py body from the exported bundle and calling its find_unbound_numeric_claims function. For each row in numeric_claims.json, the evaluator synthesizes FactAssertion instances for the declared sections, records unbound numeric detections, and blocks a case when a non-detector row leaves current-state numeric prose without a matching fact assertion. Detector rows are positive evidence only because they must surface the expected section and number.

The negative floor is semantic rather than label-trusting. evaluate_negative_case mutates the positive fixture in memory for wrong_fact_count, missing_code_locus, dead_code_locus, dead_dag_ref, and unbound_numeric_claim, then reruns the same evaluator in a temporary input directory. The tests deliberately overwrite the declared negative-case files with bogus pass rows and confirm that the component still derives the expected stable error codes from the evaluator itself. That keeps the proof tied to the mechanism, not to fixture labels.

The source-open body floor is separate from the result record floor. The exported bundle manifest names two copied bodies, derived_fact_hologram.py and paper_modules.py, with digests and line counts. Runtime result records carry refs, counts, verdicts, scope boundaries, and body_in_receipt: false; they do not embed copied source bodies or private operator material.

How to run it:

Runtime bundle route:

PYTHONPATH=src python3 -m microcosm_core.organs.doctrine_fact_claim_audit run-doctrine-fact-bundle --input examples/doctrine_fact_claim_audit/exported_doctrine_fact_claim_audit_bundle --out receipts/runtime_shell/demo_project/organs/doctrine_fact_claim_audit

Shape

• Subject: doctrine_fact_claim_audit, with mechanism mechanism.doctrine_fact_claim_audit.validates_public_doctrine_fact_claim_audit.
• Runtime locus: src/microcosm_core/organs/doctrine_fact_claim_audit.py, especially run, run_doctrine_fact_bundle, evaluate, _evaluate_numeric_claims, _load_derived_fact_module, EXPECTED_NEGATIVE_CASES, and AUTHORITY_CEILING.
• The fixture checks an expected fact count, resolves declared code-locus paths, verifies required source anchors, rejects dead DAG references, and requires volatile numeric claim cases to be bound to fact assertions.
• The accepted positive result record reports three facts, three verified code loci, two DAG edges, two numeric claim cases, and one detected unbound numeric detector case, while preserving body_in_receipt: false.
• The negative floor is stable: dead_code_locus, dead_dag_ref, missing_code_locus, unbound_numeric_claim, and wrong_fact_count.
• The public standard is standards/std_microcosm_doctrine_fact_claim_audit.json; the fixture manifest is core/fixture_manifests/doctrine_fact_claim_audit.fixture_manifest.json.

flowchart LR Facts["fact_assertions.json facts + expected_fact_count"] --> Eval["evaluate"] Dag["fact_dag.json edges"] --> Eval Numerics["numeric_claims.json cases"] --> Eval Manifest["source module manifest copied bodies"] --> Eval Eval --> Count{"declared fact count = table length?"} Eval --> Loci{"each code locus path on disk + anchor in body?"} Eval --> DagRef{"DAG endpoints are known fact ids?"} Eval --> Bound{"current-state numerics bound to a fact assertion section?"} Count -->|mismatch| Block["typed blocking finding"] Loci -->|missing path or anchor| Block DagRef -->|dead ref| Block Bound -->|unbound| Block Count -->|ok| Result record["metadata-only result record body_in_receipt: false"] Loci -->|ok| Result record DagRef -->|ok| Result record Bound -->|ok| Result record Neg["evaluate_negative_case mutate fixture, rerun evaluator"] --> Codes["expected stable error codes"]

Named Proof Consumers

• Fixture CLI consumer: PYTHONPATH=src ../repo-python -m microcosm_core.components.doctrine_fact_claim_audit run --input fixtures/first_wave/doctrine_fact_claim_audit/input --out /tmp/microcosm-doctrine-fact-claim-audit/fixture --sign-off-out /tmp/microcosm-doctrine-fact-claim-audit/sign-off.json --card. Expected proof shape: status: pass, three fact rows, three verified code loci, two DAG edges, two numeric-claim cases, one detector case, zero blocking unbound numerics, five semantic negative cases, and body_in_receipt: false.
• Exported bundle consumer: PYTHONPATH=src ../repo-python -m microcosm_core.organs.doctrine_fact_claim_audit run-doctrine-fact-bundle --input examples/doctrine_fact_claim_audit/exported_doctrine_fact_claim_audit_bundle --out /tmp/microcosm-doctrine-fact-claim-audit/bundle --card. Expected proof shape: the same evaluator runs through the exported bundle input mode, validates the source-module manifest, and writes metadata-only bundle result records.
• Focused regression consumer: PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider --basetemp=/tmp/microcosm_doctrine_fact_claim_audit_pytest tests/test_doctrine_fact_claim_audit.py -q. Expected proof shape: the seven tests cover the positive fixture, dead code locus, missing code locus, dead DAG ref, unbound numeric claim, semantic negative-case derivation, and exported-bundle route.
• Corpus parity consumer: PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus. Expected proof shape: the structured source record remains reproducible from the bundle and Markdown projection without hand-editing generated state.
• structured source record readback consumer: jq '{source_authority:.paper_module_payload.source_authority, mermaid:.paper_module_payload.generated_projections.mermaid.status, atlas:.paper_module_payload.generated_projections.atlas_card.status, edge_count:(.relationships.edges|length), unresolved:(.relationships.unpopulated_selective_relations|length)}' paper_modules/doctrine_fact_claim_audit.json. Expected proof shape: json_capsule, available_from_capsule_edges, linked_from_capsule_edges, resolved bundle edges, and zero unpopulated selective relations.

Reader Evidence Routing

• Start with paper_modules/doctrine_fact_claim_audit.json as the primary reference, then open this Markdown page as a reader guide to that record.
• Open standards/std_microcosm_doctrine_fact_claim_audit.json for the standard, required witnesses, negative floor, denied authority, and result record contract.
• Open core/fixture_manifests/doctrine_fact_claim_audit.fixture_manifest.json for fixture inputs, copied-body counts, durable result record refs, and source-open body omission rules.
• Open examples/doctrine_fact_claim_audit/exported_doctrine_fact_claim_audit_bundle/source_module_manifest.json before inspecting copied source modules; result records carry refs and digests, not copied source body text.
• Run the fixture or bundle route from the microcosm-substrate directory and inspect the written JSON files. The component CLI exposes --card, but it does not expose a --json stdout mode.
• Use scripts/build_doctrine_projection.py --check-paper-module-corpus to verify this paper-module projection stays inside the shared corpus contract.

Claim-Rot Detection

This component treats documentation claims like cached values that need an invalidation strategy. The failure mode is not only a wrong number; it is a volatile number embedded in current-state prose with no attached route for re-deriving it.

The detector flags volatile numerics: a number near a countable noun inside a current-state section. Such a claim is admissible only when it is bound to a fact assertion that records how to recompute or revalidate the value. The same audit resolves every cited code locus on disk and checks that the quoted anchor is actually present, so stale file references and plausible-but-dead anchors are negative evidence rather than inert prose.

The public fixture does not claim natural-language comprehension. It proves the more useful contract: current-state numerics, fact assertions, DAG refs, code loci, and anchor text can be audited as result record-backed claims instead of untracked documentation drift.

Scope limit: Doctrine fact claim audit checks only public fixture fact counts, code-loci existence, anchor presence, DAG references, and synthetic volatile numeric claim binding cases. It is not a comprehension engine, does not establish a minimum read graph, does not export private doctrine, and excludes launch.

Validation Result record Path

From microcosm-substrate, validate with external result record outputs so the reader check does not churn tracked result records:

A diagram view is generated for this module, and an atlas card links to it. Passing result records validate fact-count, code-locus, DAG-ref, numeric-claim, digest, and negative-case boundaries only. If copied source bodies drift, refresh the exact copy bundle through the owning lane before treating bundle red as a reader-page defect.

Negative cases covered by the fixture manifest: dead_code_locus, dead_dag_ref, missing_code_locus, unbound_numeric_claim, wrong_fact_count.

Source provenance is anchored by examples/doctrine_fact_claim_audit/exported_doctrine_fact_claim_audit_bundle/source_module_manifest.json and result records carry refs, digests, counts, verdicts, and scope boundaries only.

Purpose

A navigation system that lists what it knows is easy to build. A system that can state, precisely, what it has not yet covered is harder, and it is the more honest signal to a cold reader. This component answers one question: for a declared set of Kind Atlas families, how many rows does the option surface expose that the generated System Atlas has not yet materialised?

The answer is a small debt vector, computed rather than asserted. For each selected kind the component recomputes the live Kind Atlas row count through system.lib.kind_atlas.build_kind_atlas, counts the entities the build_system_atlas.py graph has actually materialised for that kind, and reports the difference as known coverage debt. Concepts, mechanisms and standards are checked back to real source source files so the materialised set cannot be inflated with names that have no file behind them.

The unusual part is what the validator refuses. It will not accept a fixture that claims its unknown-unknowns are exhaustive: declaring claims_unknown_unknowns_exhaustive raises a finding rather than passing. The ledger reports a bounded count of gaps it can see and explicitly declines to claim there are no others. Known debt is treated as typed residual pressure, not as a completeness proof, and absence of a row is never read as proof that nothing is missing.

Abstract

self_ignorance_coverage_ledger is a public Microcosm Crown Jewel component that measures a narrow, source-grounded form of self-ignorance: known row-level coverage debt between live Kind Atlas option-surface counts and generated System Atlas materialization evidence. It recomputes the selected Kind Atlas families, derives materialized entity IDs from a build_system_atlas.py graph snapshot, source-validates graph-derived entity IDs, replays semantic negative cases, and emits metadata-only result records with scope boundaries.

The current exported bundle is a realness-rung R4 check when the source repo is available: live Kind Atlas counts are bound, the System Atlas graph slice is builder-bound, the live System Atlas graph is cross-checked, expected entity IDs are source-backed, and copied source source bodies are digest-bound through a manifest. The claim is only known_kind_atlas_coverage_debt_projection_only: it is not absence proof, unknown-unknown omniscience, total repository search proof, source-file changes, launch-scope decision, publishing-scope decision, private-system equivalence, provider affiliation, or whole-system correctness.

Problem

Navigation systems can overstate themselves in two opposite ways. A vague "coverage is incomplete" tells a cold reader nothing operational. A confident "nothing else is missing" is worse: it converts absence of evidence into evidence of absence. This component exists to occupy the narrow technical middle: for a declared finite domain of Kind Atlas families, compute the gap between what the option surface exposes and what the System Atlas graph has materialized.

The result is a self-ignorance ledger, not a universal discovery engine. Its positive output is a bounded debt vector. Its negative output is equally important: the validator must refuse fixtures that claim exhaustive unknown-unknown coverage, hand-author materialization counts, substitute entity IDs, use stale/baked expected IDs as authority, tamper with the System Atlas builder result record, or repair a copied-source manifest into a self-reference.

Mechanism

The runtime locus is src/microcosm_core/organs/self_ignorance_coverage_ledger.py. The exported-bundle entrypoint is run_self_ignorance_bundle; the core evaluator is evaluate; the semantic negative-case replayer is evaluate_negative_case; the local scope limit is AUTHORITY_CEILING.

The evaluator consumes four public bundle files:

Algorithmically, the component performs this loop:

1. Load bundle inputs and the source-module manifest through the Crown Jewel common runner.
2. Recompute selected Kind Atlas rows from the source repo when system/lib/kind_atlas.py is available.
3. Load system_atlas_graph.json, require the System Atlas builder marker, and derive materialized IDs by kind.
4. Cross-check the bundled graph slice against state/system_atlas/system_atlas.graph.json when the source repo is available.
5. For concepts, mechanisms, and standards, verify that graph-derived expected IDs resolve to real source source files.
6. Compute known_coverage_debt_count = live_kind_atlas_row_count - graph_derived_materialized_count by kind.
7. Replay semantic negative cases from clean input copies instead of trusting declared error labels.
8. Write result records with refs, counts, hashes, findings, realness evidence, and scope boundaries; copied body text stays out of result records.

For the current exported bundle, the public count vector is:

Those numbers come from examples/self_ignorance_coverage_ledger/exported_self_ignorance_coverage_ledger_bundle/kind_atlas_rows.json, materialized_entities.json, and system_atlas_graph.json, and are proof-consuming snapshot facts. They are not stable doctrine constants; rerun the validator after Kind Atlas, System Atlas, or source manifests move.

Projection Protocol Result record

projection_protocol.json is the result record that prevents a static graph slice from masquerading as live authority. The accepted bundle must carry:

The focused tests test_self_ignorance_coverage_ledger_rejects_projection_scope_tamper and test_self_ignorance_coverage_ledger_rejects_system_atlas_receipt_tamper are the proof consumers for this protocol.

Mermaid Flow

flowchart LR KA["Live Kind Atlas rows 503 selected rows"] Graph["System Atlas graph slice 307 materialized entities"] Proto["projection_protocol.json scope + build_system_atlas.py result record"] Source["Source source files concept/mechanism/standard ids"] Manifest["source_module_manifest.json copied_non_secret_macro_body"] Eval["evaluate()"] Neg["semantic negative-case replay"] Debt["known debt vector 196 units"] Result record["metadata-only result records counts, refs, hashes, scope boundaries"] Ceiling["scope limit known debt projection only"] KA --> Eval Graph --> Eval Proto --> Eval Source --> Eval Manifest --> Eval Eval --> Debt Eval --> Neg Debt --> Result record Neg --> Result record Result record --> Ceiling

This diagram is the human proof path and must stay subordinate to the bundle and generated projection.

Real-Good / Real-Bad / Perturbation Evidence

The positive case is test_self_ignorance_coverage_ledger_projects_real_bundle_known_debt plus the bundle route:

PYTHONPATH=src ../repo-python -m microcosm_core.organs.self_ignorance_coverage_ledger run-self-ignorance-bundle --input examples/self_ignorance_coverage_ledger/exported_self_ignorance_coverage_ledger_bundle --out /tmp/microcosm-self-ignorance-coverage-ledger/bundle --card

The accepted result must report status pass, known debt 196, observed negative cases forbidden_absence_inference and coverage_debt_mismatch, realness_rung: R4, live_kind_atlas_recompute_used: true, live_system_atlas_graph_crosscheck_used: true, and source-module digest success.

The real-bad cases are not marketing examples; they are the contract. Treat a guard as validated only when the focused pytest route passes in the current checkout:

Perturbation evidence is test_self_ignorance_coverage_debt_moves_with_materialized_entity_graph: adding a real, source-backed standard entity moves the known-debt count from 196 to 195 and keeps the result passing. That proves the ledger is coupled to the graph-derived materialization set, not to a fixed prose number.

The unsourced-materialization guard target is test_self_ignorance_coverage_ledger_rejects_coherent_fake_standard_entity. Its intended refusal is SELF_IGNORANCE_EXPECTED_ENTITY_ID_SOURCE_MISSING, but the paper must not count that guard as validated unless the focused pytest route currently blocks the fake standard entity. If it regresses, lower the source-validation claim to the passing guards above and route the source/test issue through the work log before completion.

Source-Backed Concept / Mechanism / Law Links

P-19 appears in the component atlas row as an adjacent governing principle for residual classification, but it is not part of the paper-module bundle's principle_refs. Treat it as component-level context unless the bundle is later updated through the JSON authority lane.

Evidence Contract

The fixture contract lives at core/fixture_manifests/self_ignorance_coverage_ledger.fixture_manifest.json. The active standard lives at standards/std_microcosm_self_ignorance_coverage_ledger.json. Together they admit public synthetic fixtures, copied source source bodies, hashes, anchors, validator refs, and generated result records. They forbid private repo bodies outside copied public fixtures, model-output data bodies, account secret or account-bound material, operator private notes, raw thread bodies, and result record body text for copied material.

The exported bundle manifest at examples/self_ignorance_coverage_ledger/exported_self_ignorance_coverage_ledger_bundle/source_module_manifest.json currently carries one source module: tools/meta/factory/build_system_atlas.py, copied into the bundle under source_modules/tools/meta/factory/build_system_atlas.py. The manifest records the source/target relation, digests, line count, required anchors System Atlas and kind, replacements, and the boundary that transform result records record hashes and replacement classes rather than source bodies.

The standard's result record contract requires a real runtime result record, a source-module manifest for the exported bundle, a secret-exclusion scan, at least the forbidden_absence_inference negative case, and body_in_receipt: false. Synthetic result records are not accepted as stand-ins for this component's authority.

Reader Evidence Routing

Read this module in this order:

1. paper_modules/self_ignorance_coverage_ledger.json for the generated paper-module projection and relationship edges.
2. core/paper_module_capsules.json::paper_modules[49:paper_module.self_ignorance_coverage_ledger] for source authority.
3. standards/std_microcosm_self_ignorance_coverage_ledger.json for the public/private boundary, validator contract, result record expectations, and scope limit.
4. src/microcosm_core/organs/self_ignorance_coverage_ledger.py for evaluate, evaluate_negative_case, run, and run_self_ignorance_bundle.
5. examples/self_ignorance_coverage_ledger/exported_self_ignorance_coverage_ledger_bundle/ for the current public evidence bundle.
6. tests/test_self_ignorance_coverage_ledger.py for proof consumers, bad cases, and perturbation cases.

Treat negative cases as part of the positive claim. The paper should cite only guards that the focused validation route blocks in the current checkout. The validated guard set must include forbidden absence inference, coverage mismatch, baked expected IDs without source, declared entity substitution, materialized count tamper, graph materialization tamper, graph builder tamper, projection protocol tamper, stale source self-reference, and digest mismatch. Fake-but-coherent standard entities remain a required unsourced-materialization guard target, but not an observed passing guard unless the focused test route blocks that perturbation.

Prior Art Grounding

The nearest ordinary analogue is software coverage measurement: coverage tools report what was exercised or missed over a declared surface, not all possible missing behaviors. coverage.py is useful as a reference pattern for bounded observed coverage over a source set.

The health-signal side is adjacent to automated repository checks such as OpenSSF Scorecard: bounded checks can produce useful risk signals without becoming complete security or quality proof. Microcosm applies that pattern to navigation coverage debt and keeps the scope boundary in the same result record frame as the count.

Validation Result record Path

From microcosm-substrate, run:

PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider tests/test_self_ignorance_coverage_ledger.py -q
PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check

Use a throwaway result record directory for manual bundle checks:

PYTHONPATH=src ../repo-python -m microcosm_core.organs.self_ignorance_coverage_ledger run-self-ignorance-bundle --input examples/self_ignorance_coverage_ledger/exported_self_ignorance_coverage_ledger_bundle --out /tmp/microcosm-self-ignorance-coverage-ledger/bundle --card

Passing validation proves that the declared public bundle, source-module manifest, negative cases, and paper-module corpus remain coherent. It does not establish freshness beyond the checked snapshot or authorize generated projection edits by hand.

proof_diagnostic_evidence_spine sits one step before formal proof authority. It holds diagnostic evidence from the formal-math evaluation and premise-retrieval pipeline as result record-backed cells, and refuses to let any of them be read as a proof.

Purpose

The component answers a single question: does a diagnostic check that claims to be backed by real Ring2 runtime evidence actually recompute against that evidence, or is it asserting more than its refs support? Without this membrane, a check row could name a failure-taxonomy report or a graph-update candidate set, declare itself passing, and be trusted on its own word. The spine refuses that.

What is unusual is that the validator does not trust the fixture's own pass label. It ignores the legacy expected_result field as a non-authoritative fixture label and rederives the verdict itself. For each check it resolves the named source_ref to a real file, re-hashes that file with sha256, and confirms the hash matches the expected digest. It then opens the named result record anchor and checks that the result record payload actually contains that source ref and digest. A check is accepted only when the source, the digest, and the result record all agree. The pass is a recomputation, not a claim copied from the fixture.

The second idea is that negative evidence is kept rather than hidden. A stale source fingerprint is recorded as source_fingerprint_status: stale and retained as diagnostic evidence; a provider advisory row is preserved as metadata while being rejected as authority; a forbidden proof-body field turns a row into a regression fixture rather than silently dropping it. The board shows what did not hold, which is the point of an evidence membrane.

Teleology

proof_diagnostic_evidence_spine is the body-safe evidence membrane before formal proof work. It records proof/evidence diagnostics while rejecting proof bodies, provider output bodies, source-authority upgrades, stale coupling, and runtime-correctness overclaims.

Public Contract

The validator consumes failure-taxonomy records, graph-update traces, verifier-trace repair artifacts, and formal evidence-cell anchor result record refs from the formal-math evaluation and premise-retrieval pipeline, then emits diagnostic result records over those refs. Provider-advisory rows are bounded evidence authority. Passing diagnostic checks do not become formal proof authority or formal-result correctness.

How a check is accepted

A check row carries three lists: source_refs, receipt_anchor_refs, and source_digest_refs. The validator does not take the row's word for whether it passes. It recomputes the verdict from the system.

For each source_ref it resolves a real file, reads it, and hashes the bytes with sha256. That hash must equal the expected digest the component holds for the ref. It then opens each result record anchor and checks that the result record payload actually contains the source ref and its digest, so a check is only "result record-backed" if the result record it cites genuinely references it. On top of that the component applies a semantic floor: a check whose id mentions a failure taxonomy must point at a source file that carries a failure-taxonomy report with representative failures and at a result record that carries a failure-mode ledger; a graph-update check needs graph-update candidates with ids and a matching result record anchor. The check is accepted only when every source resolves, every digest matches, every cited result record backs the ref, the semantic floor is satisfied, and no expected-negative error code is declared.

The concrete failure mode this guards against is a plausible-looking row that names real artifact paths but does not actually recompute: a digest that has drifted, a result record that does not mention the ref it claims, or a check labelled as failure-taxonomy evidence while pointing at an unrelated file. Each of those becomes a rejection finding rather than a silent pass. The recompute is also why a passing check stays bounded. It establishes that the named evidence is present and coupled, not that the underlying runtime is correct, which is why a row that adds claims_runtime_correctness is rejected as an overclaim.

Shape

flowchart TD Check["Diagnostic check row source_refs, receipt_anchor_refs, source_digest_refs"] Resolve["Resolve source ref to real public file"] Hash["Re-hash file (sha256) compare to expected digest"] Result record["Open result record anchor does payload contain this ref and digest?"] Floor["Semantic floor failure-taxonomy / graph-update source and result record match"] Accept["Accepted check verdict = recomputed, body_in_receipt false"] Reject["Rejected / retained as diagnostic evidence"] Stale["Stale source fingerprint"] Provider["Provider advisory payload"] Proofbody["Forbidden proof-body field"] Check --> Resolve --> Hash --> Result record --> Floor Floor -->|all agree| Accept Floor -->|any mismatch| Reject Stale -. retained as evidence .-> Reject Provider -. metadata kept, authority denied .-> Reject Proofbody -. scrubbed, kept as regression .-> Reject Accept --> Board["diagnostic_board.json evidence accounting only"] Reject --> Board Board -. denies .-> Ceiling["no Lean/Lake run, no formal-result correctness, no provider authority, no launch"]

Evidence/accounting refs:

• Bundle authority: core/paper_module_capsules.json::paper_modules[14] sets source_authority: json_capsule, names subjects proof_diagnostic_evidence_spine and mechanism.proof_diagnostic_evidence_spine.validates_ring2_diagnostic_evidence_membrane, resolves code_loci[0].path to src/microcosm_core/organs/proof_diagnostic_evidence_spine.py, and keeps generated_projections.markdown.generated: false, generated_projections.mermaid.status: available_from_capsule_edges, and generated_projections.atlas_card.status: linked_from_capsule_edges.
• Generated instance boundary: paper_modules/proof_diagnostic_evidence_spine.json::paper_module_payload.projection_contract records authority_flip_status: not_flipped, while paper_modules/proof_diagnostic_evidence_spine.json::relationships.edges carries source-justified links to the component, mechanism, concept, principles, axioms, dependencies, and code locus.
• Component/source locus: organs/proof_diagnostic_evidence_spine.json::organ_payload.source_atlas_row names the first command, claim_ceiling_restated, mechanism_refs[0], wires_to, and the same code-locus symbols implemented in src/microcosm_core/organs/proof_diagnostic_evidence_spine.py (PROOF_AUTHORITY_CEILING, EXPECTED_NEGATIVE_CASES, validate_copied_macro_body_artifacts, validate_evidence_receipts, validate_provider_payload_policy, validate_authority_ceiling, run, and run_evidence_bundle).
• Standard contract: standards/std_microcosm_proof_diagnostic_evidence_spine.json::authority_boundary_detail limits the component to copied Ring2 diagnostic runtime artifacts, summary metrics, graph-variant metadata, and anchor result record refs. Its body_import_verification.source_open_body_import_floor records 13 copied artifact bodies, 10 exact copies, 3 public-light edits, and body_text_exported_in_receipts: false; its body_import_verification.public_organ_source_body_floor records one exact copied public component source body.
• Bundle floor: examples/proof_diagnostic_evidence_spine/exported_evidence_bundle/bundle_manifest.json has schema_version: proof_diagnostic_evidence_spine_exported_evidence_bundle_v1, bundle_id: ring2_proof_diagnostic_evidence_runtime_example, copied_macro_body_artifacts count 13, and an scope limit of Ring2 diagnostic result record refs only, not formal proof authority.
• Source-body floor: examples/proof_diagnostic_evidence_spine/exported_evidence_bundle/source_body_floor/source_module_manifest.json::modules[0] records source ref src/microcosm_core/organs/proof_diagnostic_evidence_spine.py, source_to_target_relation: exact_copy, sha256_match: true, body_in_receipt: false, and omitted material including model-output data bodies, account or browser state, browser UI live-access state, recipient-send state, private proof bodies, and oracle-needed premise ids.
• Result record behavior: receipts/first_wave/proof_diagnostic_evidence_spine/proof_evidence_validation_receipt.json records accepted_count: 2, rejected_count: 1, missing_negative_cases: [], body_in_receipt: false, source_fingerprint_status: stale, and observed negative cases for source-authority upgrade, missing result record fields, runtime-correctness overclaim, provider/proof body rejection, and stale coupling. The sibling provider_payload_policy_result.json::provider_payload_policy preserves advisory metadata while rejecting the forbidden proof-body payload, and diagnostic_board.json::authority_ceiling rejects model-output data authority, source-authority upgrade, runtime-correctness claims, and formal prover execution.
• Focused regression surface: tests/test_proof_diagnostic_evidence_spine.py asserts the observed negative cases match EXPECTED_NEGATIVE_CASES and checks the exported evidence bundle path. These tests support reader wiring and evidence accounting only; they do not establish formal-result correctness, provider authority, runtime correctness, publishing-scope decision, or launch-scope decision.

Reader Evidence Routing

Route currentness questions through ## JSON Bundle Binding and the validation commands in ## Validation Result record Path. The tests and corpus check confirm reader wiring and projection health; they do not establish proof authority.

Route source/body-floor questions through ## Source-Open Body Floor and the fixture/example paths named under ## Structured Lattice Bindings. The diagnostic artifact copies from the formal-math evaluation pipeline, public component-source copy, manifests, and digest coupling are evidence-accounting inputs; they are bounded evidence bodies, model-output data bodies, runtime correctness claims, or source-authority upgrades.

Route claim-safety and public-copy questions through ## Scope limit, ## Evidence-As-Accounting Shape, and ## Scope boundary, then pair this module with batch12_release_claim_language_gate when public wording is being checked. If the question is "did the validator still enforce the membrane?", use the focused pytest and corpus check in ## Validation Result record Path before citing the reader page.

Evidence-As-Accounting Shape

This component is the proof-adjacent evidence membrane behind Microcosm's scope limits. It accepts diagnostic runtime artifacts, result record refs, source digests, and negative-case results as evidence cells, while refusing to treat any of them as theorem authority.

The accounting rule is two-sided. A copied artifact from the formal-math evaluation and premise-retrieval pipeline can strengthen only the diagnostic claim named by its result record, digest, and validator; it cannot upgrade itself into formal-result correctness, provider authority, launch-scope decision, or private-system equivalence. Stale source coupling is retained as diagnostic evidence instead of hidden, and provider-advisory rows remain metadata without payload bodies.

Use this module with batch12_release_claim_language_gate when evaluating public copy: the evidence spine says what result record-backed cells exist, and the language gate decides whether a public sentence stays within that ceiling.

Prior Art Grounding

The evidence spine is grounded in assurance-case practice: evidence should be connected to claims, assumptions, and limits before it is treated as support. NASA's Goal Structuring Notation example for spacecraft assurance is a useful public analogue because it frames assurance as model-structured evidence rather than document-level persuasion: NTRS 20160005295.

The result record membrane also borrows from W3C PROV and observability practice: diagnostic artifacts are evidence cells with provenance, not theorem authority. That is why the component accepts digest-coupled diagnostic refs and negative cases while rejecting proof bodies, model-output data bodies, and stale source-coupling overclaims.

Validation Result record Path

./repo-pytest tests/test_proof_diagnostic_evidence_spine.py -q --basetemp=/tmp/microcosm_proof_diagnostic_evidence_spine_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

Teleology

formal_math_readiness_gate is the public runtime cell that turns the formal math slice from a deferred slogan into an executable boundary. It validates synthetic readiness metadata for corpus availability, tactic probes, premise indexes, target-shape routing, and provider context recipes before any future Lean witness can claim authority.

The page should let a cold reader answer one question without rereading the component: what evidence has Microcosm actually validated, and where does that evidence stop?

Purpose

Formal-math tooling fails quietly when a library, tactic, or corpus is assumed present rather than checked. A pipeline that routes a proof to aesop when aesop is not actually available, or that treats a premise index as proof evidence because it happens to carry a proof body, has already lost the boundary between "ready to attempt" and "proven". This component exists to make that boundary explicit before any downstream proof work begins. It answers one question: which declared formal-math inputs are well-formed and honest enough that a later proof witness could safely consume them, and where exactly does that warrant stop?

The mechanism is a deterministic reducer over five public JSON inputs: corpus readiness, tactic-portfolio availability, a premise index, target-shape routing, and provider context recipes. It does not run Lean or Lake. Instead it reads what those inputs declare and refuses the specific ways they can lie. A corpus that claims Mathlib is available without a passing probe is rejected. A tactic marked available without a probe result record is rejected. A premise row carrying a proof_body or oracle_needed_premise_ids field is rejected. A route that admits a tactic the portfolio probe already marked unavailable is rejected. The output is a readiness board, not theorem evidence.

The design choice worth noticing is that the gate proves its own discipline through negative cases. Alongside the positive inputs, the fixture carries five inputs that each commit a known overclaim, and the run passes only when every one of those overclaims is caught and no unexpected finding appears. The gate is therefore not merely asserting "we check Mathlib availability"; it is demonstrating, on each run, that a falsified Mathlib claim is actually refused. A second guard keeps the floor source-open without leaking: copied prover probe bodies are verified by digest through a manifest, while proof bodies, model-output data, and private state stay out of the result records entirely.

Shape

flowchart TD Inputs["Five public JSON inputs corpus, tactics, premises, routes, provider recipes"] Scan["Secret-exclusion scan zero blocking hits required"] Corpus["validate_corpus_readiness reject Mathlib-availability overclaim"] Tactics["validate_tactic_portfolio each available tactic needs a probe result record"] Premises["validate_premise_index reject proof_body / oracle premise ids"] Routing["validate_target_shape_routing reject route admitting an unavailable tactic"] Provider["validate_provider_context_recipes reject over-budget or proof-body recipe"] SourceFloor["validate_source_module_imports copied probe bodies, digest-checked"] Reconcile["Reconcile findings vs EXPECTED_NEGATIVE_CASES every known overclaim must be caught"] Board["Readiness board + extension board available / blocked capabilities, counts"] Ceiling["Scope limit no Lean/Lake, proof, provider, launch, or private-system authority"] Inputs --> Scan Scan --> Corpus Scan --> Tactics Scan --> Premises Scan --> Provider Tactics -->|unavailable tactic ids| Routing Corpus --> Reconcile Tactics --> Reconcile Premises --> Reconcile Routing --> Reconcile Provider --> Reconcile SourceFloor --> Reconcile Reconcile --> Board Board --> Ceiling

The machine graph remains the generated paper_module.formal_math_readiness_gate.mermaid projection derived from the source record, not from this hand-authored Mermaid block.

Reader Evidence Routing

Read this module in evidence order:

1. Start at core/paper_module_capsules.json::paper_modules[21:paper_module.formal_math_readiness_gate]. That row names the source authority, subjects, mechanism refs, code locus, Microcosm concept/principle/axiom refs, generated projection statuses, and the bundle scope limit.
2. Check the generated structured source record paper_modules/formal_math_readiness_gate.json. Its relationships.edges cite the bundle source refs and show the generated Mermaid status, Atlas status, source_authority: json_capsule, and unresolved selective-relation count.
3. Inspect the runtime locus src/microcosm_core/organs/formal_math_readiness_gate.py, especially run, run_readiness_bundle, validate_source_module_imports, write_receipts, EXPECTED_NEGATIVE_CASES, AUTHORITY_CEILING, and SOURCE_MODULE_MANIFEST_NAME.
4. Use fixture evidence for the gate behavior: fixtures/first_wave/formal_math_readiness_gate/input, receipts/first_wave/formal_math_readiness_gate/readiness_gate_result.json, formal_math_readiness_board.json, formal_math_readiness_extension_board.json, formal_math_readiness_validation_receipt.json, and result records/sign-off/first_wave/formal_math_readiness_gate_fixture_acceptance.json.
5. Use exported-bundle evidence for source-open body-floor claims: examples/formal_math_readiness_gate/exported_formal_math_readiness_bundle/source_module_manifest.json, bundle_manifest.json, source_artifacts/, source_body_floor/source_modules/, and receipts/runtime_shell/demo_project/organs/formal_math_readiness_gate/exported_formal_math_readiness_bundle_validation_result.json.
6. Use tests/test_formal_math_readiness_gate.py for the behavioral result record boundary. The tests cover negative cases, exported bundle sign-off, source-module digest and target-ref mismatch rejection, bounded command-card output, source-body omission from result records, secret-exclusion/public-relative result record paths, and non-writing plan preview.

Do not route a proof claim through this page. It routes readiness evidence, result record integrity, and source-body-floor accounting only.

Technical Mechanism

The runtime is a deterministic readiness reducer over declared public inputs. run() evaluates the first-wave fixture directory with positive and negative JSON cases enabled; run_readiness_bundle() evaluates the exported public bundle without fixture-negative cases and requires the bundle source-module manifest. Both entrypoints call _build_result(), so the fixture and exported bundle result records share one scope limit, one secret scan, one source-module digest checker, and one readiness-board schema.

_build_result() first loads the five public input families: corpus_readiness.json, tactic_portfolio_availability.json, premise_index.json, target_shape_tactic_routing.json, and provider_context_recipes.json. It then scans those inputs plus any declared source artifacts through secret_exclusion_scan.scan_paths, using the public Microcosm forbidden-class policy. The scan is not advisory: the result can pass only when the scan has zero blocking hits, source-module imports pass, all expected fixture-negative cases are observed, and no unexpected positive-case findings remain.

The mechanism is split into six validators:

• validate_corpus_readiness() records Lean and Mathlib readiness metadata and adds lean_std_synthetic_core:mathlib to blocked capabilities when Mathlib is unavailable. A Mathlib availability claim without a passing probe becomes MATHLIB_AVAILABILITY_OVERCLAIM.
• validate_tactic_portfolio() separates available from unavailable tactics and requires every available tactic to carry a probe result record. Synthetic probe labels are accepted only when _tactic_probe_realness_evidence() binds them to copied source modules or fixture-manifest source-open evidence.
• validate_premise_index() admits premise rows as metadata only. It counts premises, namespaces, retrieval terms, and split eligibility, but rejects proof_body, ground_truth_proof, provider_output_body, and oracle_needed_premise_ids.
• validate_target_shape_routing() intersects each route case's allowed tactics with the unavailable tactics emitted by the portfolio validator. Any overlap becomes ROUTING_ALLOWS_UNAVAILABLE_TACTIC, so routing cannot silently re-enable a tactic that the probe plane blocked.
• validate_provider_context_recipes() records byte budgets and deliverable shape while rejecting public recipes over 32,768 bytes or recipes that allow proof bodies or provider-body material.
• validate_source_module_imports() verifies the exported bundle's source_module_manifest.json, target refs, source refs, line counts, target digests, source digests, exact-copy rows, and the two permitted private-path rewrites. It reports digest/ref failures without placing copied source bodies in result records.

After the validators run, _merge_observed() and _merge_findings() compare observed fixture failures against EXPECTED_NEGATIVE_CASES. This is the local scope limit: the fixture run must prove that the known overclaims are caught, while the exported-bundle run must prove that the positive public bundle has no unexpected findings. _build_extension_board() then projects the accepted metadata into the extension board: selected pattern ids, namespace and split counts, tactic availability counts, Mathlib-dependent unavailable tactics, blocked route cases, provider budgets, source-body import counts, the scope limit, and the scope boundary.

Result record writing preserves the same boundary. write_receipts() emits the gate result, readiness board, extension board, validation result record, and sign-off result record for fixture mode. run_readiness_bundle() emits the exported-bundle result record. The focused test suite asserts the mechanism rather than just file existence: it checks the five expected negative case ids, local Lean/Lake probe metadata with Mathlib unavailable, six available tactics with aesop blocked, eleven premises, five route cases, three provider recipes, thirteen verified source artifacts, source/target digest mismatch rejection, target-ref mismatch rejection, secret-exclusion/public-relative result record paths, and result record omission of copied body text.

Public Contract

The component does not run Lean or Lake. It consumes public JSON fixtures and exported bundles, records which capabilities are available or blocked, rejects Mathlib availability overclaims, rejects unprobed tactics, rejects premise rows that contain proof bodies, rejects routes that admit unavailable tactics, and rejects provider recipes that exceed the public budget or allow proof bodies.

The accepted result is a readiness board. That board can tell a later component what is safe to attempt, but it is bounded evidence evidence, benchmark evidence, or permission to execute a theorem prover.

Prior Art Grounding

This component is grounded in formal-math benchmark and environment-readiness work where the presence of a library, tactic, or corpus is not enough by itself. miniF2F motivates explicit benchmark split discipline for formal mathematics, LeanDojo motivates reproducible theorem-proving environments, and mathlib makes the availability of library imports a concrete precondition rather than a vague capability claim.

Microcosm borrows the readiness-gate pattern: corpus availability, Mathlib probes, tactic probes, premise indexes, target-shape routing, and context budgets must be checked before downstream proof or retrieval language is allowed. It excludes Lean execution or proof authority.

Runtime Surfaces

• python -m microcosm_core.organs.formal_math_readiness_gate run --input fixtures/first_wave/formal_math_readiness_gate/input --out receipts/first_wave/formal_math_readiness_gate
• python -m microcosm_core.organs.formal_math_readiness_gate run-readiness-bundle --input examples/formal_math_readiness_gate/exported_formal_math_readiness_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_readiness_gate
• python -m microcosm_core.organs.formal_math_readiness_gate plan --input fixtures/first_wave/formal_math_readiness_gate/input
• microcosm formal-math-readiness-gate run --input fixtures/first_wave/formal_math_readiness_gate/input --out receipts/first_wave/formal_math_readiness_gate
• microcosm formal-math-readiness-gate plan --input fixtures/first_wave/formal_math_readiness_gate/input

Relationship To Lean Witness

formal_math_lean_proof_witness remains deferred. This gate makes the deferral typed and testable: Mathlib is absent until a passing probe says otherwise, unavailable tactics cannot be routed, premise indexes cannot carry proof or oracle bodies, and provider recipes cannot smuggle proof-body deliverables.

Validation Result record Path

./repo-pytest tests/test_formal_math_readiness_gate.py -q --basetemp=/tmp/microcosm_formal_math_readiness_gate_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.relationships.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/formal_math_readiness_gate.json

Expected generated-row proof: edge_count: 15, mermaid_status: available_from_capsule_edges, atlas_status: blocked_until_organ_atlas_owner_lane_binds_edges, source_authority: json_capsule, and unresolved_selective_relation_count: 0.

Abstract

corpus_readiness_mathlib_absence_gate is the public formal-math corpus readiness boundary for Microcosm. It carries copied corpus/toolchain rows from the 2026-05-11 proof-state curriculum smoke run and forces Mathlib absence, absent-corpus blocking, consumer gate decisions, and source-module digest coupling to be visible before any downstream retrieval, tactic-routing, or proof-witness language is allowed.

Purpose

Formal-math agents fail in a specific way: they treat "there is a corpus" as if it meant "this corpus is usable for the proof route I am about to take". A roster lists miniF2F, PutnamBench, ProofNet, LeanDojo and Mathlib, the agent assumes the libraries are present, and the failure only surfaces later as a broken import or a tactic that needs a premise the host cannot resolve. This component answers one question before that happens: for each corpus, is it actually present on this host, and is the Mathlib import lane actually available, or not?

The unusual part is that the gate does not take the answer on trust. It runs a bounded Lean/Lake import probe in a temporary directory: one small file that imports Std and is expected to compile, and one that imports Mathlib and is expected to be rejected with the toolchain's own unknown module prefix 'Mathlib' error. A corpus is only marked usable for Mathlib-dependent work when the runtime evidence agrees the corpus exists, carries a Lake file, and the Mathlib lane probe passes. In the current system the Mathlib probe stays false, so every Mathlib-dependent consumer is blocked, and the one consumer that passes is the Lean3 translation smoke, which needs no Mathlib project at all.

This closes the most common way a readiness claim drifts. Stale alias fields such as mathlib_available, or a PASS lean status, cannot turn the gate green on their own; they must agree with the live probe or the row is flagged. The probe is deliberately narrow. It checks that imports resolve and that Mathlib is genuinely absent. It does not run a lake build, prove any theorem, or claim Mathlib is installed. The output is a readiness board and a set of blocked consumer verdicts, bounded evidence.

Shape

flowchart TD fixture["Fixture or exported bundle input corpus readiness rows + consumer gate cases"] probe["runtime_lean_import_probe lake env lean: Std compiles, Mathlib import rejected"] artifacts["validate_runtime_source_artifacts check SHA-256 digests, parse probe JSON"] mathlib{"Mathlib lane available? corpus exists + Lake file + probe passes"} corpus["validate_corpus_readiness 7 corpus rows, alias fields must agree with probe"] gates["validate_consumer_gate_cases derive verdicts from readiness facts"] imports["validate_source_module_imports 4 copied source artifacts, digest match"] allowed["Allowed: Lean3 translation smoke (needs no Mathlib project)"] blocked["Blocked: Mathlib-dependent and absent-corpus consumers"] result records["metadata-only result records result, board, validation, sign-off, bundle"] ceiling["Scope limit no Mathlib availability, proof, provider, launch"] fixture --> artifacts artifacts --> probe probe --> mathlib mathlib -->|no, probe false| corpus corpus --> gates gates --> allowed gates --> blocked fixture --> imports corpus --> result records gates --> result records imports --> result records result records --> ceiling

This reader diagram is intentionally smaller than the generated doctrine-lattice graph.

Mechanism

The mechanism is a readiness reducer, not a theorem-proving backend. The runtime entrypoints run and run_projection_bundle both call _build_result, which loads public fixture or exported-bundle inputs, scans those inputs against the non-public-state exclusion policy, verifies copied source artifacts, and then combines corpus readiness, consumer gate, source-module import, negative-case, and scope limit fields into one metadata-only result.

validate_runtime_source_artifacts anchors the reducer to four source refs: the corpus readiness rows, tactic-affordance probe, Mathlib import probe Lean file, and tactic portfolio availability JSON. It checks expected SHA-256 digests, parses the JSON source artifacts, and runs a bounded Lean/Lake import probe that can show Std imports and Mathlib remains absent without running a Lake build or exporting Lean bodies.

validate_corpus_readiness normalizes seven corpus rows against those runtime source artifacts. A corpus is usable for Mathlib-dependent work only when the runtime evidence says the corpus exists, has a Lake file, and mathlib_lake_project_import_available is true. In the current fixture and bundle evidence that field remains false, so Mathlib-dependent capabilities are blocked, absent corpora are recorded, and stale alias fields such as mathlib_available cannot turn the gate green.

validate_consumer_gate_cases then derives consumer verdicts from the normalized readiness facts instead of trusting expected-decision labels. The translation smoke consumer can pass because it does not require a Mathlib Lake project and names an available Lean3 reference corpus; Mathlib-dependent or absent-corpus consumers stay blocked. validate_source_module_imports adds the exported bundle floor by requiring the manifest class copied_non_secret_macro_body, material classes, target/source digest agreement, and no body material in result records.

The proof consumers are the two component commands, the focused regression test tests/test_corpus_readiness_mathlib_absence_gate.py, the paper-module corpus check, and the command-card surfaces emitted by result_card. Together they exercise the success path, contradictory Mathlib claims, consumer-gate skips, source digest tampering, private-path rewrites, runtime-probe blocks, and result record body exclusion. The resulting evidence relates the bundle's two mechanisms to concept.formal_math_and_proof_witness_bundle, P-8, and AX-7 by making readiness visibility a precondition for downstream formal-math claims while keeping the scope limit below theorem, provider, benchmark, or launch-scope decision.

Public Surfaces

• Component runner: python -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run --input fixtures/first_wave/corpus_readiness_mathlib_absence_gate/input --out receipts/first_wave/corpus_readiness_mathlib_absence_gate
• Exported bundle runner: python -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run-projection-bundle --input examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle --out receipts/runtime_shell/demo_project/organs/corpus_readiness_mathlib_absence_gate
• Standard: standards/std_microcosm_corpus_readiness_mathlib_absence_gate.json
• Source-module manifest: examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle/source_module_manifest.json
• Runtime result record: receipts/runtime_shell/demo_project/organs/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle_validation_result.json

Reader Evidence Routing

Read this module in five passes:

1. Start with the source record at core/paper_module_capsules.json::paper_modules[8:paper_module.corpus_readiness_mathlib_absence_gate]. It is the source authority that names source_authority: json_capsule, the component subject, two mechanism subjects, the resolved runtime code locus, the concept concept.formal_math_and_proof_witness_bundle, the dependency paper_module.tactic_portfolio_availability, P-8, and AX-7.
2. The reader proof is the current row shape: eight generated relationship edges, Mermaid available_from_capsule_edges, Atlas blocked_until_organ_atlas_owner_lane_binds_edges, and no unpopulated paper-module selective dependency residual for the tactic-portfolio edge. The structured source record is wiring evidence, not theorem-correctness, runtime-correctness, launch, provider, or production authority.
3. Inspect the runtime locus src/microcosm_core/organs/corpus_readiness_mathlib_absence_gate.py. The load-bearing symbols are run, run_projection_bundle, validate_corpus_readiness, validate_consumer_gate_cases, validate_source_module_imports, _build_result, write_receipts, result_card, EXPECTED_NEGATIVE_CASES, AUTHORITY_CEILING, SOURCE_MODULE_MANIFEST_NAME, BUNDLE_RESULT_NAME, and CARD_SCHEMA_VERSION.
4. For fixture evidence, use fixtures/first_wave/corpus_readiness_mathlib_absence_gate/input and the result records under receipts/first_wave/corpus_readiness_mathlib_absence_gate/ plus result records/sign-off/first_wave/corpus_readiness_mathlib_absence_gate_fixture_acceptance.json. The first-wave result result record records seven corpus rows, seven consumer cases, one allowed Lean3 translation-smoke case, six blocked absent or Mathlib-dependent cases, mathlib_lake_project_import_available: false, body_in_receipt: false, and the five negative cases mathlib_available_without_probe, consumer_skips_readiness_gate, private_corpus_source_ref, proof_body_leakage, and release_overclaim.
5. For exported-bundle evidence, use examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle/source_module_manifest.json and receipts/runtime_shell/demo_project/organs/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle_validation_result.json. The manifest verifies four copied source artifacts: corpus readiness JSON, tactic-affordance probe JSON, the Mathlib import probe Lean file, and tactic portfolio availability JSON. The exported result record records source_module_import_count: 4, copied_source_artifact_count: 4, source_modules_pass: true, body_in_receipt: false, and three blocked absent or Mathlib-dependent bundle consumer cases.

If a reader needs validation result records rather than prose, run the commands in ## Validation Result record Path, including the focused regression test and paper-module corpus check. Treat every result record as corpus-readiness boundary evidence only; it does not create Lean/Lake execution authority, Mathlib availability, theorem-proof authority, provider authority, private-system equivalence, or launch-scope decision.

Prior Art Grounding

This component is grounded in Lean corpus and neural theorem-proving work where library availability, premise access, and benchmark splits are part of the claim. The Lean mathematical library establishes Mathlib as a large community-maintained formal mathematics corpus, miniF2F gives a cross-system benchmark for formal Olympiad statements, and LeanDojo shows why reproducible corpus extraction and accessible-premise metadata matter for theorem-proving agents.

Microcosm borrows the readiness gate: corpus rows, Mathlib availability probes, blocked consumer cases, source-module digests, and negative leakage guards must be visible before retrieval, tactic-routing, or proof-witness language is allowed. It does not claim Mathlib is present or that any theorem was proved.

Research Bet

Formal-math agents fail when they treat "there is a corpus" as equivalent to "this corpus is usable for this proof route." This component makes that boundary runnable. It records seven corpus rows, blocks six absent or Mathlib-dependent consumer cases, allows only the Lean3 translation-smoke case, and keeps the Mathlib probe false until an actual passing probe is present.

The exported bundle carries four copied body artifacts: corpus readiness JSON, tactic-affordance probe JSON, the Mathlib import probe Lean file, and tactic portfolio availability JSON. Two rows are exact copies and two use a verified private-path rewrite. The result record records the manifest status, counts, material classes, digests, and metadata-only policy; the copied bodies stay under source_artifacts/, not inside result records.

Source-Backed Doctrine Binding

• Component: src/microcosm_core/organs/corpus_readiness_mathlib_absence_gate.py
• Bundle: core/paper_module_capsules.json#paper_module.corpus_readiness_mathlib_absence_gate
• Mechanism: core/mechanism_sources.json#mechanism.corpus_readiness_mathlib_absence_gate.validates_public_corpus_readiness_boundary
• Standard: standards/std_microcosm_corpus_readiness_mathlib_absence_gate.json
• Evidence class: core/organ_evidence_classes.json::corpus_readiness_mathlib_absence_gate records algorithmic_projection at rank 3.
• Source-module manifest: examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle/source_module_manifest.json
• Sign-off result records: receipts/first_wave/corpus_readiness_mathlib_absence_gate/* and result records/sign-off/first_wave/corpus_readiness_mathlib_absence_gate_fixture_acceptance.json

Cold-Agent Use

Open the source-module manifest first, then the runtime bundle result record, then the first-wave result result record. The useful claim is not that Microcosm has Mathlib or can prove downstream theorems. The useful claim is that Microcosm can force a formal-math route to expose corpus availability, Mathlib absence, consumer gating, source-module digest evidence, copied-body boundaries, negative-case result records, and an explicit scope boundary before any proof route is treated as usable.

Re-entry condition: the current atlas row already points at this paper module. After the sibling organ_atlas.json lane releases, bind this bundle's mechanism ref and code locus into the atlas row and rerun python -m microcosm_core.doctrine_lattice --check.

Validation Result record Path

Reader-verifiable commands, run from the microcosm-substrate/ public root:

PYTHONPATH=src python3 -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run \
  --input fixtures/first_wave/corpus_readiness_mathlib_absence_gate/input \
  --out /tmp/microcosm-corpus-readiness-mathlib-absence-vrp
PYTHONPATH=src python3 -m microcosm_core.organs.corpus_readiness_mathlib_absence_gate run-projection-bundle \
  --input examples/corpus_readiness_mathlib_absence_gate/exported_corpus_readiness_bundle \
  --out /tmp/microcosm-corpus-readiness-mathlib-absence-bundle-vrp
PYTHONPATH=src python3 scripts/build_doctrine_projection.py --check-paper-module-corpus
PYTHONPATH=src .venv/bin/python -m pytest -p no:cacheprovider --basetemp=/tmp/microcosm-corpus-readiness-mathlib-absence-tests -q tests/test_corpus_readiness_mathlib_absence_gate.py
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.paper_module_payload.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/corpus_readiness_mathlib_absence_gate.json

The fixture command writes the public corpus-readiness board, result result record, and validation result record. The bundle command validates the exported source-module manifest and metadata-only runtime result record. The corpus check and jq structured source record query prove the bundle-derived projection currentness without hand-editing generated JSON. The focused test keeps the Mathlib absence boundary, consumer gate cases, source-module digest checks, non-public paths rewrite policy, and scope boundary behavior from regressing.

Passing these commands does not establish Mathlib is installed, rerun Lean/Lake, validate downstream formal-result correctness, benchmark a corpus, authorize external model access, or approve launch; it only proves the bounded fixture and exported bundle result records preserve the declared readiness boundary.

mathematical_strategy_atlas_hypothesis_scorer is the public pre-oracle strategy layer for Microcosm formal-math work. It turns problem feature tags into an explicit strategy hypothesis before premise retrieval or proof execution, then records the result as redacted result records.

The point is not to prove anything. The point is to make the first mathematical move inspectable: an iff_goal shape selects iff_split, a recursive list shape selects recursive_data_induction, arithmetic normalization selects the arithmetic lens, and unmapped shapes become a typed STRATEGY_SELECTION_MISS instead of a hidden failure mode.

The current body-floor import carries eight copied source bodies: the prover graph benchmark harness, the provider result record reducer, their strategy-boundary regression tests, the compute-provider strategy classification standard, and three public runtime artifacts from PROVER_PROVIDER_CONTEXT_SWEEP_20260510_v0 (strategy_cards.json, strategy_hypothesis_set.json, and prover_skill_atlas.json). They live in source_artifacts/ under both the first-wave fixture input and the exported bundle; result records carry refs, counts, hashes, anchors, and verdicts instead of body text.

Purpose

A proof search has to start somewhere. Before any premise is retrieved or any tactic is run, an agent has already committed to a first move: a goal shape, a lens, a family of tactics it expects to use. That choice is usually implicit, buried inside a model call or a prompt. This component exists to pull it into the open. The single question it answers is: for a given problem shape, which strategy did the system pick first, and on what visible evidence?

The interesting part is what the answer is allowed to depend on. The scorer never sees the oracle's expected strategy, the ground-truth proof, or any provider output. It works only from public problem features and a strategy atlas of trigger features, negative triggers, and retrieval-expansion terms. The selected strategy is therefore a hypothesis, recomputed from inputs a cold reader can also read, not a result borrowed from the answer key.

That constraint is what the page guards. The common failure mode for a "strategy classifier" is to bake the answer in: declare the chosen strategy as a plain label, or score it on shallow feature overlap that happens to line up with the known-good label. The component rejects both. A declared selection must match the score the scorer recomputes from evidence, and a strategy chosen on overlap alone is a typed negative case rather than a pass.

Shape

The local component standard, when changing runtime behavior or the claim envelope, is standards/std_microcosm_mathematical_strategy_atlas_hypothesis_scorer.json; the general paper-module contract remains standards/std_microcosm_paper_module.json.

The diagram below traces the scorer's runtime flow inside that projection: how public inputs become a per-candidate score, how a selection or a typed miss is chosen, and how the result is recomputed and written as metadata-only result records under the scope limit.

flowchart TD subgraph Inputs["Public inputs"] atlas["strategy_atlas.json trigger / negative / retrieval terms"] features["problem_features.json feature tags, oracle hidden"] cases["hypothesis_cases.json candidate strategy ids"] end subgraph Scoring["Per-candidate scoring"] score["score = trigger_hits x4 - negative_hits x3 + retrieval_bonus (cap 2)"] rank["rank positive scores tie-break by order, then id"] end select{"any positive score?"} selected["selected_strategy_id + score components"] miss["STRATEGY_SELECTION_MISS (unknown)"] recheck["recompute vs declared selection / score / ranking"] result records["metadata-only result records refs, counts, hits, verdicts"] ceiling["Scope limit no Lean/Lake, oracle labels, external model access, or launch"] atlas --> score features --> score cases --> score score --> rank rank --> select select -- yes --> selected select -- no --> miss selected --> recheck miss --> recheck recheck --> result records result records --> ceiling

The generated instance currently exposes 19 concrete relationships.edges: two subject edges for the component and mechanism, one governing concept edge, six principle edges, six axiom edges, three sibling paper-module dependency edges, and one resolved code-locus edge into src/microcosm_core/organs/mathematical_strategy_atlas_hypothesis_scorer.py. relationships.unpopulated_selective_relations is empty, so the module-level unresolved selective-relation count available from this instance is 0.

Runtime evidence enters through the fixture input fixtures/first_wave/mathematical_strategy_atlas_hypothesis_scorer/input, the exported bundle examples/mathematical_strategy_atlas_hypothesis_scorer/exported_mathematical_strategy_atlas_bundle, and their copied source_artifacts/ / source_module_manifest.json bundles. The focused test file is tests/test_mathematical_strategy_atlas_hypothesis_scorer.py; result records include receipts/first_wave/mathematical_strategy_atlas_hypothesis_scorer/mathematical_strategy_atlas_result.json, mathematical_strategy_atlas_board.json, mathematical_strategy_atlas_validation_receipt.json, result records/sign-off/first_wave/mathematical_strategy_atlas_hypothesis_scorer_fixture_acceptance.json, and runtime-shell exported-bundle validation result records.

The honest ceiling is narrow by design: this module can say that public pre-oracle strategy hypotheses, retrieval-lens metadata, copied public source tool/standard/runtime bodies, source-artifact digests, and negative cases are inspectable. It cannot say that Lean or Lake ran, that a theorem was proved, that oracle labels or model-output data are visible, that benchmark performance is certified, that public sharing is approved, that launch is approved, or that the private root has been made public-safe.

How it works

The scorer reads three public inputs: a strategy atlas, a set of problem features, and a set of hypothesis cases. For each candidate strategy in a case it computes a single integer score from three terms. Each problem feature that matches a strategy's trigger_features adds four points. Each feature that matches the strategy's negative_triggers subtracts three. Retrieval-query terms that appear in the strategy's expansion terms add one point each, capped at two. Plain feature overlap is recorded as a diagnostic count but is deliberately kept out of the score.

Selection is then a deterministic sort. Only strategies with a positive score are eligible. Among those, the scorer ranks by score (highest first), breaking ties by the strategy's declared order and then its id, and takes the top row. If no candidate scores positive, the case resolves to the typed STRATEGY_SELECTION_MISS rather than guessing. The output for each case carries the selected id, the score, the component breakdown, the ranked candidate scores, and the trigger, negative, and retrieval hits that produced them, so the choice can be re-derived by hand.

The weights matter because they encode the design intent. Trigger matches are worth more than retrieval matches, so a strategy is chosen mainly for the shape it claims to handle, not for how many search terms happen to coincide. Negative triggers can veto a strategy that looks superficially apt. The retrieval cap stops a strategy from winning on keyword volume alone. A fixture that tries to score on overlap without these terms is caught by the superficial_overlap_only_scoring negative case.

The same recomputation is what enforces honesty. When a case declares its own selected_strategy_id, score, classifier, retrieval_bonus, or candidate_scores, the component recomputes each from the evidence and reports a stale-declaration finding on any mismatch. Declaring the selected strategy as a bare label, with nothing for the scorer to check against, is itself rejected: a label with no derivable evidence is not strategy evidence. Alongside this, the copied source artifacts are checked for leakage policy, so the strategy cards, hypothesis set, and skill atlas stay pre-oracle, free of proof bodies, and free of oracle strategy ids.

Reader Evidence Routing

Read this module as a pre-oracle strategy-hypothesis audit, not as a proof result. The primary reader path is:

• Start with strategy_atlas.json, problem_features.json, and hypothesis_cases.json to see how public feature tags select a strategy id before retrieval or proof execution.
• Check source_module_manifest.json and the copied source_artifacts/ bodies to verify that the imported source bodies are public tool/runtime bodies with exact digests, required anchors, and body-floor result records.
• Inspect the fixture and exported-bundle result records to confirm that strategy ids, retrieval-term effects, oracle-label exclusion, source-card consistency, and negative cases are checked without exposing proof bodies or model-output data.
• Use the structured source record only for structural lattice proof: it confirms bundle-backed subjects, code loci, doctrine refs, and dependency edges; it does not establish the scorer's correctness or any theorem.

Public Inputs

• strategy_atlas.json defines the known strategy enum, match features, and retrieval-term additions.
• problem_features.json carries synthetic public problem features with oracle labels hidden.
• hypothesis_cases.json validates deterministic pre-oracle strategy scoring.
• source_module_manifest.json binds copied source body files to exact source refs, SHA-256 digests, byte counts, line counts, material classes, and required anchors.
• Negative cases reject unknown strategy ids, proof bodies, oracle labels, post-oracle strategy selection, and launch/proof/provider overclaims.

Result records

The component emits:

• mathematical_strategy_atlas_result.json
• mathematical_strategy_atlas_board.json
• mathematical_strategy_atlas_validation_receipt.json
• mathematical_strategy_atlas_hypothesis_scorer_fixture_acceptance.json

Runtime-shell exported bundle validation writes exported_mathematical_strategy_atlas_bundle_validation_result.json.

Prior Art Grounding

The strategy atlas is grounded in the formal-methods practice of separating problem-shape classification from proof execution. Lean's tactic model, as introduced in Theorem Proving in Lean 4, gives the immediate precedent: proof work is often arrange around tactics chosen for a goal shape, while the kernel checks the final proof state. The mathlib overview also motivates explicit retrieval terms and domain tags because a large formal library is navigated by topic, structure, and reusable theorem families.

The atlas is also adjacent to hammer-style premise and method selection, such as Isabelle Sledgehammer, where a front-end tool searches for useful facts or proof methods before replay. This module keeps the pattern pre-oracle and metadata-only: it records why a first strategy hypothesis was selected, not whether the proof can be completed.

Validation Result record Path

Run from microcosm-substrate:

PYTHONPATH=src ../repo-python -m microcosm_core.organs.mathematical_strategy_atlas_hypothesis_scorer run \
  --input fixtures/first_wave/mathematical_strategy_atlas_hypothesis_scorer/input \
  --out /tmp/microcosm-mathematical-strategy-atlas-hypothesis-scorer/fixture \
  --card
PYTHONPATH=src ../repo-python -m microcosm_core.organs.mathematical_strategy_atlas_hypothesis_scorer run-strategy-bundle \
  --input examples/mathematical_strategy_atlas_hypothesis_scorer/exported_mathematical_strategy_atlas_bundle \
  --out /tmp/microcosm-mathematical-strategy-atlas-hypothesis-scorer/bundle \
  --card
PYTHONPATH=src ../repo-python -m pytest -p no:cacheprovider tests/test_mathematical_strategy_atlas_hypothesis_scorer.py -q
PYTHONPATH=src ../repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

A green result record proves only pre-oracle strategy-hypothesis metadata, copied public source tool bodies, source artifact digests, and negative-case enforcement; it does not run Lean or Lake, prove formal-result correctness, reveal oracle labels, export proof bodies, use external model services, certify benchmark performance, authorize public sharing, or include launch operations.

tactic_portfolio_availability_probe is the public component that turns tactic callability into an explicit artifact before routing or proof search treats a tactic as usable.

The fixture is copied from real source system: the 2026-05-11 PROVER_PROOF_STATE_SEARCH_CURRICULUM smoke run's Lean/Std tactic affordance probe. It records compile-status rows for rfl, decide, omega, simp, simp_all, grind, native_decide, and aesop, with source digests for the run-level affordance probe, the portfolio_core_v0 tactic availability artifact, and the paired corpus-readiness boundary. The Mathlib-dependent aesop row is marked environment_fail because the paired environment probe reports mathlib_lake_project_import_available=false.

The component validates:

• every tactic has an environment-scoped compile_status;
• Mathlib-dependent tactics are not marked available without a passing Mathlib import probe;
• downstream consumers reference only tactics present in the probe portfolio;
• proof bodies, raw model-output data, benchmark claims, launch-scope decision, and non-public paths stay out of the public artifact.

The generated board is a callability map, bounded evidence evidence. It can make target-shape routing cheaper and more honest, but it cannot prove a goal, widen Lean/Lake authority, use external model services, claim benchmark performance, or include launch operations.

The result record contract reports body_material_status=copied_non_secret_macro_body_with_provenance, tactic_availability_status=real_lean_std_tactic_affordance_probe_rows, source digests, target refs, and secret_exclusion_scan. It does not use body-redaction or non-public-state-scan grammar as product evidence.

Purpose

A tactic name is not a usable tactic. aesop is callable only if the surrounding Lean and Std environment actually carries the imports it needs; omega is callable in one project layout and not in another. Routing or proof search that trusts a bare tactic name will reach for tactics that the current environment cannot run, and then misread the resulting failure as a property of the goal rather than a property of the environment. This component answers one question: in the observed Lean/Std environment, which tactics were actually callable, and on what evidence?

The interesting part is how it treats failure. A copied probe row that reports a Lean FAIL is not flattened into a single "unavailable" verdict. When a tactic declares requires_mathlib and the paired environment probe reports that the Mathlib import is absent, the failure is classified as environment_fail with the reason MATHLIB_IMPORT_MISSING. The same Lean FAIL for a tactic that does not depend on Mathlib is classified as compile_fail. The distinction keeps a missing import from masquerading as a broken tactic, and it preserves Mathlib absence as a recorded fact about the environment rather than discarding it. A downstream router can then re-attempt the same tactic in a different environment instead of striking it off permanently.

The second deliberate choice is that none of this is a measurement of quality. The component copies probe durations and bands them as fast, moderate, or slow so a router can prefer a cheaper available tactic, but the latency profile is stamped as environment-scoped, not benchmark authority. Callability and speed in one observed environment are useful for cheaper routing; they are explicitly not evidence that a tactic is correct, that a goal was proved, or that Lean was rerun by this component.

Shape

flowchart TD A["Copied Lean/Std affordance probe rows (compile_status, requires_mathlib, duration_ms)"] --> B["tactic_portfolio_availability_probe"] C["Environment probe mathlib_lake_project_import_available"] --> B B --> D{"Copied compile_status"} D -->|PASS| E["available band duration fast / moderate / slow"] D -->|FAIL + requires_mathlib + Mathlib absent| F["environment_fail reason MATHLIB_IMPORT_MISSING"] D -->|FAIL otherwise| G["compile_fail"] E --> H["Availability board for target-shape routing"] F --> H G --> H I["Downstream tactic reference"] --> J{"Tactic in probed portfolio?"} J -->|no| K["Rejected: unprobed tactic referenced"] J -->|yes| H B --> L["metadata-only fixture and bundle result records no proof, Lean, or provider bodies"] L --> M["Generated paper-module row and validation result records"]

The flow is deliberately smaller than the generated doctrine-lattice graph.

Reader Evidence Routing

Read this page in four passes:

1. Start with the bundle source row at core/paper_module_capsules.json::paper_modules[40:paper_module.tactic_portfolio_availability]. It names the public component subject, mechanism subject, resolved code locus, Microcosm concept, governing principles, axioms, and sibling paper-module dependencies that generate the relationship edges.
2. Inspect the runtime system at src/microcosm_core/organs/tactic_portfolio_availability_probe.py. The load-bearing symbols are run, run_availability_bundle, _build_result, _write_receipts, EXPECTED_NEGATIVE_CASES, and AUTHORITY_CEILING; those are the code-loci symbols that make the paper module about an executable component instead of a prose topic.
3. Reproduce the evidence floor with the fixture input fixtures/first_wave/tactic_portfolio_availability_probe/input, the exported bundle examples/tactic_portfolio_availability_probe/exported_tactic_portfolio_availability_bundle, the focused test tests/test_tactic_portfolio_availability_probe.py, and the paper-module corpus check. Treat the result records as environment-scoped tactic-callability evidence only; validation result records do not widen the proof boundary, scope limit, launch posture, provider posture, or benchmark posture.

Prior Art Grounding

The module is patterned after feature-detection probes and proof-assistant tactic inventories. GNU Autoconf's configure workflow established the habit of testing local capability before relying on it; Lean's tactic documentation shows that tactic use is environment- and goal-sensitive, so a tactic name is not enough to justify downstream routing. This component applies that older probe discipline to Microcosm: it records which tactics were callable in the observed Lean/Std environment and preserves Mathlib-dependent absence as evidence, without treating callability as proof quality.

Prior-art anchors:

• GNU Autoconf feature/configuration probing: https://ftp.gnu.org/old-gnu/Manuals/autoconf-2.57/html_chapter/autoconf.html
• Lean 4 tactic documentation: https://lean-lang.org/theorem_proving_in_lean4/Tactics/

Primary commands:

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary result records:

The expected projection row is paper_module.tactic_portfolio_availability with 18 generated relationship edges, no unpopulated selective relations, Mermaid status available_from_capsule_edges, and Atlas status linked_from_capsule_edges. These checks validate environment-scoped tactic availability rows and bundle result records only; they do not turn callability into proof quality, benchmark performance, Mathlib proof authority, or launch-scope decision.

target_shape_tactic_routing_gate is the public Microcosm component for the pre-execution tactic admissibility layer.

It turns real problem-domain, failure-class, and graph-update candidate refs from the formal-math evaluation pipeline into route decisions: which tactics are admitted, which are rejected as unavailable, which are rejected as unprobed, and which are rejected because they do not match the declared goal shape.

Purpose

A proof attempt is expensive, and most of that cost is spent on tactics that were never going to work: tactics the environment cannot run, tactics absent from the probe portfolio, or tactics that do not match the shape of the goal. This component answers one question before any Lean call is made: given the target shape and the current availability probe, which tactics may a route even attempt?

The decision is deliberately made early. Routing happens before execution, so a case that carries Lean result records, execution results, or a post-execution stage is rejected outright rather than trusted. The point is to decide admissibility from evidence that already exists, not from the outcome of the attempt the gate is meant to filter.

What is unusual is that the gate recomputes the choice rather than accepting the declared one. Each target shape carries a small preferred-tactic order (for example omega for integer linear arithmetic, decide for closed natural-number decisions). The gate walks that order, skips any preferred tactic that is unprobed or unavailable, records why it skipped, and falls back to the next allowed candidate or to a default safe order for shapes it does not recognise. A route whose declared selection disagrees with this computed preference is flagged rather than honoured. The route is a claim about what should run; the gate treats it as something to check, not something to believe.

Shape

flowchart TD Bundle["JSON bundle paper_module.target_shape_tactic_routing"] structured source record["Generated structured source record paper_modules/target_shape_tactic_routing.json"] Component["Runtime component target_shape_tactic_routing_gate.py"] Portfolio["Tactic probe portfolio available/unavailable tactic ids"] Routes["Target-shape route cases pre_execution selected tactics"] SourceFloor["Copied Ring2 source artifacts 4 body imports, body_in_receipt=false"] Decisions{"Route admissible before proof execution?"} Result records["Result records result, board, validation, sign-off"] Tests["Focused tests negative cases and digest checks"] Ceiling["Scope limit no Lean/Lake, proof, provider, post-execution, launch"] Bundle --> structured source record Bundle --> Component Component --> Portfolio Component --> Routes Portfolio --> Decisions Routes --> Decisions SourceFloor --> Decisions Decisions --> Result records Tests --> Result records Result records --> Ceiling

Technical Mechanism

The named mechanism mechanism.target_shape_tactic_routing_gate.validates_public_tactic_routing_boundary is a fail-closed scorer over two public input planes: the tactic probe portfolio and the target-shape route cases. _build_result loads the fixture or exported bundle payloads, scans the inputs and copied source artifacts for forbidden body material, derives known/available/unavailable tactic sets, scores every route case, checks copied Ring2 source-artifact digests, and emits metadata-only result, board, validation, and sign-off result records.

For each route case, _decision_for_tactic rejects a candidate before selection if the tactic id is absent from the public probe portfolio, marked unavailable, or outside the case's declared allowed_tactic_ids. Only a tactic that is probed, available, and target-shape-admissible can receive TARGET_SHAPE_ADMISSIBLE. _shape_preferred_selection then applies the local target-shape preference map, records the unknown-shape default fallback when no specific map exists, and records the preferred-unavailable fallback when the first preferred tactic is known but not usable. _route_integrity_findings turns any unavailable admission, unprobed admission, post-execution route, or declared-selection mismatch into typed findings.

The proof consumer is tests/test_target_shape_tactic_routing_gate.py: it asserts seven pre_execution route cases, shape-preferred selection for the real Ring2 cases, unknown-shape and unavailable-Mathlib fallback behavior, rejection of mutated shape and availability inputs, exported-bundle sign-off, four copied source artifacts with digest verification, compact card omission of the full routing board, and result record text without non-public paths or body fields. Those tests consume the same fixture and exported-bundle surfaces named by the mechanism row, so this page's evidence is the runnable route-reference and result record contract rather than a prose-only claim.

The governing lattice stays explicit: the bundle binds the module to concept.formal_math_and_proof_witness_bundle, principles P-1, P-2, P-3, P-6, P-8, and P-9, axioms AX-1, AX-2, AX-5, AX-7, and AX-8, and dependency modules for tactic portfolio availability, formal-math readiness, proof-diagnostic evidence, verifier-trace repair, and formal evidence-cell anchor resolution. The standard narrows that lattice to one allowed claim: public pre-execution route cases may admit only tactics that were both probed and available before proof execution. The same standard forbids widening this mechanism into formal-result correctness, Lean/Lake execution, external model access, proof or provider body export, post-execution route authority, publishing-scope decision, or launch-scope decision.

Evidence/accounting:

• Bundle authority: core/paper_module_capsules.json::paper_modules[41:paper_module.target_shape_tactic_routing] names source_authority: json_capsule, subjects component:target_shape_tactic_routing_gate and mechanism.target_shape_tactic_routing_gate.validates_public_tactic_routing_boundary, the resolved code locus src/microcosm_core/organs/target_shape_tactic_routing_gate.py, and generated projection statuses mermaid.status: available_from_capsule_edges plus atlas_card.status: linked_from_capsule_edges.
• Generated structured source record: paper_modules/target_shape_tactic_routing.json carries relationships.edges for the bundle subjects, concept/principle/axiom refs, dependency paper modules, and code locus; relationships.unpopulated_selective_relations: []; and scope boundaries that the JSON row does not establish runtime correctness, launch-scope decision, or whole-system completeness.
• Runtime contract: standards/std_microcosm_target_shape_tactic_routing_gate.json limits the allowed claim to pre-execution tactic admission from probed, available tactics; its required_fields bind tactic_portfolio_availability.tactics[].tactic_id, availability_status, target_shape_routes.route_cases[].target_shape, allowed_tactic_ids, selected_tactic_id, and route_stage.
• Source-body accounting: examples/target_shape_tactic_routing_gate/exported_target_shape_tactic_routing_bundle/source_module_manifest.json records source_import_class: copied_non_secret_macro_body, module_count: 4, body_in_receipt: false, three verified_public_safe_private_path_rewrite rows, and one exact_copy row.
• Fixture/bundle behavior: examples/target_shape_tactic_routing_gate/exported_target_shape_tactic_routing_bundle/target_shape_routes.json has seven pre_execution route cases, while tactic_portfolio_availability.json marks decide, omega, simp_all, and rfl available and aesop unavailable.
• Result record floor: receipts/first_wave/target_shape_tactic_routing_gate/target_shape_tactic_routing_result.json, target_shape_tactic_routing_board.json, target_shape_tactic_routing_validation_receipt.json, and result records/sign-off/first_wave/target_shape_tactic_routing_gate_fixture_acceptance.json report status: pass, route_case_count: 7, copied_source_artifact_count: 4, source_artifacts_pass: true, missing_negative_cases: [], secret_exclusion_scan.blocking_hit_count: 0, and authority flags with Lean/Lake, proof, provider, post-execution routing, and launch-scope decision set false.
• Test boundary: tests/test_target_shape_tactic_routing_gate.py checks observed negative cases, shape-preferred selection, unknown-shape and Mathlib-unavailable fallback, exported-bundle sign-off, source-module digest verification, compact card omission of full boards, and result record output without non-public paths or body fields.

Reader Evidence Routing

Read this module as a pre-execution admissibility gate, not as a proof attempt. The primary reader path is:

• Start with the problem-domain, failure-class, graph-update candidate, and tactic-probe refs in the fixture input. They are the public route evidence the gate is allowed to inspect before any Lean/Lake work in the formal-math evaluation and premise-retrieval pipeline.
• Compare each target-shape route case against the selected tactic ids and rejection reasons: admitted tactics must match both the declared goal shape and the public availability probe.
• Inspect negative cases before the happy path. The important behavior is that unavailable tactics, unprobed tactics, proof/provider body leakage, post-execution routing, and launch overclaims all fail closed.
• Use the structured source record only for structural lattice proof: it confirms subjects, code loci, doctrine refs, and dependency edges; it does not establish the tactic route can solve the target.

Runtime Surfaces

PYTHONPATH=src python3 -m microcosm_core.organs.target_shape_tactic_routing_gate run --input fixtures/first_wave/target_shape_tactic_routing_gate/input --out receipts/first_wave/target_shape_tactic_routing_gate
PYTHONPATH=src python3 -m microcosm_core.cli target-shape-tactic-routing-gate run-routing-bundle --input examples/target_shape_tactic_routing_gate/exported_target_shape_tactic_routing_bundle --out receipts/runtime_shell/demo_project/organs/target_shape_tactic_routing_gate

Negative Cases

• unavailable_tactic_admitted rejects an aesop route while Mathlib is absent.
• unprobed_tactic_allowed rejects a tactic absent from the public probe portfolio.
• proof_body_leakage rejects proof/provider/Lean body fields.
• post_execution_route rejects route selection after execution evidence.
• release_overclaim rejects proof, provider, Lean/Lake, public sharing, and launch-scope decision overclaims.

Prior Art Grounding

The routing layer follows established proof-search and policy-gating patterns: match a goal shape to methods that are known to be available before spending runtime on them. Lean's tactic documentation supplies the local proof-assistant context for goal-directed tactic choice, while Isabelle/Sledgehammer represents a mature prior-art pattern for selecting external provers and relevant facts from a goal. Microcosm narrows that idea to a pre-execution admissibility filter: target shape, allowed references, and current tactic availability must line up before a tactic route can be exported.

Prior-art anchors:

• Lean 4 tactic documentation: https://lean-lang.org/theorem_proving_in_lean4/Tactics/
• Isabelle Sledgehammer user guide: https://isabelle.in.tum.de/doc/sledgehammer.pdf

Why It Matters

After corpus readiness and strategy scoring, Microcosm needs a visible gate that prevents wasted or misleading proof attempts. This component shows that gate over the formal-math evaluation and premise-retrieval pipeline already feeding verifier repair, evidence anchoring, and proof diagnostics: a tactic is not tried just because it exists; it is admitted only when the target shape and the public availability probe both allow it.

Validation Result record Path

From microcosm-substrate/, reproduce this page's proof boundary with temporary result records:

These checks validate route-reference fixture and bundle result records only; they do not widen the no-Lean/no-proof scope limit.

lean_std_premise_index is the closed public premise-index lane for the formal-math slice. It validates premise metadata and selected Ring2 premise-retrieval source result record bodies that a cold reader can inspect without importing Mathlib, exposing proof bodies, or relying on private source run state.

Purpose

A premise index is the catalogue a theorem-proving system reads before it tries to prove anything: a list of the named lemmas and definitions it is allowed to cite, with enough metadata to retrieve the relevant ones. This component answers a narrower question. Given that such an index already exists inside a private Ring2 benchmark run, can a cold reader inspect its public shape and be sure that what they are reading is a faithful copy of the real thing, and not a separate hand-written stand-in?

The answer rests on one design choice that is worth noticing. The validator does not just describe eleven premise rows; it opens the declared source artifact from the Ring2 premise-retrieval run, recomputes its SHA-256, and checks every public row against the matching source row by premise_id. The only permitted difference is a path rewrite: a raw Lean toolchain path becomes a public lean-toolchain://.../Init/... reference, so the reader sees where a lemma lives in the standard library without seeing a private filesystem. If the public catalogue ever drifts from the source it claims to copy, the digest or the row-signature comparison fails and the result record is blocked.

The interesting tension is the line between a useful index and a leaked answer key. A premise index for a benchmark is one edit away from telling a solver exactly which lemmas it needs. So the same pass that admits names, namespaces, retrieval terms, and train/dev/test eligibility rejects the things that would turn the catalogue into proof authority: Mathlib references, proof bodies, the oracle-needed premise ids that name the answer, and any flag that authorises tuning on the test split. The catalogue stays inspectable precisely because those are kept out.

Shape

This module is a cold-reader map from a JSON bundle and copied public Lean/Std premise artifacts into metadata-only validation result records. The readable path is bundle -> generated instance/status -> runtime validator -> fixtures and exported source bundle -> tests and result records -> scope limit; none of those projections expands the closed-index boundary.

flowchart TD bundle["core/paper_module_capsules.json paper_module.lean_std_premise_index source basis: source record"] instance["paper_modules/lean_std_premise_index.json generated instance from source record Markdown stays reader projection"] generated["Generated status Mermaid: available_from_capsule_edges Atlas: blocked_until_organ_atlas_owner_lane_binds_edges"] runtime["src/microcosm_core/components/lean_std_premise_index.py run / run_index_bundle / scope_limit"] standard["standards/std_microcosm_lean_std_premise_index.json closed Lean/Std premise-index contract"] fixtures["fixtures/first_wave/lean_std_premise_index/input projection_protocol, premise_index, index_policy, negative cases"] bundle["examples/lean_std_premise_index/exported_lean_std_premise_index_bundle source_module_manifest: 6 copied body modules"] tests["tests/test_lean_std_premise_index.py fixture, manifest, bundle, and runtime-shape checks"] result records["result records/first_wave/lean_std_premise_index result records/runtime_shell/demo_project/components/lean_std_premise_index"] ceiling["Scope limit no Lean/Lake, Mathlib, proof bodies, providers, benchmark authority, source-file changes, public sharing, or launch-scope decision"] bundle --> instance instance --> generated standard --> runtime fixtures --> runtime bundle --> runtime runtime --> tests tests --> result records generated --> ceiling result records --> ceiling

Technical Mechanism

The mechanism is a two-entry validator over copied public artifacts, not a proof engine. run reads the first-wave fixture inputs, opens the declared source premise-index source artifact, verifies the declared source_sha256, normalizes Lean toolchain paths into lean-toolchain://.../Init/... public refs, compares every public row against the source row signature, and then checks the protocol, policy, copied-material contract, namespace coverage, split coverage, negative cases, secret exclusion scan, and scope limit before writing metadata-only result, board, validation, and sign-off result records. run_index_bundle applies the same public boundary to the exported bundle and requires the source-module manifest to verify six copied body-material files by source ref, target ref, digest, line count, byte count, and source-to-target equivalence while keeping body text out of result records.

The proof consumer is therefore concrete and local: tests/test_lean_std_premise_index.py asserts that the validator observes all five negative cases, imports the real Ring2 premise-index source artifact, rejects digest, row-count, row-signature, source-ref, source-module digest, and rehash-body-swap mutations, and validates the runtime-shell bundle shape. The positive fixture carries 11 premise rows across Nat, Bool, List, and Iff; the source-open body floor carries one normalized Lean/Std premise index plus five Ring2 source result record or pattern bodies. This is evidence of a bounded public premise catalog and copied-source manifest, not evidence of Lean formal-result correctness.

The governing lattice is source-backed through the bundle-generated instance: paper_module.lean_std_premise_index explains the lean_std_premise_index component and the two mechanism.lean_std_premise_index.* mechanisms, is governed by concept.formal_math_and_proof_witness_bundle, cites P-1, P-2, P-3, P-6, and P-8, abides by AX-1, AX-2, AX-5, and AX-7, and depends only on paper_module.formal_math_premise_retrieval.

Inputs

• projection_protocol.json records source pattern ids, source source refs, public replacement refs, projection result records, omitted material, and copy policy.
• premise_index.json carries public metadata rows: premise id, declaration name, namespace, Init/ source ref, retrieval terms, and split eligibility.
• index_policy.json keeps the closed-index scope limit explicit.
• source_module_manifest.json records six source-open body imports: the normalized Lean/Std premise index plus five exact bodies from the formal-math premise-retrieval pipeline (source result records and graph-pattern bodies) under source_modules/.

Prior Art Grounding

This component is grounded in formal-library indexing and premise-selection work. The Lean mathematical library anchors the library-as-corpus side, while LeanDojo and HOList anchor the need for premise metadata, retrieval splits, and theorem-proving environments that can be inspected by learning systems.

Microcosm borrows the closed-index discipline: premise ids, declaration names, namespaces, source refs, retrieval terms, split eligibility, and source-module digests are public metadata, while proof bodies and oracle-needed ids remain outside the public boundary. It does not import Mathlib or prove theorems.

Negative Cases

The fixture rejects:

• Mathlib premise refs;
• proof-body leakage;
• oracle-needed premise ids;
• test-split tuning authority;
• namespace rows without Init/ source refs.

These are stable negative cases because the index is intended to be useful without becoming proof authority.

Result records

The validator emits:

• lean_std_premise_index_result.json;
• lean_std_premise_index_board.json;
• lean_std_premise_index_validation_receipt.json;
• an sign-off result record under result records/sign-off/first_wave/.

Runtime-shell execution emits exported_lean_std_premise_index_bundle_validation_result.json after checking the source-module manifest, target file digests, line counts, byte counts, and secret-exclusion boundary.

Reader Evidence Routing

• Start with the JSON Bundle Binding to identify the source row, generated instance, and scope limit.
• Use Structured Lattice Bindings only as navigation evidence; the resolved dependency edge points to the premise-retrieval module and does not expand the closed-index proof boundary.
• Use Inputs and Result records when checking whether public metadata, copied body manifests, and runtime-shell validation stayed body-safe.
• Use Negative Cases and Scope limit together when deciding whether a proposed public claim exceeds the closed-index boundary.

Validation Result record Path

./repo-pytest tests/test_lean_std_premise_index.py -q --basetemp=/tmp/microcosm_lean_std_premise_index_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

formal_math_premise_retrieval is the source-available first real formal-math import slice after the source projection protocol. It turns the source prover lab's premise-index, term-scoring, context-budget, and strategy-selection patterns into a runnable Microcosm component.

It is still deliberately below proof authority. It validates:

• Lean/Std premise metadata;
• query term scoring across public premise ids, namespaces, declaration names, statement excerpts, and retrieval terms;
• split eligibility;
• context recipe budgets;
• public strategy ids;
• redacted result records;
• negative cases.

It does not run Lean or Lake, use external model services, expose proof bodies, expose oracle-needed premise ids, tune on test split truth, claim formal-result correctness, or include launch operations.

Purpose

Before a model can attempt a formal proof, it has to find the right lemmas. A Lean library holds thousands of theorems and definitions, and the useful ones for a given goal are a handful. Premise selection is the step that narrows that library down to candidates worth putting in front of a prover. This component is the smallest honest version of that step: it takes a query, scores every public premise against it, and returns a ranked shortlist.

The single question it answers is narrow and checkable: given a copied catalogue of public Lean/Std premise metadata, does a transparent term-scoring retrieval return the premises a query should find, without ever touching a proof? Both halves matter. The retrieval has to actually work, so each fixture query carries the premise ids it is expected to surface and the run fails if the shortlist misses them. And the boundary has to hold, so the same run refuses any input that smuggles in a proof body, an oracle answer, or test-split truth.

What is unusual is the restraint. The retrieval index is not a learned embedding model and the scoring is not a benchmark claims. It is plain term overlap over fields that a reader can inspect: premise ids, namespaces, declaration names, statement excerpts, and retrieval terms. The interesting claim is therefore not "this retrieves well" but "this retrieves over real, copied Lean metadata and can be audited end to end, and the design forbids the shortcuts that would make a premise-selection result look better than it is".

Shape

flowchart TD bundle["JSON source record paper_module.formal_math_premise_retrieval"] --> instance["Generated paper-module instance 15 relationship edges"] instance --> component["Runtime component formal_math_premise_retrieval.py"] subgraph Inputs["Public inputs"] index["Premise index copied Lean/Std metadata"] queries["Retrieval queries terms, split, strategy, top_k"] recipes["Context recipes byte budgets"] negatives["Negative-case inputs proof body, oracle ids, test-split tuning, budget, strategy"] end component --> index component --> queries component --> recipes component --> negatives index --> split["Split gate skip premises not in allowed_for_split"] queries --> split split --> score["Term-overlap scoring shared tokens + strategy bonus"] score --> shortlist["Ranked top_k shortlist"] shortlist --> recall["Recall check vs expected premise ids"] negatives --> reject["Required rejections five leakage/overclaim guards"] recipes --> reject recall --> result records["metadata-only result records board, validation, sign-off"] reject --> result records result records --> ceiling["Scope limit metadata coherence, no Lean/Lake, no proof"]

Evidence/accounting:

• Bundle authority: core/paper_module_capsules.json::paper_modules[25:paper_module.formal_math_premise_retrieval] has source_authority: json_capsule, three subjects, one resolved code_loci[0].path, depends_on naming paper_module.formal_math_lean_proof_witness, and generated projection statuses for Markdown, Mermaid, and Atlas.
• Generated instance: paper_modules/formal_math_premise_retrieval.json::paper_module_payload repeats the bundle authority_ceiling, reports Mermaid status available_from_capsule_edges, and derives 15 relationships.edges with relationships.unpopulated_selective_relations: [].
• Component atlas: core/organ_atlas.json::organs[9:formal_math_premise_retrieval] classifies the component in family: formal_math_and_proof, cites the runtime locus, and restates that retrieval metadata coherence is not Lean/Lake, provider, theorem-correctness, benchmark, or launch-scope decision.
• Mechanism rows: core/mechanism_sources.json::mechanisms[27:mechanism.formal_math_premise_retrieval.validates_public_premise_retrieval_slice] and core/mechanism_sources.json::mechanisms[37:mechanism.formal_math_premise_retrieval.validates_public_premise_retrieval_projection] point at src/microcosm_core/organs/formal_math_premise_retrieval.py and name first-wave, sign-off, and runtime-shell result record refs.
• Runtime and tests: src/microcosm_core/organs/formal_math_premise_retrieval.py exposes run, run_retrieval_bundle, EXPECTED_NEGATIVE_CASES, and AUTHORITY_CEILING; tests/test_formal_math_premise_retrieval.py checks 11 premises, 4 queries, 44 considered candidates, five negative cases, metadata-only result records, and compact runtime-shell cards.
• Result records: receipts/first_wave/formal_math_premise_retrieval/formal_math_premise_retrieval_result.json records status: pass, 11 premises, 4 queries, 44 considered candidates, five observed negative cases, missing_negative_cases: [], and a secret-exclusion scan with blocking_hit_count: 0; the exported runtime result record at receipts/runtime_shell/demo_project/organs/formal_math_premise_retrieval/exported_premise_retrieval_bundle_validation_result.json records status: pass, the same premise/query/candidate counts, no negative cases, and secret_exclusion_scan.scanned_path_count: 11.
• Standard ceiling: standards/std_microcosm_formal_math_premise_retrieval.json::authority_ceiling has status: pass while keeping formal_proof_authority, lean_lake_authority, provider_authority, and release_authority false.

Runtime Surfaces

• Component runner: python -m microcosm_core.organs.formal_math_premise_retrieval run --input fixtures/first_wave/formal_math_premise_retrieval/input --out receipts/first_wave/formal_math_premise_retrieval
• Exported bundle runner: python -m microcosm_core.organs.formal_math_premise_retrieval run-retrieval-bundle --input examples/formal_math_premise_retrieval/exported_premise_retrieval_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_premise_retrieval
• CLI route: microcosm formal-math-premise-retrieval run-retrieval-bundle
• Standard: standards/std_microcosm_formal_math_premise_retrieval.json
• Fixture manifest: core/fixture_manifests/formal_math_premise_retrieval.fixture_manifest.json

Public Claim

Microcosm can show a real formal-math retrieval mechanism in miniature:

• a source-available Lean/Std premise index;
• public field-haystack term-scored queries;
• split-aware eligibility;
• context recipe ceilings;
• strategy gates;
• redacted validation result records.

How retrieval scoring works

Each premise row contributes five inspectable fields to the haystack: its premise id, namespace, declaration name, statement excerpt, and a list of retrieval terms. A query carries its own terms, a data split, an optional strategy id, a context recipe, and the public premise ids it is expected to return.

Scoring is term overlap, computed per query. Both the query and each premise are tokenised into lowercase word counts. A premise is only considered if the query's split appears in that premise's allowed_for_split list, which is how test-split leakage is kept out at the structural level rather than by trust. For each eligible premise the score is the summed minimum count of every shared token across the five fields, so a term that appears in both the query and the premise contributes as many points as the smaller of the two counts. A premise that also carries the query's strategy id as a tag gets a single extra point. The ranked list is sorted by score descending, ties broken by premise id, and the top of that list up to the query's top_k is taken as the retrieval.

The retrieval is then graded against itself. Each query declares the public premise ids it should surface, and the component computes recall as the fraction of those expected ids that actually landed in the shortlist. A query that declares expectations but misses any of them blocks the run. In the first-wave fixture this is eleven premises and four queries, scoring forty-four considered candidates in total, and every query is expected to reach full recall.

The failure mode this guards against is a premise-selection result that looks good because it cheated. The five negative-case inputs each encode one such shortcut: a premise index that ships a proof body, a query that lists the oracle premise ids it is "meant" to find, a query that tunes on test-split truth, a context recipe that blows past the byte budget, and a query naming a strategy id outside the allowed set. The run is required to observe all five rejections; if any expected rejection is missing, the whole fixture is blocked rather than passed. Recall over copied real metadata is the positive signal; the refusals are what keep that signal honest.

Prior Art Grounding

This component is grounded in premise-selection and retrieval-augmented theorem proving work. LeanDojo is the closest modern anchor because it couples Lean interaction with retrieval-augmented premise selection. Earlier theorem-proving environments such as HOList and GamePad also motivate extracting proof-state or premise metadata for learning-assisted theorem proving.

Microcosm borrows the retrieval accounting pattern: premise ids, namespaces, statement excerpts, retrieval terms, split eligibility, context budgets, and strategy gates must be inspectable before premise-retrieval claims are admitted. It does not run Lean/Lake or expose proof bodies.

Negative Cases

• premise_index_proof_body_forbidden
• query_oracle_ids_forbidden
• test_split_tuning_attempt
• context_recipe_budget_overflow
• unknown_strategy_id

Reader Evidence Routing

• Start with the JSON Bundle Binding to identify the source record, generated instance, proof boundary, and scope limit.
• Use Structured Lattice Bindings for navigation; the generated JSON row is the authority for relationship counts and dependency state.
• Use Runtime Surfaces and Result record Expectations when checking metadata coherence, redaction, leakage checks, and source-available bundle behavior.
• Use Negative Cases, Scope limit, and Scope limit together before admitting any formal-math public claim.

Validation Result record Path

./repo-pytest tests/test_formal_math_premise_retrieval.py -q --basetemp=/tmp/microcosm_formal_math_premise_retrieval_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus

formal_math_verifier_trace_repair_loop is the source-available replay of a source proof-lab pattern over copied Ring2 run system: verifier feedback becomes a teaching signal only after a trace grade, a repair action, a failure-mode ledger append, a curriculum delta, and a cold rerun result record.

It is deliberately not a Lean/Lake proof component. It sits between the existing readiness, premise retrieval, tactic routing, proof diagnostic, and Lean witness surfaces so a cold reader can inspect real failure taxonomy, graph-update candidates, and oracle-repair contrast rows without seeing proof bodies, oracle premise ids, model-output data bodies, or private run logs.

Purpose

A failed proof attempt is cheap to throw away and expensive to learn from. The question this component answers is narrow: can a verifier's failure be turned into a reusable repair signal, on the public side, without that signal quietly inheriting the authority of a real theorem prover? It exists because the interesting work in a proof-repair loop is the bookkeeping, not the proving, and that bookkeeping is where overclaim usually creeps in.

The design choice worth noticing is that the loop refuses to collapse its stages into a single verdict. A verifier failure only counts as a teaching signal once it carries a trace grade backed by trace events, a repair action named against the verifier failure class it responds to, a failure-mode ledger append, a curriculum delta, and a cold-rerun result record. Each of those is a separate field, and promotion is blocked until the cold-rerun result record is present. The same separation keeps the dangerous material out: proof bodies, oracle-needed premise ids, and model-output data bodies are forbidden keys, so a row may name a failure class without ever exposing the proof or the oracle answer that produced it.

The failure mode it guards against is stale copied rows pretending to be live proof-lab evidence. The repair rows here are imported from a real Ring2 benchmark run, so the temptation is to treat the copy as if the run were happening now. The realness gate is the answer: it only reaches its top rung when every verifier attempt and curriculum row replays cleanly against the imported source bodies, and the focused tests deliberately perturb an oracle row, a manifest digest, an attempt label, and a curriculum count so that any drift downgrades the verdict rather than passing quietly. A single deterministic toy-theorem rerun is the one thing actually executed here, and it is plain arithmetic over public inputs, not a Lean proof.

Shape

flowchart TD Input["Fixture input or exported bundle copied Ring2 rows + source-module manifest"] Protocol["Projection protocol copied-material provenance"] Manifest["Source-module manifest digest, line and byte match, body_in_receipt false"] Secret["Secret-exclusion scan proof bodies, oracle ids, model-output data forbidden"] Attempts["Verifier-attempt replay grade needs trace events, repair needs failure class"] Curriculum["Repair-curriculum replay failure-mode ledger, curriculum deltas"] Promotion["Promotion policy requires cold-rerun result record"] Toy["Deterministic toy rerun fail then repair over public inputs"] Realness["Realness gate clean source replay -> top rung; any drift downgrades"] Result records["metadata-only result records result, board, validation, sign-off"] Ceiling["Scope limit repair-loop accounting, bounded evidence"] Input --> Protocol Protocol --> Manifest Manifest --> Secret Secret --> Attempts Attempts --> Curriculum Curriculum --> Promotion Promotion --> Toy Attempts --> Realness Curriculum --> Realness Toy --> Realness Realness --> Result records Result records --> Ceiling

Technical Mechanism

The named mechanism mechanism.formal_math_verifier_trace_repair_loop.validates_public_verifier_trace_repair_bundle is a staged public verifier-repair validator, not a proof executor. _build_result composes five checks over the fixture or exported bundle: projection-protocol density, copied source-module manifest integrity, verifier attempt replay, repair-curriculum replay, promotion policy, and one deterministic toy-theorem repair rerun. The result is pass only when the projection protocol has copied-material provenance, the secret scan has no blocking hits, source modules pass when required, verifier attempts and curriculum rows replay against their imported Ring2 source bodies, promotion requires a cold rerun reference, and the toy rerun succeeds.

The exported-bundle path is intentionally stricter than the fixture path. validate_source_module_manifest requires a source import class, body_in_receipt: false, one row for each declared Ring2 source ref, matching target digests, line counts, and byte counts, and a metadata-only source_open_body_imports summary. _validate_attempt_source_replay then dereferences the premise-run row, oracle-repair contrast row, and graph-update candidate for each verifier attempt. Mismatches become typed findings such as VERIFIER_TRACE_SOURCE_REPLAY_MISMATCH, VERIFIER_TRACE_ORACLE_REPLAY_MISMATCH, VERIFIER_TRACE_COLD_RERUN_SOURCE_MISMATCH, or VERIFIER_TRACE_CANDIDATE_REPLAY_MISMATCH; curriculum-source mismatches are checked separately by validate_repair_curriculum.

The realness gate is also mechanical. _runtime_realness_evidence reaches the R4 state only for an exported bundle with verified source modules, at least 30 source replay checks, zero source replay mismatches, at least three attempts, at least nine trace events, at least three failure modes, and a passing toy rerun. The focused tests deliberately perturb the oracle source row, a manifest digest, a verifier-attempt source label, and a curriculum source count; each mutation blocks the verdict or downgrades the realness evidence instead of letting stale copied rows masquerade as proof-lab evidence.

The proof consumer is tests/test_formal_math_verifier_trace_repair_loop.py: it asserts five attempts, 15 trace events, five repair actions, three cold-rerun promotions, three toy-theorem failures repaired into four passing rerun inputs, seven exported source modules, 37 source replay checks, compact-card omission and fresh-result record reuse, public-relative result record paths, no private/body fields in result records, and exact source module copies. Those checks consume the same fixture, bundle, source-module manifest, and mechanism row cited by this page, so the evidence is executable replay accounting rather than a prose-only description.

The governing lattice is deliberately narrow: the bundle binds the module to concept.formal_math_and_proof_witness_bundle, principles P-1, P-2, P-3, P-6, and P-8, axioms AX-1, AX-2, AX-5, and AX-7, and dependency modules for the Lean standard premise index, tactic portfolio availability, target-shape tactic routing, and formal-math premise retrieval. The standard allows only copied Ring2 verifier-trace repair result record schemas and metadata-only public fields. It does not widen a passing replay into Lean/Lake authority, formal-result correctness, proof-body evidence, oracle premise authority, provider authority, human-approval proof authority, publishing-scope decision, launch-scope decision, or whole-system correctness.

Evidence/accounting:

• Bundle authority: core/paper_module_capsules.json::paper_modules[23:paper_module.formal_math_verifier_trace_repair_loop] sets source_authority: json_capsule, binds the component, binds mechanism.formal_math_verifier_trace_repair_loop.validates_public_verifier_trace_repair_bundle, and resolves src/microcosm_core/organs/formal_math_verifier_trace_repair_loop.py.
• Generated instance: paper_modules/formal_math_verifier_trace_repair_loop.json reports paper_module_payload.source_authority: json_capsule, Mermaid available_from_capsule_edges, Atlas linked_from_capsule_edges, 17 relationship edges, and resolved paper_module.depends_on.paper_module edges to the Lean standard premise index, tactic portfolio, target-shape routing, and formal-math premise retrieval modules named by the active standard.
• Runtime, fixture, and bundle: src/microcosm_core/organs/formal_math_verifier_trace_repair_loop.py exposes run, run_loop_bundle, validate_source_module_manifest, _write_receipts, EXPECTED_NEGATIVE_CASES, AUTHORITY_CEILING, and SOURCE_MODULE_MANIFEST_REF. The fixture input and exported bundle replay copied Ring2 verifier-trace repair metadata, source-module digests, failure classes, repair actions, promotion gates, and one deterministic public toy-theorem rerun.
• Result record and test floor: receipts/first_wave/formal_math_verifier_trace_repair_loop/formal_math_verifier_trace_repair_loop_result.json, verifier_trace_repair_board.json, formal_math_verifier_trace_repair_loop_validation_receipt.json, and result records/sign-off/first_wave/formal_math_verifier_trace_repair_loop_fixture_acceptance.json are metadata-only evidence. tests/test_formal_math_verifier_trace_repair_loop.py checks source-module manifest validation, negative cases, toy rerun evidence, and scope limits.
• Claim boundary: standards/std_microcosm_formal_math_verifier_trace_repair_loop.json and the generated structured source record limit this module to copied Ring2 verifier-trace repair metadata, source-module digests, public fixture result records, and deterministic toy rerun evidence. They do not authorize Lean/Lake authority, formal-result correctness, proof bodies, oracle premise ids, external model access, human approval as proof authority, launch-scope decision, publishing-scope decision, or whole-system correctness.

Reader Evidence Routing

Those rows prove reader wiring, not formal-result correctness.

Route runtime and replay questions through ## Runtime, ## Receipts, and the fixture/bundle paths in the validation command. The fixture runner, exported bundle runner, CLI route, standard, and fixture manifest show how verifier-trace repair accounting is replayed over copied public rows without importing proof bodies, oracle-needed premise ids, model-output data bodies, or private logs.

Route claim-safety questions through ## What It Proves, ## What It Refuses, ## Result record Expectations, and ## Scope limit. If the question is whether the repair loop is still body-safe and result record-backed, run the focused pytest and paper-module corpus check before citing this page.

Prior Art Grounding

This component is grounded in interactive theorem-proving feedback loops and learning environments where failed proof attempts become structured training or repair signals. GamePad and HOList both expose theorem-proving interaction data for machine-learning experiments, while LeanDojo reinforces the need to keep proof assistant feedback, retrieval, and proof-state interaction reproducible.

Microcosm borrows the repair-loop accounting pattern: verifier events, grades, failure classes, repair actions, curriculum deltas, and cold rerun result records are separate fields. It does not treat human or provider advice as formal-result correctness.

Runtime

• Component runner: python -m microcosm_core.organs.formal_math_verifier_trace_repair_loop run --input fixtures/first_wave/formal_math_verifier_trace_repair_loop/input --out receipts/first_wave/formal_math_verifier_trace_repair_loop
• Exported bundle runner: python -m microcosm_core.organs.formal_math_verifier_trace_repair_loop run-loop-bundle --input examples/formal_math_verifier_trace_repair_loop/exported_verifier_trace_repair_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_verifier_trace_repair_loop
• CLI: microcosm formal-math-verifier-trace-repair-loop run-loop-bundle --input examples/formal_math_verifier_trace_repair_loop/exported_verifier_trace_repair_bundle --out receipts/runtime_shell/demo_project/organs/formal_math_verifier_trace_repair_loop
• Standard: standards/std_microcosm_formal_math_verifier_trace_repair_loop.json
• Fixture manifest: core/fixture_manifests/formal_math_verifier_trace_repair_loop.fixture_manifest.json

What It Proves

• A public verifier replay can require trace events before trace grades.
• Copied Ring2 failure rows can feed a repair curriculum without becoming proof authority.
• A repair action must name the verifier failure class it responds to.
• A failure-mode ledger update can be represented without proof bodies.
• Promotion requires a cold rerun result record reference.
• Human or provider advice stays advisory until checker evidence exists.

What It Refuses

• Proof bodies in public verifier traces.
• Oracle-needed premise ids in public inputs.
• model-output data bodies in fixtures or result records.
• Human approval as checker authority or theorem-quality evidence.
• launch, public sharing, secret export, or general theorem-proving claims.

Result records

• receipts/first_wave/formal_math_verifier_trace_repair_loop/formal_math_verifier_trace_repair_loop_result.json
• receipts/first_wave/formal_math_verifier_trace_repair_loop/verifier_trace_repair_board.json
• receipts/first_wave/formal_math_verifier_trace_repair_loop/formal_math_verifier_trace_repair_loop_validation_receipt.json
• result records/sign-off/first_wave/formal_math_verifier_trace_repair_loop_fixture_acceptance.json

Validation Result record Path

./repo-pytest tests/test_formal_math_verifier_trace_repair_loop.py -q --basetemp=/tmp/microcosm_formal_math_verifier_trace_repair_loop_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.relationships.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/formal_math_verifier_trace_repair_loop.json

Expected generated-row proof: edge_count: 17, mermaid_status: available_from_capsule_edges, atlas_status: linked_from_capsule_edges, source_authority: json_capsule, and unresolved_selective_relation_count: 0.

formal_evidence_cell_anchor_resolver makes Microcosm's formal-math evidence claims inspectable without turning result record summaries into proof authority. It resolves paper-module claims to evidence-cell ids, checks source-anchor refs, records machine-anchor classes, and enforces a claim-strength boundary before any proof-language claim can pass. Its formal-math trace cell anchors the real Ring2 verifier-trace repair result records.

It is not a theorem prover. It does not execute Lean or Lake, expose proof bodies, expose non-public source refs, use external model services, or claim formal-result correctness. It emits real runtime result records over the imported evidence-cell system, carries digest-bearing Ring2 failure-taxonomy and graph-update source refs, and uses secret-exclusion scanning only for account secret-equivalent or non-result record body payloads.

Purpose

Proof-adjacent prose is the easiest place for a claim to drift. A paper module can write "this proves the theorem" or "this is certified" and a cold reader has no cheap way to tell whether the words are backed by a checked artifact or by nothing at all. This component answers one question: when a claim uses proof language, can the words be resolved to a specific piece of public evidence, and does that evidence stay below theorem-correctness authority?

The mechanism is an evidence cell. A cell is a stable id that stands in for a bundle of result record-backed evidence: its source-anchor refs, a machine_anchor_class that names what kind of machine artifact backs it, and the list of claim strengths the cell is allowed to support. The policy proof_language_requires_machine_anchor is the rule that makes the resolver useful. A claim that uses proof language must name a cell, the cell must resolve in the registry, and its source anchors must point at files that actually exist on the public path. A claim that uses proof language but names no cell, or names a cell that is not in the registry, lowers the run to a blocked status rather than passing as green prose.

What is worth noticing is what the cell id buys. It is a compressed handle: one short reference that a reader can follow back to the real result records behind a claim, instead of inlining proof bodies or trusting narrative. Two boundaries sit on top of that handle. Claim strength is capped by the cell, so a claim cannot assert more than its anchored evidence allows. And human approval is refused as a substitute for a machine anchor, which keeps a sign-off from being treated as proof.

Shape

flowchart TD Bundle["source record core/paper_module_capsules.json::paper_modules[24]"] --> structured source record["structured source record paper_modules/formal_evidence_cell_anchor_resolver.json source basis: source record"] structured source record --> Mermaid["diagram view available_from_capsule_edges"] structured source record --> Atlas["map view blocked_until_organ_atlas_owner_lane_binds_edges"] structured source record --> Reader["this page this page"] Reader --> Runtime["runtime locus src/microcosm_core/components/formal_evidence_cell_anchor_resolver.py"] Runtime --> Fixture["first-wave fixture input fixtures/first_wave/formal_evidence_cell_anchor_resolver/input"] Runtime --> Bundle["exported evidence-cell anchor bundle examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle"] Bundle --> Manifest["source-open body manifest source_module_manifest.json"] Fixture --> Result records["validation result records result records/first_wave/... + result records/sign-off/..."] Bundle --> BundleReceipt["runtime-shell result record result records/runtime_shell/demo_project/components/formal_evidence_cell_anchor_resolver/..."] Result records --> Ceiling["proof boundary + scope limit anchor metadata only, not formal-result correctness"] BundleReceipt --> Ceiling

Read the diagram left to right: the bundle and generated structured source record name the relationships; the runtime validates fixture and bundle inputs; the result records show what passed; the scope limit prevents any of those surfaces from becoming proof, launch, provider, private-system, or theorem-correctness authority.

Reader Evidence Routing

A cold reader should inspect this module through these system surfaces, in order:

1. Authority seed: core/paper_module_capsules.json::paper_modules[24:paper_module.formal_evidence_cell_anchor_resolver]. This is the source record that binds the Markdown projection, generated JSON, runtime locus, fixture, exported bundle, mechanism rows, and scope boundaries.
2. Generated structured source record: paper_modules/formal_evidence_cell_anchor_resolver.json. Check relationships.source_authority, the 15 relationship edges, the generated_projections statuses, unpopulated_selective_relations, and the bundle-carried scope limit before trusting any prose summary.
3. Runtime locus: src/microcosm_core/organs/formal_evidence_cell_anchor_resolver.py. The relevant runtime symbols are run, run_anchor_bundle, validate_source_module_manifest, _build_result, _source_module_summary_card, EXPECTED_NEGATIVE_CASES, AUTHORITY_CEILING, SOURCE_MODULE_MANIFEST_REF, BUNDLE_RESULT_NAME, and CARD_SCHEMA_VERSION.
4. Fixture and exported bundle: fixtures/first_wave/formal_evidence_cell_anchor_resolver/input, examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle, and examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle/source_module_manifest.json. The first-wave fixture exercises negative cases and Ring2 result record anchors; the exported bundle validates six source-open body modules by digest while keeping source bodies out of result records.
5. Result records: receipts/first_wave/formal_evidence_cell_anchor_resolver/formal_evidence_cell_anchor_resolver_result.json, receipts/first_wave/formal_evidence_cell_anchor_resolver/evidence_cell_anchor_board.json, receipts/first_wave/formal_evidence_cell_anchor_resolver/formal_evidence_cell_anchor_resolver_validation_receipt.json, result records/sign-off/first_wave/formal_evidence_cell_anchor_resolver_fixture_acceptance.json, and receipts/runtime_shell/demo_project/organs/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle_validation_result.json. These result records report pass/fail state, metadata-only public refs, negative-case observations, and explicit release_authorized=false, provider_calls_authorized=false, lean_lake_execution_authorized=false, formal_proof_authority=false, and theorem_correctness_authority=false ceilings.
6. Focused checks: tests/test_formal_evidence_cell_anchor_resolver.py, scripts/build_doctrine_projection.py --check-paper-module-corpus, and the JSON-row proof query in the validation section below. Those checks validate the reader route and generated-row parity; they do not authorize public sharing or formal proof claims.

Prior Art Grounding

This component is grounded in provenance and proof-certificate work where claims must point at checkable evidence rather than untyped narrative. The W3C PROV model is a general anchor for linking entities, activities, and agents in an evidence graph, while Proof-Carrying Code and small-kernel proof assistants motivate separating a certificate or anchor from the trusted checker that bounds its meaning.

Microcosm borrows the anchor-resolution pattern: proof-language claims must name evidence-cell ids, source anchors, machine-anchor classes, and claim strength limits. It does not turn metadata cells into theorem-correctness authority.

Runtime

• Component runner: python -m microcosm_core.organs.formal_evidence_cell_anchor_resolver run --input fixtures/first_wave/formal_evidence_cell_anchor_resolver/input --out receipts/first_wave/formal_evidence_cell_anchor_resolver
• Exported bundle runner: python -m microcosm_core.organs.formal_evidence_cell_anchor_resolver run-anchor-bundle --input examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle --out receipts/runtime_shell/demo_project/organs/formal_evidence_cell_anchor_resolver
• CLI: microcosm formal-evidence-cell-anchor-resolver run-anchor-bundle --input examples/formal_evidence_cell_anchor_resolver/exported_evidence_cell_anchor_bundle --out receipts/runtime_shell/demo_project/organs/formal_evidence_cell_anchor_resolver
• Standard: standards/std_microcosm_formal_evidence_cell_anchor_resolver.json
• Fixture manifest: core/fixture_manifests/formal_evidence_cell_anchor_resolver.fixture_manifest.json

What It Establishes As Evidence Routing

• Proof-language claims must resolve to a public evidence cell before this reader treats them as routed evidence.
• Evidence cells must carry source-anchor refs.
• Machine-anchor metadata is visible as metadata, not formal-result correctness.
• Claim strength is bounded by the resolved cell.
• Secret, account secret-equivalent, or non-result record body payloads must have explicit exclusion result records.
• The verifier-trace cell is anchored to the first-wave formal_math_verifier_trace_repair_loop result, board, validation result record, and Ring2 failure-taxonomy source digest.

What It Refuses

• Unknown evidence-cell ids used as proof authority.
• Proof-language claims without evidence-cell ids.
• Proof bodies in public claim rows.
• non-public source refs in public claim or cell rows.
• Human approval as proof authority.
• Theorem-correctness claims from metadata cells.
• launch, public sharing, secret export, or provider authority.

Result records

• receipts/first_wave/formal_evidence_cell_anchor_resolver/formal_evidence_cell_anchor_resolver_result.json
• receipts/first_wave/formal_evidence_cell_anchor_resolver/evidence_cell_anchor_board.json
• receipts/first_wave/formal_evidence_cell_anchor_resolver/formal_evidence_cell_anchor_resolver_validation_receipt.json
• result records/sign-off/first_wave/formal_evidence_cell_anchor_resolver_fixture_acceptance.json

Validation Result record Path

./repo-pytest tests/test_formal_evidence_cell_anchor_resolver.py -q --basetemp=/tmp/microcosm_formal_evidence_cell_anchor_resolver_pytest
./repo-python scripts/build_doctrine_projection.py --check-paper-module-corpus
jq '{edge_count:(.relationships.edges|length), mermaid_status:.paper_module_payload.generated_projections.mermaid.status, atlas_status:.paper_module_payload.generated_projections.atlas_card.status, source_authority:.relationships.source_authority, unresolved_selective_relation_count:(.relationships.unpopulated_selective_relations|length)}' paper_modules/formal_evidence_cell_anchor_resolver.json

Expected generated-row proof: edge_count: 15, mermaid_status: available_from_capsule_edges, atlas_status: blocked_until_organ_atlas_owner_lane_binds_edges, source_authority: json_capsule, and unresolved_selective_relation_count: 0.

This module is the Microcosm projection of the formal-prover rule that a Lean-accepted proof can still violate the evaluation contract when it uses a real library symbol that was not in the allowed premise set. It is a provenance-bearing symbol-boundary component, not a proof checker.

The fixture carries copied Lean/Std premise rows from the real Ring2 premise-index system and real Ring2 problem ids / candidate artifact digests for the symbol-boundary examples. It records extracted qualified symbol refs and classifies a known symbol outside allowed_premise_ids as UNDECLARED_LIBRARY_PRIOR. If cited_unallowed_premise_ids is present, that explicit budget violation takes precedence and routes as PREMISE_BUDGET_VIOLATION.

The source chain is digest-bearing: the real Ring2 premise index sha256:c78b176388a5e81bd8a785950e7db0c9a65fd38e556515134146163b48604df1, Ring2 run summary sha256:93304410f32d40f5cad1c161c1d01a5d6f353ee10b7cf3fecbaaf7b068b43008, copied Lean/Std premise fixture sha256:0be36ba5b75b40d2ede2d90cefa5181829420df7abbae216d18282b92a30f869, and the adjacent corpus-readiness / tactic-availability result records anchor the Mathlib-absent toolchain boundary.

The exported bundle carries a source-open body floor at examples/undeclared_library_prior_symbol_classifier/exported_symbol_classifier_bundle/source_module_manifest.json. It imports the reducer and set-calibration builder source bodies exactly, plus run bodies for the Ring2 premise index, Ring2 run summary, recipe policy metrics, and result record reduction matrix. The two run-state bodies are path-normalized to <repo-root> and <lean-toolchain-root> while preserving source and target digests, line counts, byte counts, and required anchors.

Purpose

A theorem prover can return a proof that Lean accepts, yet that proof can still break the rules of the evaluation it was run under. The usual reason is simple: the proof reached for a library lemma that the recipe never put on the table. The symbol is real and the proof is sound, but the run quietly used a fact it was not allowed to assume. This component answers one question. Given a set of premises a candidate was allowed to use and the symbols it actually reached for, did it cite a known library symbol that was outside that allowed set?

The unusual choice is what the classifier refuses to do. It does not run Lean, it does not read the proof body, and it does not treat the standard library as an implicit allowlist where anything that exists is fair game. It works only from a copied premise index and a list of symbol observations that were extracted beforehand, and it compares the two. That keeps the check cheap and keeps proof material out of the public result record, but it also means the allowed set is closed by construction: a symbol is admissible only because a premise row names it, never because it happens to live in Lean's standard library.

The check also separates two failure modes that are easy to confuse. An explicit budget breach, where the candidate names a premise id the recipe did not allow, is not the same as a residual breach, where the candidate used an allowed-looking symbol that turns out to be undeclared. The first is settled directly from the cited ids and takes precedence; the second is what the symbol comparison is for. Treating both as one class would either over-escalate honest retries or let genuine out-of-recipe library use slip through as a budget note. Keeping them apart is the point.

Shape

flowchart TD bundle["JSON source record paper_module.undeclared_library_prior_classifier"] structured source record["structured source record 19 edges, no selective residuals"] runtime["Runtime component undeclared_library_prior_symbol_classifier.py"] premise["Copied Lean/Std premise index 11 sanctioned symbols"] observations["Pre-extracted symbol observations Nat/List/Bool/Iff/Eq refs"] budget["cited_unallowed_premise_ids present"] residual["Known qualified symbol outside allowed_premise_ids"] clean["Allowed symbol or no known undeclared symbol"] retry["PREMISE_BUDGET_VIOLATION route: retry"] escalate["UNDECLARED_LIBRARY_PRIOR route: bridge_escalate"] advisory["NONE route: accept_as_advisory"] result records["Result record stream fixture, board, validation, sign-off"] ceiling["Scope limit no Lean/Lake, proof, provider, launch, private-system claim"] bundle --> structured source record structured source record --> runtime runtime --> premise runtime --> observations observations --> budget observations --> residual observations --> clean budget --> retry residual --> escalate clean --> advisory retry --> result records escalate --> result records advisory --> result records result records --> ceiling

Technical Mechanism

The component separates three questions that are easy to conflate in proof evaluation: whether a candidate explicitly cites a premise outside the recipe, whether it uses a known Lean/Std symbol that was not in the allowed premise set, and whether the theorem is actually correct. Only the first two are in scope. validate_premise_index builds the closed allowlist from copied Lean/Std premise rows, validate_symbol_observations reads pre-extracted qualified symbol observations, and _classify_row applies the precedence rule: cited_unallowed_premise_ids yields PREMISE_BUDGET_VIOLATION with retry; otherwise a known qualified symbol outside allowed_premise_ids yields UNDECLARED_LIBRARY_PRIOR with bridge_escalate; clean or unknown observations remain advisory. The classifier records observed symbols and computed/asserted classes, but it never evaluates proof bodies or runs Lean.

The exported-bundle mechanism is a second boundary rather than a richer proof. validate_source_module_manifest requires source_module_manifest.json, rejects manifest or row-level body_in_receipt: true, verifies six declared body imports against source/target digests, line counts, byte counts, required anchors, material classes, and relation type, and keeps path-normalized Ring2 run-state bodies separate from exact copied reducer bodies. secret_exclusion_scan then checks the declared public fixture and bundle inputs for proof-body, provider-payload, private-ref, and host-path sentinel classes. _write_receipts writes result, board, validation, and sign-off result records; result_card deliberately emits a small pass/fail card that omits source modules, source digests, proof bodies, non-public source refs, secret-scan detail, and scope limit bodies. This is why the module can be source-open about the symbol-boundary system without becoming a proof-body export.

The governing lattice follows the same separation. The bundle binds the component to mechanism.undeclared_library_prior_symbol_classifier.validates_public_symbol_boundary, concept.formal_math_and_proof_witness_bundle, principles P-1, P-2, P-3, P-6, P-8, and P-9, and axioms AX-1, AX-2, AX-5, AX-7, AX-8, and AX-10. The technical claim is therefore limited to public symbol-budget classification over copied, digest-bearing premise evidence. It does not establish theorem truth, Mathlib availability, Lean/Lake execution, launch-scope decision, provider correctness, or complete library allowlisting.

Reader Evidence Routing

Start with the source record, not this prose: core/paper_module_capsules.json::paper_modules[56:paper_module.undeclared_library_prior_classifier] is the source authority that names the component subject undeclared_library_prior_symbol_classifier, the mechanism mechanism.undeclared_library_prior_symbol_classifier.validates_public_symbol_boundary, the code locus src/microcosm_core/organs/undeclared_library_prior_symbol_classifier.py, the concept concept.formal_math_and_proof_witness_bundle, the governing principles P-1, P-2, P-3, P-6, P-8, and P-9, the axioms AX-1, AX-2, AX-5, AX-7, AX-8, and AX-10, and the sibling modules paper_module.corpus_readiness_mathlib_absence_gate, paper_module.tactic_portfolio_availability, and paper_module.lean_std_premise_index.

Then read the generated structured source record paper_modules/undeclared_library_prior_classifier.json. It is the parity projection from the bundle, carrying source_authority: json_capsule, Mermaid available_from_capsule_edges, Atlas linked_from_capsule_edges, 19 generated relationship edges, and no unpopulated selective relations. The structured source record is evidence that the reader page is wired into the doctrine lattice; it is not theorem-correctness, launch, or runtime-correctness authority.

For runtime behavior, inspect src/microcosm_core/organs/undeclared_library_prior_symbol_classifier.py. The named locus validates projection protocol, premise index, classifier policy, source-module manifest, symbol observations, secret-exclusion scan, result construction, result record writing, and result-card compaction. The load-bearing classifier rule is _classify_row: explicit cited_unallowed_premise_ids short-circuit as PREMISE_BUDGET_VIOLATION with retry; otherwise a known qualified Lean/Std symbol outside allowed_premise_ids classifies as UNDECLARED_LIBRARY_PRIOR with bridge_escalate. Negative cases reject proof bodies, non-public source refs, theorem-correctness overclaims, allowed-symbol false positives, unqualified-token overclaims, and missing escalation.

For public fixture evidence, use fixtures/first_wave/undeclared_library_prior_symbol_classifier/input/. The fixture carries the premise index, classifier policy, projection protocol, symbol observations, and the seven negative-case files named by EXPECTED_NEGATIVE_CASES. For exported source-open body-floor evidence, use examples/undeclared_library_prior_symbol_classifier/exported_symbol_classifier_bundle/source_module_manifest.json. That manifest verifies six source body imports: reducer source, set-calibration builder source, path-normalized Ring2 premise-index state, path-normalized Ring2 run summary, recipe policy metrics, and result record reduction matrix. The manifest keeps body_in_receipt false and checks source/target digests plus required anchors; it does not export proof bodies, model-output data bodies, account or browser state, source notes, or private source-root bodies.

For result records, read receipts/first_wave/undeclared_library_prior_symbol_classifier/undeclared_library_prior_symbol_classifier_result.json, receipts/first_wave/undeclared_library_prior_symbol_classifier/undeclared_library_prior_symbol_classifier_board.json, receipts/first_wave/undeclared_library_prior_symbol_classifier/undeclared_library_prior_symbol_classifier_validation_receipt.json, and result records/sign-off/first_wave/undeclared_library_prior_symbol_classifier_fixture_acceptance.json. The fixture result record reports 11 premises, 3 classifications, 1 undeclared-library prior, 1 premise-budget-precedence case, 1 bridge escalation, 1 retry, zero blocking secret-exclusion hits, and the scope boundary that this is not Lean/Lake, formal-result correctness, provider, private-ref, whole-library-allowlist, or launch-scope decision.

Focused regression coverage lives in tests/test_undeclared_library_prior_symbol_classifier.py. It runs both the fixture command and run-symbol-bundle, checks public-relative result records, verifies digest/manifest boundary failures, and confirms the compact card reuses a fresh result record without exporting source modules, body ids, secret-scan details, source digests, proof bodies, or non-public source refs. The paper-module coverage contract also names this module in tests/test_microcosm_paper_module_coverage_contract.py; that is route coverage evidence, not runtime proof evidence.

Named Proof Consumers

The fixture consumer is microcosm_core.organs.undeclared_library_prior_symbol_classifier run over fixtures/first_wave/undeclared_library_prior_symbol_classifier/input. It proves the public example still classifies 11 copied premise rows and 3 symbol observations into one undeclared-library-prior escalation, one premise-budget retry, and one advisory clean case, while the expected negative cases cover proof-body export, non-public refs, theorem-correctness overclaim, allowed-symbol false positives, unqualified-token overclaims, and missing escalation.

The exported-bundle consumer is microcosm_core.organs.undeclared_library_prior_symbol_classifier run-symbol-bundle over examples/undeclared_library_prior_symbol_classifier/exported_symbol_classifier_bundle. It proves the six source-open body imports remain digest/size/anchor checked and public-safe, including the exact copied reducer and calibration-builder bodies plus path-normalized Ring2 state, recipe metrics, and reduction-matrix bodies. It is the consumer that catches source-module digest drift and manifest-boundary violations; it does not certify formal-result correctness.

The focused regression consumer is tests/test_undeclared_library_prior_symbol_classifier.py. It ties the fixture and bundle commands to public-relative result records, source-module digest mismatch blocking, manifest and row-level body_in_receipt rejection, compact-card redaction, and fresh-card reuse. The corpus consumer is scripts/build_doctrine_projection.py --check-paper-module-corpus, which proves the Markdown remains part of the 98-module Microcosm paper-module corpus. That corpus check is routing and projection parity evidence only; it is not a runtime proof substitute.

Public Mechanics

• Qualified symbol refs are restricted to Nat, List, Bool, Iff, and Eq namespaces in this public fixture.
• The closed premise index is an allowlist boundary, not permission to use the whole standard library.
• UNDECLARED_LIBRARY_PRIOR routes to bridge_escalate because the proof may be informative while still out of recipe.
• PREMISE_BUDGET_VIOLATION routes to retry and short-circuits the residual symbol classifier.
• Result records expose ids, candidate artifact digests, symbols, counts, failure classes, source refs, source digests, and scope limits.
• secret_exclusion_scan records zero blocking hits for the declared sentinel classes in the public result record stream; it is not a complete secret audit, launch clearance, or proof that no private material exists anywhere.

Prior Art Grounding

This classifier is grounded in formal-methods work on premise control and library-aware proof search. Isabelle/Sledgehammer makes relevant-fact selection an explicit part of automated proof search, and Lean/Mathlib practice makes clear that accepted proofs can depend on a large library context. Microcosm uses that insight as a boundary check: an accepted proof artifact is not enough if it quietly used symbols outside the declared premise set. The component classifies the symbol-budget violation without judging theorem truth or exporting proof bodies.

Prior-art anchors:

• Isabelle Sledgehammer and relevant-fact selection: https://isabelle.in.tum.de/doc/sledgehammer.pdf
• Lean community Mathlib overview: https://leanprover-community.github.io/mathlib-overview.html
• Lean 4 tactic and proof environment context: https://lean-lang.org/theorem_proving_in_lean4/Tactics/

Regression Cases

The forbidden proof-body, private-ref, allowed-symbol false-positive, unqualified-token, and theorem-correctness cases are regression-only leakage guards. They are not product evidence and cannot stand in for the copied Lean/Std symbol-boundary system.

Validation Result record Path

Run from microcosm-substrate:

The expected bundle projection is Mermaid available_from_capsule_edges, Atlas linked_from_capsule_edges, and 19 generated relationship edges with no unpopulated selective relations. A green result record proves only the allowed-premise and symbol-budget classification boundary; it does not establish formal-result correctness, run Lean or Lake, expose proof bodies, authorize external model access, claim Mathlib availability, or broaden all Std and Mathlib declarations into allowed priors.

ring2_premise_retrieval_precision_recall_harness is the public Microcosm component for evaluating copied Ring-2 premise retrieval rankings against after-the-fact labels.

The component computes precision and recall per problem, then classifies the result as retrieval_hit, partial_retrieval_miss, retrieval_miss, or proof_failure_despite_hit. That distinction matters because a failed proof with all needed premises retrieved is a different failure than a missing premise retrieval path.

Purpose

When a proof search fails, it is easy to blame the prover and miss the simpler cause: the right supporting facts were never put in front of it. This component exists to keep those two cases apart. It answers one question: did the retrieval step actually surface the premises a problem needed, or did the failure happen somewhere downstream after the premises were already in hand?

It answers that by recomputing precision and recall from copied records rather than trusting a reported figure. For each problem it intersects the retrieved premise ids with the labelled needed-premise ids, then reads the proof outcome alongside that overlap. Full recall with a passing proof is a retrieval_hit; full recall with a non-passing proof is proof_failure_despite_hit, the case where retrieval did its job and the fault lies elsewhere. Partial overlap and zero overlap are graded as partial_retrieval_miss and retrieval_miss.

The unusual part is the direction the labels are allowed to flow. The needed premise ids are after-the-fact measurement labels, and the component treats them as strictly one-way: they may be used to score a finished run, but they may not be fed back into the retrieval ranking, used to tune on a test split, or carried into a provider-context recipe. Planting an oracle label inside a ranking, or tuning on test answers, is a typed refusal, not a higher score. The point is a metric that cannot quietly become the very advantage it is meant to measure, and that never inflates a retrieval result into a claim about formal-result correctness.

Shape

flowchart TD Bundle["source record core/paper_module_capsules.json[42]"] --> JSON["structured source record paper_modules/ring2_premise_precision_recall.json"] JSON --> Markdown["this page reader projection"] JSON --> Mermaid["diagram view available_from_capsule_edges"] JSON --> Atlas["map view organ_atlas.ring2_premise_retrieval_precision_recall_harness"] Fixture["fixture input fixtures/first_wave/.../input"] --> Runtime["runtime component ring2_premise_retrieval_precision_recall_harness.py"] Bundle["exported bundle examples/.../exported_ring2_precision_recall_bundle"] --> Runtime Runtime --> Metrics["precision/recall labels retrieval vs proof-failure attribution"] Runtime --> Result records["validation result records first_wave + runtime_shell"] Runtime --> Negatives["negative cases leakage, tuning, overclaim, missing decoy"] Result records --> Boundary["proof boundary metrics and copied artifacts only"]

Technical Mechanism

The runtime splits the proof consumer into three evidence classes before it reports any metric. _load_payloads reads the declared fixture or exported bundle inputs; _validate_run_material checks that copied Ring-2 run material carries source refs, target refs, validation refs, digests, and the expected copied_non_secret_macro_body_with_provenance status; and _validate_source_artifacts verifies the four copied source artifacts against either the source digest or the private-path rewrite digest. The result record therefore proves the presence and provenance of the copied public artifacts before the precision/recall scores can be interpreted.

The scoring core is _evaluate. It indexes after-the-fact labels by problem_id, applies the policy default_top_k or per-ranking top_k, truncates retrieved premise ids to that cutoff, intersects retrieved ids with labelled needed-premise ids, and computes precision_at_k = hits/top_k and recall_at_k = hits/needed. Aggregate precision and recall use total hit, candidate, and needed-premise counts, then compare the computed aggregate metrics with the policy's expected values. This is why the paper module can distinguish a retrieval miss from a proof failure after full premise recall without asserting anything about the downstream proof.

The failure taxonomy is mechanical rather than rhetorical. Full recall plus a passing proof is retrieval_hit; full recall plus a non-passing proof is proof_failure_despite_hit; partial overlap is partial_retrieval_miss; and zero overlap is retrieval_miss. The policy floor also requires expected failure modes and an adversarial decoy whose needed premise is absent or missed. Those gates make the metric harness test the shape of the evaluation set, not just the happy path.