refactor(seed): remove legacy semantics and sharpen formal boundaries

[attractor-set]

refactor(seed): remove legacy semantics and sharpen formal boundaries

Summary

This PR performs a deep semantic cleanup of ASET Seed.

It removes accumulated RC11/RC12-era concepts from the active Seed surface, separates Seed-owned state from environment observations, makes evaluation an observer rather than a state transition, simplifies the authority boundary, strengthens the canon-to-TLA refinement architecture, and aligns assurance claims with what is actually proved.

The goal is not to add new Seed behavior. The goal is to make the active specification reflect the minimal semantics that Seed currently implements and proves.

Main changes

1. Separate Seed state from environment state

Seed-owned mutable state is now explicitly:

• requestMeta
• terminalMeta

Conflict observation is modeled separately as environment state:

• conflicts

This removes the previous ambiguity where an environment observation could mutate something described as canonical Seed state.

The formal model now distinguishes:

• Seed transitions that may change Seed-owned state
• environment observations that preserve Seed-owned state

The corresponding formal guarantees include:

• SpecImpliesSeedStateChangesOnlyByRecognizedTransition
• SpecImpliesConflictObservationPreservesSeedState

2. Make evaluation an observer

EVALUATE_RESOLUTION is no longer modeled as an artificial stuttering state transition.

Resolution evaluation is treated as an observer over current state:

• ResolutionOf
• EffectPermitted

This better reflects the actual semantics: evaluation reads authoritative state but does not mutate it.

3. Clarify invalid-material semantics

Invalid, malformed, unverifiable, or otherwise non-authoritative material does not mutate canonical Seed state and does not override an otherwise unique valid terminal resolution.

A unique valid terminal ALLOW therefore remains ALLOW in the presence of additional invalid material.

UNKNOWN is reserved for cases where an authoritative unique terminal result cannot be established, including conflicting valid terminal material.

An adversarial conformance case was added for:

valid ALLOW
+
malformed/non-authoritative extra material
→
ALLOW remains authoritative

This avoids making invalid material a trivial denial-of-service mechanism.

4. Simplify the Authority boundary

The active Seed no longer claims to model or prove a concrete delegation/grant-chain mechanism.

The formal boundary is now expressed in terms of recognized exact-binding authorization:

• RequestAuthorityBindings
• TerminalAuthorityBindings

Concrete mechanisms such as:

• signatures
• certificates
• grant chains
• delegation formats
• cryptographic verification

remain outside the Seed semantic kernel.

Seed consumes their recognized result rather than defining their implementation.

5. Remove inactive RC11/RC12 protocol legacy

The active protocol surface was reduced substantially.

Before:

• 48 active protocol JSON schemas

After:

• 11 active protocol JSON schemas

Legacy schemas related to older permit, outcome, membership, context, reconciliation, execution-intent, authority-grant, and related RC11/RC12 designs were removed from the active Seed surface.

Historical frozen artifacts remain preserved separately.

The frozen RC11 bundle continues to validate successfully.

6. Remove obsolete formal modules

Legacy formal modules that no longer define the active Seed semantics were removed from the active formal surface, including the old bootstrap/RC12 model artifacts.

The active formal specification is now centered on the current Seed resolution kernel and its proofs.

7. Strengthen canon-to-TLA refinement

The generated SeedCanonProjection.tla is now a standalone projection of the machine-readable canon.

Previously, the generated projection depended directly on SeedResolution, weakening the independence of the refinement check.

The V4 structure is now:

machine-readable canon
        ↓
standalone SeedCanonProjection
        ↓
explicit refinement mapping
        ↓
SeedResolution

The projection does not EXTEND or import SeedResolution.

The refinement proof explicitly instantiates the standalone canon model onto the handwritten formal state.

This makes the canon-to-TLA relationship materially stronger and removes the previous projection-to-target coupling.

8. Make bounded exploration saturating

The executable bounded model checker no longer stops at an arbitrary fixed depth.

It explores the finite model until a fixpoint is reached.

Current saturated model:

• reachable states: 2,500
• transitions: 5,500
• terminal states: 1,800
• TLA-aligned formal properties: 14
• saturation reached: true

