# 999.52 Proof Engineering Memory And Proof-Fragment Distillation

## Why this backlog item exists

AITP already has most of the raw ingredients for durable formal-proof
engineering memory:

- run-local `strategy_memory.jsonl` rows can already record helpful or harmful
  patterns and are consumed by `mode_learning`
- `proof_fragment` and `derivation_step` are already legal `candidate_type`
  and canonical `unit_type` families
- runtime proof artifacts such as Lean-ready packets and proof-repair plans
  already exist

What is still missing is the connective tissue.

Today the system can:

- remember strategy rows locally inside one run
- render runtime-side learning summaries
- reserve canonical family names for proof material

But it still cannot:

- record proof-engineering patterns through the normal strategy-memory API
- distill those rows into `proof_fragment` candidates
- or promote that knowledge into canonical `L2` so later topics can reuse it

That leaves formal-theory work with a broken memory ladder:

`proof debugging in one run`
-> `runtime memory summary`
-> `stop`

instead of:

`proof debugging in one run`
-> `strategy memory row`
-> `proof_fragment candidate`
-> `L4` review / promotion gate
-> `canonical proof_fragment`

## Current repository reality

The current codebase state is:

- `strategy_memory` is implemented and consumed, but the allowed
  `strategy_type` values are still oriented toward search/verification/debug
  patterns rather than explicit proof-engineering knowledge
- `proof_fragment` is already listed as a legal family in the canonical unit
  schema and candidate schema
- `LAYER2_OBJECT_FAMILIES.md` already gives `proof_fragment` and
  `derivation_step` semantic roles
- canonical storage routing in `knowledge_hub/l2_graph.py` does not yet route
  `proof_fragment` or `derivation_step` into concrete directories
- there is no distillation path from runtime proof memory into canonical
  proof-fragment candidates

This means the ontology is already reserved.
The missing work is implementation and governance closure, not another family
explosion.

## Recommended implementation stance

Do not solve this by inventing several new top-level canonical families.

The better path is:

1. extend runtime strategy memory to support proof-engineering patterns
2. keep strategy memory runtime-side and non-authoritative
3. add family-specific payload contracts for canonical `proof_fragment`
4. distill high-confidence runtime rows into `proof_fragment` candidates
5. promote only through the existing review and approval path

This keeps the current AITP honesty boundary intact:

- runtime memory can be cheap and local
- canonical `L2` still requires governed promotion

## Concrete target shape

### A. Runtime-side proof-engineering memory

Extend the allowed `strategy_type` set so the formal-theory lane can record
patterns such as:

- `proof_engineering`
- `api_workaround`
- `failure_pattern`

Keep using the existing row structure:

- `summary`
- `lane`
- `outcome`
- `confidence`
- `reuse_conditions`
- `do_not_apply_when`
- `input_context`
- `evidence_refs`

This lets `mode_learning` benefit immediately without requiring canonical
schema work first.

### B. Canonical proof-fragment payload contract

Do not replace the shared canonical-unit shell.

Instead add a family-specific payload contract for `proof_fragment` covering:

- reusable goal shape
- construction steps
- API surface
- failure signatures / common pitfalls
- reuse conditions
- do-not-apply conditions

That keeps `proof_fragment` aligned with the existing canonical model instead
of creating a parallel one-off theorem-engineering schema stack.

### C. Distillation before promotion

Add one explicit distillation step:

`strategy_memory row`
-> `proof_fragment candidate`

Only rows that meet an explicit threshold should distill automatically, for
example:

- `lane == formal_theory`
- `outcome == helpful`
- confidence above a declared threshold
- at least one durable evidence ref

Promotion into canonical `L2` should still go through the existing candidate
review / gate path.

## What this item should not do

This backlog item should not:

- declare all proof-debugging notes canonical by default
- bypass `L4` review because the pattern "felt useful"
- add several new proof-only unit families before `proof_fragment` is actually
  used well
- expand into whole-topic automated formalization
- claim Lean-bridge maturity by itself

## Likely files and surfaces involved

- `research/knowledge-hub/knowledge_hub/aitp_service.py`
- `research/knowledge-hub/knowledge_hub/mode_learning_support.py`
- `research/knowledge-hub/knowledge_hub/l2_graph.py`
- `research/knowledge-hub/canonical/canonical-unit.schema.json`
- `research/knowledge-hub/feedback/schemas/candidate.schema.json`
- `research/knowledge-hub/canonical/LAYER2_OBJECT_FAMILIES.md`
- one new proof-fragment payload schema under `research/knowledge-hub/schemas/`
- runtime and promotion tests that prove the full bridge works

## Promotion guidance

Promote this backlog item when:

- real formal-theory topic work starts generating repeated proof-engineering
  lessons worth reusing
- strategy memory is no longer enough because cross-topic reuse is needed
- or the current real-topic E2E/postmortem identifies proof-memory loss as a
  concrete blocker

Do not promote it just because `proof_fragment` exists in the ontology.
Promote it when the missing bridge becomes an actual workflow pain point.
