Repair and Dynamics

Repair and synthesis

A `RepairStep` is an operation intended to reduce a selected obstruction measure. A repair theorem must state which witness universe decreases, which invariant is preserved, which axes are not claimed to improve, and where side effects may appear.

RepairStep
  = source
  + target
  + selected obstruction measure
  + decrease theorem boundary
  + side-effect boundary

Synthesis constructs an architecture object or operation sequence satisfying constraints. A no-solution result needs a finite complete search universe, explicit constraint language, decision procedure, and coverage boundary; solver failure alone is not a mathematical certificate.

Complexity transfer

`ComplexityTransfer` captures the case where complexity or an obstruction appears to disappear only because it moved to another axis. AAT requires selected evidence, selected target, residual gap, and non-conclusion boundary before calling an obstruction eliminated.

Repair theorem schema

A repair theorem is intentionally narrow. It states that a selected measure decreases or a selected witness disappears, while preserving named invariants and recording all axes whose behavior is not concluded.

RepairStep X Y
  + selected witness universe W
  + obstruction measure m
  + invariant family I
  + side-effect boundary E
  ->
  m(Y) < m(X)
  + I is preserved within B
  + non-conclusions for untracked axes

Synthesis has a stronger burden. A generated candidate needs satisfaction evidence, while a no-solution claim needs a finite complete candidate universe and a checked decision procedure.

Signature trajectory

A repair is best read as a movement through signature space. The theorem may prove a decrease on one selected coordinate, while the trajectory records unchanged, transferred, introduced, or unmeasured coordinates elsewhere.

ArchitecturePath X0 Xn
  + selected repair steps
  + signature coordinates at each step
  + transferred or residual witnesses
  + non-conclusions
  -> bounded repair reading

This trajectory view is what prevents a local repair theorem from becoming a total quality claim.

Paths and filling

`ArchitecturePath` is an operation sequence. Two paths can reach the same feature outcome while preserving different invariants, introducing different witnesses, or tracing different signature trajectories.

`PathHomotopy` compares paths under selected generators and an observation model. Semantic diagram filling supplies evidence that different implementation paths give the same observation; a failed equality can become a `NonFillabilityWitness`.

Obs(lhs) != Obs(rhs)
  -> NonFillabilityWitness D

No-solution boundary

Synthesis can produce a candidate object, a repair sequence, or a no-solution certificate. The last case is the strongest and therefore needs the clearest boundary: a finite complete search universe, an explicit constraint language, a decision procedure, refuted candidate cases, and coverage assumptions.

Solver failure alone is not a mathematical certificate. It may be a tooling result, a timeout, or an unsupported-construct boundary. AAT keeps those cases separate from a proved no-solution theorem.

finite complete candidate universe
  + explicit constraints
  + decision procedure
  + refuted candidates
  + coverage boundary
  -> no selected solution

Path example

Two coupon implementations can reach the same visible checkout result while following different paths: one introduces a declared discount interface first, then adds the feature; the other adds a direct adapter call and later repairs the static graph. The final feature may look equivalent while the witness history and signature trajectory differ.

• Path invariant A property preserved at every step of the selected operation sequence.
• Homotopy generator A permitted rewrite between operation fragments under a selected observation model.
• Non-fillability witness Evidence that two paths fail to agree on the selected observation.

Lean status

Repair steps, repair synthesis, architecture paths, homotopy skeletons, diagram fillers, non-fillability witnesses, and selected observation-invariance bridges are tracked in the Lean theorem index. The public reading is bounded: global semantic completeness and all-axis improvement are not current conclusions.