This makes the reported state count an exhaustive result for the selected finite instance rather than a depth-limited prefix.

9. Align assurance claims with proof boundaries

The assurance layer now distinguishes between:

• properties proved in TLA/TLAPS
• executable/static properties
• external trust-boundary guarantees

Current assurance taxonomy:

• 14 TLA/TLC properties
• 5 executable/static/boundary properties
• 19 total assurance properties

Proof traceability covers all 14 TLA properties without claiming that external cryptographic or authority-recognition mechanisms are proved inside Seed.

10. Preserve semantic mutation and conformance closure

The conformance corpus now contains 25 cases, including the new invalid-material adversarial case.

Semantic mutation closure remains complete:

• mutations: 13
• killed: 13
• survived: 0

Resulting architecture

The active Seed semantic model is now approximately:

Immutable/trust-boundary context
├── RequestAuthorityBindings
├── TerminalAuthorityBindings
└── RecognizedTerminalCommitments

Seed-owned mutable state
├── requestMeta
└── terminalMeta

Environment state
└── conflicts

Derived state / observers
├── Requests
├── TerminalRequests
├── ResolutionOf
└── EffectPermitted

The distinction between decision state, environment observations, provenance, and external trust recognition is now explicit.

Formal assurance

Validated against the pinned formal toolchain:

TLC

TLC_MODEL_CHECK=PASS

TLAPS

TLAPS_OBLIGATIONS=159
TLAPS_VERDICT=PASS

Final theorems include:

• SpecImpliesAlwaysSeedStateSafety
• SpecImpliesRequestsAppendOnly
• SpecImpliesTerminalRecordsImmutable
• SpecImpliesSeedStateChangesOnlyByRecognizedTransition
• SpecImpliesConflictObservationPreservesSeedState

Canon-to-TLA refinement

CANON_TLA_REFINEMENT_OBLIGATIONS=3
CANON_TLA_REFINEMENT_VERDICT=PASS

Final theorem:

SeedResolutionBehaviorallyEquivalentToCanonProjection

Unlike the previous projection profile, the canon projection used by this proof is standalone and does not depend on the target SeedResolution module.

Executable assurance

Current saturated bounded model:

MODEL_CHECK_STATES=2500
MODEL_CHECK_TRANSITIONS=5500
MODEL_CHECK_TERMINAL_STATES=1800
MODEL_CHECK_FORMAL_PROPERTIES=14
MODEL_CHECK_SATURATED=true
MODEL_CHECK_VERDICT=PASS

Mutation testing:

SEMANTIC_MUTATIONS=13
SEMANTIC_MUTATIONS_KILLED=13
SEMANTIC_MUTATIONS_SURVIVED=0
SEMANTIC_MUTATION_VERDICT=PASS

Traceability:

ASSURANCE_TRACEABILITY=PASS
PROOF_TRACEABILITY=PASS
CANON_TLA_REFINEMENT_CHECK=PASS
INVARIANT_COVERAGE=PASS

Scope

This PR intentionally does not introduce:

• cryptographic accumulators
• Merkle/MMR structures
• signature algorithms
• concrete certificate formats
• delegation-chain protocols
• execution orchestration
• higher-level ASET extensions

Those mechanisms remain outside the minimal Seed semantic kernel.

Compatibility and history

Historical frozen artifacts are preserved.

This PR removes legacy material from the active semantic surface rather than rewriting project history.

The purpose is to make the current normative Seed specification smaller, clearer, and more auditable while retaining historical evidence independently.

Why this refactor

Over several iterations, Seed accumulated terminology and protocol artifacts from earlier architectural stages.

Some of those concepts were no longer part of the actual resolution kernel but remained present in schemas, documentation, assurance metadata, or formal interfaces.

That created unnecessary ambiguity about:

• what Seed owns
• what is environment input
• what is merely provenance
• what is externally recognized
• what is formally proved
• what remains historical or implementation-specific

This refactor removes that ambiguity.

The resulting Seed is closer to a minimal specification in which each retained concept has an explicit semantic role and each formal claim corresponds to an actual proof boundary.