Microcosm Axiom System

Read-only evidence accounting for each axiom

The axiom system is a read-only evaluator that measures how much on-disk evidence actually backs each Microcosm axiom, and reports where that evidence runs out. The axiom system is a read-only evaluator that measures how much on-disk evidence actually backs each Microcosm axiom, and reports where that evidence runs out. Its core is evaluate_axiom_support_cover in src/microcosm_core/validators/axiom_support_cover.py.

A doctrine file can assert that the system holds twelve axioms. The harder question is whether anything checkable stands behind each one. A doctrine file can assert that the system holds twelve axioms. The harder question is whether anything checkable stands behind each one. This component answers a single question: for each axiom, how strong is the support that already exists on disk, and where does it stop short of proof?

It emits one result record per run: a support case for every obligation, a per-axiom verdict, an anti-axiom rejection mapping, a strong-gate summary, and derived principle support. It emits one result record per run: a support case for every obligation, a per-axiom verdict, an anti-axiom rejection mapping, a strong-gate summary, and derived principle support. No node in that record ever reports strong_certified: true.

Purpose

The routing source core/axiom_organ_routing.json hand-stamps eleven of the twelve axioms with witness_strength: strong and names the anti-axiom each is meant to reject: AX-1 against asserted_label_is_truth, AX-5 against silent_default_pass, AX-8 against endpoint_label_assertion_without_propagation, AX-12 against meta_artifact_exemption. The routing source core/axiom_organ_routing.json hand-stamps eleven of the twelve axioms with witness_strength: strong and names the anti-axiom each is meant to reject: AX-1 against asserted_label_is_truth, AX-5 against silent_default_pass, AX-8 against endpoint_label_assertion_without_propagation, AX-12 against meta_artifact_exemption. A loose reader would take those stamps at face value. The evaluator does not. It recomputes support from the material each obligation actually cites, and caps every axiom below strong.

Loose fails in a specific way. The routing defines strong as computing the property and rejecting the named anti-axiom with a negative case. Loose fails in a specific way. The routing defines strong as computing the property and rejecting the named anti-axiom with a negative case. Confirming that a witness component's result record holds a complete negative-case suite is not the same as proving that suite rejects one obligation's slice. If the evaluator let the first stand in for the second, a green count would mask an unproven claim. So the gap is reported as pressure to do more witness work, never closed by relabelling. The honesty contract points back at the evaluator too: because it is itself a Microcosm artifact, AX-12 forbids it from reading its own generated output as evidence for itself.

How it works

evaluate_axiom_support_cover is the entrypoint. It reads the routing rows, the eight-component ceiling registry and its six sub-order registries through _ceiling_dimension_registry, the component registry, the evidence-class table, and PRINCIPLES.md. evaluate_axiom_support_cover is the entrypoint. It reads the routing rows, the eight-component ceiling registry and its six sub-order registries through _ceiling_dimension_registry, the component registry, the evidence-class table, and PRINCIPLES.md. It walks the twelve rows in order and evaluates each row's obligations, then folds the results into one record.

Each obligation carries a binding: the witness components, source surfaces, and negative-case codes meant to back it. Each obligation carries a binding: the witness components, source surfaces, and negative-case codes meant to back it. _binding_issues checks that every cited piece resolves. A witness component must exist in core/organ_registry.json, a surface must exist on disk or match a glob, and a negative-case code must be declared on the routing row. Any unresolved reference is returned as a concrete issue string such as organ_not_in_registry:<id> or surface_missing:<path>, which caps the obligation at blocked_binding_unresolved rather than letting it pass.

For bindings that resolve, _ceiling_vector computes a value for each of eight named components: evidence_class, checker_scope, provenance_class, freshness_state, domain_scope, negative_case_status, authority_scope, and projection_scope. For bindings that resolve, _ceiling_vector computes a value for each of eight named components: evidence_class, checker_scope, provenance_class, freshness_state, domain_scope, negative_case_status, authority_scope, and projection_scope. Each value is read off the bound material. evidence_class is the strongest rank among the witness components and never exceeds it. freshness_state is pinned to its honest floor, unknown_live_freshness_no_refresh_contract: a deterministic basis digest proves the inputs are reproducible, not that they are current. authority_scope and projection_scope each carry a non-laundering note so read-only output and generated projections cannot be read back as source evidence.

_anti_axiom_rejection tracks rejection apart from support. Its tier rises to organ_receipt_coverage_present only when _organ_receipt_negative_coverage finds a component result record under receipts/first_wave/ whose negative_case_coverage has an empty missing list and top-level status: pass. _anti_axiom_rejection tracks rejection apart from support. Its tier rises to organ_receipt_coverage_present only when _organ_receipt_negative_coverage finds a component result record under receipts/first_wave/ whose negative_case_coverage has an empty missing list and top-level status: pass. Even then mapping_verified stays false unless a source-owned mapping row on the routing declares an exact or subsuming rejection for that obligation. The record notes plainly that no v0 tier certifies a per-obligation rejection from component-level coverage.

