Calculus and Extensions

Architecture operation

`ArchitectureOperation` maps one architecture object to another under a theorem boundary. The operation includes support, precondition, transition relation, invariant preservation claim, witness mapping, theorem boundary, and non-conclusions.

ArchitectureOperation X Y
  = support
  + precondition
  + transition relation
  + invariant preservation claim
  + witness mapping
  + theorem boundary
  + non-conclusions

Operation laws

Under fixed observation and theorem-boundary compatibility, operations can be read as a partial category with identity, composition, and associativity under observation. Stronger laws such as replacement equivalence, protection idempotence, repair monotonicity, and synthesis soundness depend on their own assumptions.

Operation families and invariant families also form a weak Galois-style correspondence: requiring stronger invariants reduces allowed operations, while allowing more operations reduces the invariant family that can be guaranteed.

Feature extension

`FeatureExtension` moves from an existing architecture into a larger one while keeping a feature view. Static split, interface declarations, lifting, runtime preservation, and semantic preservation are not bundled into the base extension; they are separate evidence packages.

ExtensionObstruction
  = inherited core obstruction
  + feature-local obstruction
  + interaction obstruction
  + lifting failure
  + filling failure
  + complexity transfer
  + residual coverage gap

Operation families

The calculus treats common refactoring and architecture moves as operation families sharing the same boundary-indexed shape. `compose`, `replace`, `refine`, `abstract`, `split`, `merge`, `isolate`, `protect`, `migrate`, `reverse`, `contract`, `repair`, and `synthesize` can each be useful, but the family name is not itself a proof.

Each operation needs its own support, precondition, transition relation, invariant preservation claim, witness mapping, and non-conclusions. A replacement theorem, a migration theorem, and a protection theorem may share notation while requiring different observation and exactness assumptions.

operation tag
  + selected support
  + precondition
  + invariant family
  + witness mapping
  + theorem boundary
  -> bounded conclusion

Proof obligations

To turn an architecture operation into a theorem package, the operation must expose the data that a proof can actually use. This is the calculus-level version of claim discipline.

• Well-formed support The source, target, and affected sub-universe are explicit enough to state the transition.
• Precondition and transition The operation says when it is allowed and what relation connects source and target.
• Invariant and witness mapping The proof states which invariant is preserved and how selected witnesses are removed, preserved, introduced, or transferred.
• Conclusion boundary The theorem records which axes are not claimed to improve and which evidence remains outside the operation.

Extension theorem schema

Feature extension is the running operation family because it forces all boundaries to appear at once: inherited core structure, feature-local behavior, interaction with the core, lifting through declared interfaces, semantic filling, and residual coverage.

FeatureExtension X X'
  + StaticSplitFeatureExtension evidence
  + selected feature-view section laws
  + SplitExtensionLiftingData
  + runtime / semantic preservation evidence
  + theorem boundary B
  -> bounded extension claim within B

The structural extension formula classifies where a witness comes from. It does not say the classes are disjoint and does not provide global witness completeness by itself.

Extension evidence

A base `FeatureExtension` only says that an existing core has been embedded into a larger object with a feature view. Stronger readings require additional evidence packages: static split, declared interface use, selected feature-view section laws, lifting data, runtime preservation, and semantic preservation.

• StaticSplitFeatureExtension Evidence about static relations and boundary policy for the extension.
• FeatureViewSectionPackage Evidence that the feature view reads the selected feature correctly under the observation model.
• SplitExtensionLiftingData Evidence that selected feature steps lift through the declared interface.

Lean status

The Lean API contains defined operation schemas, accessor theorems, bounded calculus laws, feature-extension structures, split-extension lifting APIs, and structural extension formula entrypoints. Some components are proved theorem packages and some remain defined-only APIs or docs-facing metadata.