Repository navigation
[Principia M1] Add canonical source-object packets, mappings, safe authoring, and validation #19
Description
Objective
Add a backward-compatible, policy-enforced source ontology to MathCorpus. The implementation must make historical source identity and source-to-modern mappings canonical without weakening the existing formal packet path.
Schema changes
- Add
source_objectto packetkind. - Add
source_onlyto packetstatus. - Enforce
source_only → trust.rung = 0andproof_authority = none. - Add optional
category_ref, validated against Expand the packet curriculum taxonomy across mathematics and add a generic first-principles-to-frontier authoring prompt #11's category registry. - Add a conditional
source_objectblock with:- literature source ID and hash;
- textual layer;
- source role;
- structured edition/book/section/item/page locator;
- segment-normalization version and source-segment SHA-256;
- source/target language;
- attribution roles;
- extraction method;
- editorial review state;
- rights review state;
- excerpt/full-text export permissions;
- fidelity notes.
- Add canonical
source_mappingsrelations for faithful restatement, modern specialization/generalization, formalization, analytical core, approximation justification, empirical premise, and historical context.
Safe authoring
Create tools/author_source_packet.py; do not overload the formal authoring defaults.
It must:
- default to source-only, rung 0, no proof authority;
- default training eligibility to
private_audit_only; - default proof/full-text export to false;
- require source record/hash, role, textual layer, structured locator, segment hash, attribution, and rights state;
- never invent authorship, license, public-domain status, review state, or training eligibility;
- refuse public eligibility until rights and review fields are explicit;
- use existing canonical JSON/hash utilities;
- produce deterministic output and support a check/no-op mode.
Policy and validation
- Resolve every mapping target.
- Enforce relation/target compatibility.
- Require
formalizationtargets to be recognized as formal by policy. - Require
empirical_premisetargets to carry no proof authority. - Detect duplicate locator + segment-hash pairs.
- Reject authority propagation from a target theorem back to source wording.
- Reject reviewed mappings to superseded/quarantined packets without an explicit reason.
- Fail public export for pending/restricted rights or disallowed excerpts.
- Require authoritative Proof Search artifact-index resolution in the Principia release workflow.
Generated artifacts
manifests/source_object_index.jsonmanifests/source_relation_index.jsonmanifests/principia_coverage.jsonreports/principia_source_map.md
Required tests
Include positive and adversarial tests for valid source packets, missing pins, locator errors, hash mismatches, duplicate sources, illicit proof authority, unsafe training defaults, pending rights with public excerpts, missing or mistyped targets, formalization-to-nonformal mappings, empirical-to-proof-bearing mappings, superseded targets, deterministic authoring, export separation, and unchanged behavior of author_packet.py.
CI gates
- changed Lean modules kernel build through feat(corpus): NumberTheory/PrimeDistribution wave 1 — Erdős-647 analytic core (#12) #16 or equivalent;
- regenerated packet manifests produce no diff;
- regenerated Lean root produces no diff;
- source relation and export tests pass;
- clean release replay validates with an authoritative artifact index.
Acceptance criteria
Existing packets remain valid and canonically identical unless a documented migration requires a version bump. A source packet cannot accidentally become a theorem, public training object, MathCorpus-authored text, or rights-cleared export through defaults.
Activity