AAT/SFT Research Notes

SFT Part II

Algebraic and Observational Basis

Part II fixes the dependency direction: AAT provides local algebra, ArchSig provides observations and field estimates, and SFT keeps claim levels explicit.

AAT dependency

SFT sits on AAT, but AAT does not depend on SFT. AAT turns software architecture into local algebra. SFT uses that algebra as architecture projection, local transition law, observable coordinate, and admissibility boundary.

  • Architecture projection SFT reads `ArchitectureObject` as the architecture object projected from a `SoftwareField`.
  • Local transition premise `ArchitectureOperation` becomes a local premise for accepted or proposed field transitions.
  • Forecast boundary AAT theorem boundaries and non-conclusions become SFT forecast boundaries.
Direction of dependency
AAT does not depend on SFT.
SFT depends on AAT.
Minimal interface map
architecture projection   -> ArchitectureObject
local transition law     -> ArchitectureOperation
protected constraint     -> InvariantFamily
defect / repair target   -> ObstructionWitness
observable coordinate    -> ArchitectureSignature
admissibility boundary   -> theorem boundary / non-conclusions
local path skeleton      -> ArchitecturePath

ArchSig bridge

ArchSig is the observation layer between real artifacts, AAT observables, and SFT field estimates. It reports measured axes, unmeasured axes, out-of-scope axes, evidence boundaries, and measurement non-conclusions.

Observation bridge
real artifacts
  -> ArchSig
  -> AAT observables
  -> SFT field estimates

Signature deltas are defined only where both sides are measured and axis-wise comparison is available. Unmeasured does not mean zero, and tool output is not a theorem.

ArchSigSFTReport
ArchSigSFTReport
  = action_class_candidates
  + target_architecture_regions
  + candidate_operation_families
  + comparable_signature_axes
  + expected_axis_delta_ranges
  + selected_obstruction_witness_families
  + missing_invariants
  + theorem_boundary_items
  + forecast_boundary
  + unknown_unmodeled_remainder
  + claim_level

Claim levels

SFT claims must state their observation, model, and calibration basis. The same sentence can have different status depending on whether it is conceptual, trace-grounded, set-valued, probabilistic, calibrated, or operationally deployed.

  • Level 0 Conceptual or diagnostic interpretation.
  • Level 1 Trace-grounded field diagnosis.
  • Level 2 Set-valued formal theorem schema.
  • Level 3 and above Transition-kernel models, calibrated forecasts, or deployed closed-loop governance systems.

The levels keep three claims apart: a formal AAT theorem, a set-valued SFT schema over an explicit support relation, and an empirical forecast validated against traces or deployed outcomes.

A good specification may narrow a cone under support inclusion and step simulation. Without calibration, that is not an empirical prediction theorem.

Basis boundary and non-conclusions

Part II is the bridge layer, so its main job is preventing category errors. ArchSig evidence may inform a field estimate, but it is not a Lean proof. AAT theorem status may supply a local premise, but it is not automatically software evolution forecast status.

  • Formal claim Lives in AAT or in a set-valued SFT schema with stated support and step semantics.
  • Tooling estimate Records measured axes, missing axes, evidence boundaries, and non-conclusions.
  • Empirical forecast Requires trace or dataset calibration; it is not obtained by renaming a theorem.