Research-Stack/6-Documentation/docs/semantics/COMPRESSION_MECHANICS_EXECUTION_PLAN.md

# Compression Mechanics Execution Plan

This plan defines the work needed to verify compression approaches through a
rigorous chain:

1. informational compression evidence
2. thermodynamic lower bounds
3. physically admissible substrate witnesses
4. end-to-end bridge theorems

The plan is organized into phases, steps, and sub-steps with explicit completion
metrics.

## Phase 0: Scope Lock

Goal:

- freeze the theorem target so implementation work does not drift back into
  unsupported chemistry claims

### Step 0.1: Lock the proof target

Sub-steps:

1. State the target theorem family in one sentence.
2. State what is explicitly out of scope.
3. Bind the target to the Nature-family source pack in
   `NATURE_RIGOR_PREP.md`.

Completion metrics:

- one canonical statement of the goal exists in repo docs
- one explicit out-of-scope list exists in repo docs
- every later theorem module can be mapped to one section of the source pack

### Step 0.2: Lock the minimal variable set

Sub-steps:

1. Define the minimal quantities that every later phase may use.
2. Reject unsupported quantities from the proof core.
3. Separate proof-layer quantities from approximation-layer quantities.

Completion metrics:

- proof core variables list is finite and documented
- no theorem in later phases depends on free-form strings or vague descriptors
- no step assumes atomic weight alone can determine structure or admissibility

Suggested proof-core variables:

- source trace
- model trace
- block cost
- accuracy witness
- erased-information witness
- nonequilibrium cost
- substrate witness
- admissibility predicate

## Phase 1: Informational Core

Goal:

- prove that the compression side is mathematically well-defined before any
  physics is attached

### Step 1.1: Define compression evidence semantics

Sub-steps:

1. Create `Semantics.CompressionEvidence`.
2. Define a finite alphabet type.
3. Define block, trace, model state, and cost witness types.
4. Define deterministic scoring semantics.

Completion metrics:

- Lean file exists under `0-Core-Formalism/lean/Semantics/Semantics/`
- every new `def` has either an `#eval` witness or theorem in the same file
- no `Float` appears in the new core module
- no open string matching appears in core decisions

### Step 1.2: Define code-length / accuracy objects

Sub-steps:

1. Define code-length witness in Q16.16-compatible form.
2. Define accuracy witness for reconstruction or prediction quality.
3. Define contextual and flat model interfaces.

Completion metrics:

- code-length object is typed and total
- accuracy witness is typed and total
- contextual and flat models can be compared on the same trace

### Step 1.3: Prove first informational theorem

Sub-steps:

1. Formalize deterministic conditional source case.
2. Prove a matching contextual model is no worse than a flat model.
3. Add one concrete `#eval` example demonstrating the bound.

Completion metrics:

- theorem compiles without `sorry`
- theorem statement is independent of any physics module
- at least one example trace evaluates to the expected inequality witness

Exit criteria for Phase 1:

- `Semantics.CompressionEvidence` builds in isolation
- one nontrivial compression theorem is proven
- the theorem uses only informational quantities

## Phase 2: Thermodynamic Layer

Goal:

- connect irreversible information change to a rigorous physical lower bound

### Step 2.1: Define thermodynamic primitives

Sub-steps:

1. Create `Semantics.LandauerCompression`.
2. Define erased-information witness.
3. Define nonequilibrium cost object.
4. Define lower-bound function for irreversible steps.

Completion metrics:

- Lean file exists and compiles in isolation
- every primitive has a documented physical meaning
- no theorem depends on unformalized external numerics

### Step 2.2: Bind informational state change to thermodynamic cost

Sub-steps:

1. Define irreversible update predicate.
2. Define mapping from compression step to erased-information witness.
3. Define lower-bound theorem target.

Completion metrics:

- there is a total function from compression step to thermodynamic witness
- irreversible and reversible cases are distinguished by a typed predicate
- at least one simple theorem covers the nonzero irreversible case

### Step 2.3: Prove the first physics bridge theorem

Sub-steps:

1. Prove positive erased-information witness implies nonzero lower bound.
2. Add example witnesses for zero and nonzero cases.
3. Document the theorem's exact scope and limitations.

Completion metrics:

- theorem compiles without `sorry`
- theorem is stated in terms of the defined typed quantities only
- example witnesses distinguish reversible from irreversible cases

Exit criteria for Phase 2:

- `Semantics.LandauerCompression` builds in isolation
- one theorem links compression evidence to a thermodynamic lower bound
- the repo now has a truthful information -> physics bridge

## Phase 3: Materials / Defect Witness Layer

Goal:

- define a physically meaningful substrate witness that can support or reject a
  proposed compression process

### Step 3.1: Define local physical witness objects

Sub-steps:

1. Create `Semantics.DefectMechanics`.
2. Define a finite substrate or neighborhood type.
3. Define local descriptors such as vacancy or charge witness.
4. Define a transport / dissipation witness.

Completion metrics:

- Lean file exists and compiles in isolation
- descriptors are finite, typed, and enumerable where needed
- no descriptor is represented by an open-ended string in core logic

### Step 3.2: Define admissibility predicates

Sub-steps:

1. Define heat-dissipation admissibility.
2. Define defect-energy admissibility.
3. Define transport-regime admissibility.

Completion metrics:

- each predicate is total
- each predicate has one `#eval` or theorem witness
- predicates can be combined without ambiguity into a single admissibility view

