Handshake.lean

View source on GitHub

Handshake

A handshake is a pair of contracts (postcondition of the preceding stage, precondition of the following stage) plus a proof that the postcondition implies the precondition. This is what makes adjacent stages compatible.

structure Handshake (β : Type) where
  post : Contract β
  pre  : Contract β
  compatible : ∀ b : β, post b → pre b

PipelineHandshake

The full pipeline handshake: four forward handshakes (Perceive→Cache, Cache→Filter, Filter→Attend, Attend→Remember) plus one cross-cycle handshake (Consolidate→Attend). The cross-cycle one is special: what Consolidate guarantees at cycle k is what Attend requires at cycle k+1.

cycle_preserves_policy

The coupling lemma. This says: if Consolidate preserves its postcondition (for all policies and persisted states), then after one pipeline cycle, the output policy satisfies Attend's precondition for the next cycle.

theorem cycle_preserves_policy [Monad M] [LawfulMonad M] [Support M]
    (h : PipelineHandshake I) (p : Pipeline M I)
    (hcon : ∀ (pol : I.policy) (per : I.persisted),
      ∀ pol' : I.policy, Support.support (p.consolidate pol per) pol' →
        h.consolidate_attend.post pol')
    (policy : I.policy) (input : I.raw)
    : ∀ result : I.policy × I.persisted,
        Support.support (p.cycle input policy) result →
        h.consolidate_attend.pre result.1

The proof unfolds the cycle definition and peels apart each bind using support_bind. After extracting the forward stages, Remember, and Consolidate, it applies the handshake compatibility to convert the postcondition into the precondition.

# Handshake: post(stage N) implies pre(stage N+1)
# If the guarantee breaks, the next stage can't trust its input.

def perceive(raw):
    return {"type": "encoded", "data": raw.upper()}

def cache(encoded):
    assert encoded["type"] == "encoded"  # pre: must be encoded
    return {"type": "indexed", "key": hash(encoded["data"]),
            "data": encoded["data"]}

def filter_stage(indexed):
    assert indexed["type"] == "indexed"  # pre: must be indexed
    return {"type": "selected", "data": indexed["data"][:3]}

# Each postcondition matches the next precondition:
x = perceive("hello world")
print(f"perceive post: type={x['type']}")

y = cache(x)  # pre satisfied: type == 'encoded'
print(f"cache post:    type={y['type']}")

z = filter_stage(y)  # pre satisfied: type == 'indexed'
print(f"filter post:   type={z['type']}")

print("\nAll handshakes hold — pipeline composes safely.")

cycle_preserves_policy_at

A weaker form: Consolidate's postcondition only needs to hold for the specific input policy (not all policies). Needed for up-induction on the fractal tower where we only know the postcondition for the starting policy.

cycle_consolidate_support

An extraction lemma: any output policy from a cycle came from Consolidate applied to the input policy. Useful for decomposing the tower construction.

step_position_injective

The six pipeline steps have a total order (positions 0-5). The mapping from step to position is injective — distinct steps have distinct positions.

NonExpanding / StrictlyLossy

Information monotonicity. A kernel is non-expanding if no output has more information than the input. Strictly lossy means at least one input sees a strict decrease. These formalize that information flows downhill through the pipeline.

non_expanding_compose

Composing two non-expanding kernels gives a non-expanding kernel. Information can only decrease, never increase, through composition.

PipelineFunctor / def FunctorNatural

A structure-preserving map between two pipeline instances. If domain A and domain B both implement six roles with compatible types, the mapping between them is a functor. Naturality means: mapping commutes with each role. The framework lexicon maps how this functor language translates across mathematical communities.

TracedPipeline

The feedback trace: Remember's output feeds back to Perceive's input. In the self-recursive case, persisted = raw. A traced pipeline can run autonomously, feeding each cycle's output into the next cycle's input.

Connections

• Pipeline.lean — imported; handshakes apply to the Pipeline structure
• Contracts.lean — imported; handshakes chain contracts
• Fractal.lean — the coupling lemma is the key hypothesis for the recursive tower
• Hoare/Comp.lean — restates the handshake chain as Hoare triple composition
• Hoare/Divergence.lean — NonExpanding characterized as threshold triples