Uniqueness.lean

View source on GitHub

InfoTy / ForwardStage

Interface types are modeled as an enum (raw, encoded, indexed, selected, ranked, persisted, policy). Each forward stage has a domain (input type) and codomain (output type). The handshake condition is: the codomain of stage i must equal the domain of stage i+1.

def ForwardStage.dom : ForwardStage → InfoTy
  | .perceive => .raw
  | .cache    => .encoded
  | .filter   => .indexed
  | .attend   => .selected
  | .remember => .ranked

Consumer uniqueness theorems

Five theorems, one per interface type: only Perceive consumes raw, only Cache consumes encoded, only Filter consumes indexed, only Attend consumes selected, only Remember consumes ranked. Each is proved by case analysis — try every stage, only one matches.

forward_ordering_unique

The main theorem. Any handshake-compatible ordering that starts from raw must equal the canonical ordering (Perceive → Cache → Filter → Attend → Remember) at every position. The type chain forces each slot.

theorem forward_ordering_unique
    (ord : Fin 5 → ForwardStage)
    (hcompat : handshake_ok ord)
    (hfirst : (ord ⟨0, _⟩).dom = .raw)
    : ∀ i : Fin 5, ord i = canonical i

The proof chains through positions: position 0 must be Perceive (only consumer of raw), position 1 must be Cache (only consumer of encoded, which Perceive produces), and so on through all five positions.

no_forward_consumes_policy

No forward stage takes policy as input. Consolidate produces policy, so nothing in the forward chain can follow it. This is why Consolidate must be the backward pass, not a forward stage.

consolidate_has_no_slot

Consolidate cannot be spliced into the forward chain. Even if some stage produced persisted (Consolidate's input), the next stage would need to consume policy (Consolidate's output), and no forward stage does.

pipeline_unique

The combined uniqueness result: (1) the forward ordering is forced by the type chain, (2) Consolidate's output type has no forward consumer, (3) Consolidate's input type has no forward consumer. Therefore: five forward stages in canonical order plus Consolidate as backward pass is the only configuration whose types compose. This is why the framework claims exactly six roles in exactly this order.

Connections

• Pipeline.lean — imported; defines the Pipeline structure whose ordering is proved unique
• Contracts.lean — imported; the handshake condition on type compatibility
• Handshake.lean — the cross-cycle coupling that Consolidate participates in