_axiom_verdict folds each axiom's required obligations into one verdict and an explicit list of strong_blocked_reasons. _axiom_verdict folds each axiom's required obligations into one verdict and an explicit list of strong_blocked_reasons. It sets hand_stamped_strong_not_certifiable to true whenever the row stamped strong. _strong_gate_summary then takes the bilattice meet of two judgements: positive_support_status from the obligations' resolution, and rejection_mapping_status from the mappings. A detected conflict beats layer debt, which beats an unverified rejection. strongest_allowed_claim equals the raw verdict only when rejection is verified and nothing caps it, which for the current source is never.

_compile_support_case builds the citation envelope for one obligation. It cites only bundle and result-record refs that resolve on disk, stamps a deterministic basis_digest from _basis_digest, records the rederive command, and labels itself as citation, not certified strength. _compile_support_case builds the citation envelope for one obligation. It cites only bundle and result-record refs that resolve on disk, stamps a deterministic basis_digest from _basis_digest, records the rederive command, and labels itself as citation, not certified strength. Principle support is derived, not measured: _principle_obligation_groundings parses each principle's Obligation grounding: line in PRINCIPLES.md and inherits support from those obligations, so a principle is never stronger than the obligations it rests on. main wraps the entrypoint as a CLI, writing the record to --out or stdout.

flowchart TD Routing["Routing rows core/axiom_organ_routing.json AX-1 to AX-12, anti-axiom, hand-stamped witness_strength"] Bind["_binding_issues witness components, surfaces, negative-case codes resolve?"] Capped["blocked_binding_unresolved or layer_debt"] Ceiling["_ceiling_vector eight named components"] Reject["_anti_axiom_rejection mapping_verified false without a source-owned row"] Meet["_strong_gate_summary meet of support and rejection"] Claim["strongest_allowed_claim strong_certified: false"] Routing --> Bind Bind -- "unresolved" --> Capped --> Meet Bind -- "resolved" --> Ceiling --> Meet Bind --> Reject --> Meet Meet --> Claim

Negative cases

The evaluator refuses a fixed set of moves. It never echoes a hand-stamped strong: eleven rows stamp it and AX-8 stamps partial, and no axiom node reports strong_certified: true. The evaluator refuses a fixed set of moves. It never echoes a hand-stamped strong: eleven rows stamp it and AX-8 stamps partial, and no axiom node reports strong_certified: true. It never promotes organ_receipt_coverage_present into exact_obligation_rejection; component-level coverage is admissible material, not a per-obligation rejection. It fails an obligation closed when any binding reference does not resolve, rather than passing it silently. It flags any binding that cites a principle as a witness, since a principle that leans on an axiom cannot also serve as that axiom's evidence. The AX-8 mappings stay deliberately non-uniform in the source rows so that endpoint coverage never reads as general source-to-sink propagation rejection.

Prior Art Grounding

The pattern draws from two older ideas: formal assumptions should be inspectable, and machine-readable schemas should make support claims testable. The pattern draws from two older ideas: formal assumptions should be inspectable, and machine-readable schemas should make support claims testable. Lean gives the immediate analogue through its axiom-audit practice, where a theorem can be checked and then separately inspected for its assumptions with #print axioms. This component adapts that spirit to doctrine by making each axiom expand into witness surfaces, negative cases, routing rows, and support-frontier status instead of treating the axiom prose as self-certifying. The schema side is grounded in JSON Schema, which frames schemas as a way to define validation rules and document shared structure. The provenance side is adjacent to W3C PROV: support rows and witness refs are evidence links with bounded meaning, bounded evidence of whole-system completeness.

Validation Result record Path

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

PYTHONPATH=src ../repo-python \
  -m microcosm_core.validators.axiom_support_cover \
  --root . \
  --out /tmp/microcosm-axiom-support-cover-vrp.json

Focused test command, run from the repository root:

A pass means the evaluator wrote a record that reports support cases, support frontiers, anti-axiom rejection mappings, principle inheritance, and strong-gate pressure without mutating law, and that the tests confirm routing-schema parity, witness refs, negative-case evidence, the AX-8 mapping readback, and the rule that component coverage is not laundered into exact obligation rejection. A pass means the evaluator wrote a record that reports support cases, support frontiers, anti-axiom rejection mappings, principle inheritance, and strong-gate pressure without mutating law, and that the tests confirm routing-schema parity, witness refs, negative-case evidence, the AX-8 mapping readback, and the rule that component coverage is not laundered into exact obligation rejection.