### Step 3.3: Prove the first substrate theorem

Sub-steps:

1. Define a minimal substrate witness record.
2. Prove that a substrate satisfying the threshold conditions is admissible.
3. Add one positive and one negative example witness.

Completion metrics:

- theorem compiles without `sorry`
- positive witness evaluates to admissible
- negative witness evaluates to not admissible

Exit criteria for Phase 3:

- `Semantics.DefectMechanics` builds in isolation
- one theorem certifies substrate admissibility
- local physical descriptors are separated from learned surrogate claims

## Phase 4: Compression <-> Mechanics Bridge

Goal:

- prove that a compression step is physically admissible on a specified
  substrate witness

### Step 4.1: Define bridge objects

Sub-steps:

1. Create `Semantics.CompressionMechanicsBridge`.
2. Import the informational, thermodynamic, and substrate layers.
3. Define a bridge record carrying all required witnesses.

Completion metrics:

- bridge record contains no undocumented fields
- every bridge field comes from a previous phase
- no direct dependency on approximation-layer ML outputs exists in the theorem core

### Step 4.2: Define admissible compression step

Sub-steps:

1. Define the predicate that a compression step is physically admissible.
2. Separate proof obligations for informational validity, lower-bound validity,
   and substrate validity.
3. Add a helper theorem for assembling the three obligations.

Completion metrics:

- predicate is total
- obligations are decomposed into named lemmas
- at least one helper theorem reduces final theorem complexity

### Step 4.3: Prove the bridge theorem

Sub-steps:

1. Prove that a compression step with valid informational witness, valid
   thermodynamic lower bound, and admissible substrate is physically admissible.
2. Add one end-to-end worked example.
3. Document what this theorem does not prove.

Completion metrics:

- theorem compiles without `sorry`
- one complete end-to-end example evaluates successfully
- limitations are written explicitly in the module or companion doc

Exit criteria for Phase 4:

- repo contains one honest end-to-end compression-to-physics theorem
- theorem depends only on proven or explicitly witnessed inputs
- no unsupported chemistry claims remain in the proof path

## Phase 5: Approximation / Surrogate Layer

Goal:

- allow ML or symbolic-regression accelerators to be used without confusing them
  with the proof layer

### Step 5.1: Define approximation boundary

Sub-steps:

1. Document that surrogates are extraction targets or numerical witnesses.
2. Define accepted surrogate outputs as data artifacts, not axioms.
3. Define a verification boundary for importing surrogate results.

Completion metrics:

- documentation explicitly separates proof from surrogate
- surrogate artifacts are never imported as trusted theorems
- each imported surrogate result must attach to a typed witness object

### Step 5.2: Add one surrogate-backed witness path

Sub-steps:

1. Choose one descriptor class such as vacancy witness.
2. Define how an external predictor may populate it.
3. Prove that the bridge theorem only uses the populated witness, not the model internals.

Completion metrics:

- surrogate-backed witness path exists without changing proof-layer theorems
- theorem statements remain independent of the surrogate architecture
- repo documentation states what is proved and what is estimated

Exit criteria for Phase 5:

- the project can use practical predictors without collapsing rigor
- proof-layer semantics remain stable if the surrogate changes

## Phase 6: Integration and Validation

Goal:

- integrate the new modules into the repo and validate them against the repo's
  operating rules

### Step 6.1: Local build validation

Sub-steps:

1. Build each new module in isolation.
2. Record any dependencies that prevent integration.
3. Fix isolated issues before touching broader imports.

Completion metrics:

- each new module builds individually
- no new module contains `sorry`
- no new module introduces new dependencies

### Step 6.2: Repo integration

Sub-steps:

1. Add imports to the appropriate aggregate files only after isolated success.
2. Re-run `lake build`.
3. Separate pre-existing failures from new failures.

Completion metrics:

- import graph is minimal
- any build failures introduced by integration are attributable and fixed
- no unrelated files are changed during integration

### Step 6.3: Documentation closure

Sub-steps:

1. Update the rigor prep note with implemented modules.
2. Add a short theorem inventory.
3. Record any deferred work explicitly.

Completion metrics:

- theorem inventory exists in repo docs
- every implemented module has a corresponding documentation entry
- deferred items are listed as explicit future work, not hidden gaps

Exit criteria for Phase 6:

- new modules are integrated cleanly
- documentation and code agree
- completion can be reported against explicit metrics

## Overall Completion Metrics

The program is complete when all of the following are true:

1. `Semantics.CompressionEvidence` exists, builds, and contains at least one
   nontrivial informational theorem.
2. `Semantics.LandauerCompression` exists, builds, and contains at least one
   theorem linking erased-information witness to nonzero lower bound.
3. `Semantics.DefectMechanics` exists, builds, and contains at least one
   substrate admissibility theorem.
4. `Semantics.CompressionMechanicsBridge` exists, builds, and contains one
   end-to-end admissibility theorem.
5. Every new theorem is free of `sorry`.
6. Every new `def` has an `#eval` or theorem witness.
7. No new core module uses `Float`.
8. No new core decision procedure uses open string matching.
9. No new dependencies are added.
10. The final documentation states clearly what is proved, what is witnessed, and
    what is only approximated.

## Reporting Template

Use this template at the end of each implementation checkpoint:

- Phase completed:
- Steps completed:
- Files added or changed:
- Theorems added:
- `#eval` witnesses added:
- Isolated build status:
- Full `lake build` status:
- Deferred items: