AAT/SFT Research Notes

SFT Part IV

Principles and Theorems

Part IV records the theorem-shaped claims SFT can make only under explicit support semantics, step simulation, safe regions, coverage policy, and observation boundaries.

ForecastCone narrowing

If a specification adds sound constraints, preserves the intended feature direction, and excludes a selected witness family, then the relevant cone narrows under the selected support semantics.

Set-valued schema
PointwiseSupportInclusion(U2, U1)
  + StepSimulation(U2, U1, relation)
  + F2 relation F1
  -> ForecastCone(F2, U2, h)
     projects into ForecastCone(F1, U1, h)

The proof idea is induction on horizon. Each accepted U2-step is simulated by a U1-step while the relation between fields is maintained.

The claim level is L2 for set-valued support semantics and step simulation, L3 only after transition-kernel semantics are supplied, and L4 only after dataset calibration.

Support safety

Safe regions live on state or signature observations, not on operation names alone. Support safety says that selected accepted operations preserve a selected safe region under a selected observation model.

  • Relative guarantee The claim applies to accepted trajectories and selected safe regions.
  • No global future safety Unmodeled operations, missing axes, and different horizons remain outside the claim.
Support safety schema
StateInSafeRegion(O, R, F)
  + accepted steps are selected from U
  + SupportOperationsPreserveSafeRegion(U, O, R)
  -> accepted trajectory remains in R

Proposal accounting and review mediation

Dissipation is not a formal conservation law. The formal vocabulary is `ProposalAccounting` and `ReviewMediation`: classifying proposal pressure as accepted, rejected, delayed, unresolved, coordination record, runtime pressure estimate, or unaccounted remainder.

Review, CI, type checking, and architecture rules produce records that feed field update and governance design.

ProposalAccounting
ProposalAccounting(raw_proposal_universe)
  classifies proposal pressure as:
    accepted
    rejected
    delayed
    unresolved
    coordination_record
    runtime_pressure_estimate
    unaccounted_remainder

Feedback boundary update

Observed transitions, signature deltas, obstruction witnesses, review outcome, CI outcome, and runtime feedback can update the posterior field by making forecast error and missing evidence explicit.

Boundary-aware update
forecast
  + observed transition
  + forecast error
  -> posterior field that records
     missing evidence, unexpected witnesses,
     policy drift, and non-conclusions

This is update soundness as record preservation. It is not a theorem that every update narrows the next forecast.

Stable regions and recurrent paths

Attractor and basin language requires extra semantics. The set-valued core separates may reachability, must reachability, stable region, and reachable preimage before adding probability or recurrence claims.

Minimal vocabulary
MayReach_h(F, U, A)
MustReach_h(F, U, A)
StableRegion(U, A)
ReachablePreimage_h(U, A)

Attractor language is allowed only after the semantics needed for stability, recurrence, policy preference, or probability have been made explicit. Otherwise the safe vocabulary is `DefaultPath`, `RecurrentPattern`, `StableRegion`, and `ReachablePreimage`.

Principle boundary and non-conclusions

Part IV contains theorem-shaped schemas, not unrestricted guarantees about software projects. Cone narrowing is relative to selected support, witness family, and horizon; support safety is relative to accepted trajectories and measured safe regions; proposal accounting depends on explicit coverage and overlap policy.

  • Not global risk reduction Complexity may move to another witness family or unmeasured axis.
  • Not automatic accuracy improvement Feedback update preserves records; calibration is a separate empirical claim.
  • Not physical attractor dynamics Attractor and basin require additional semantics before stronger claims are made.