Alignment of the Enter interface

The following clauses describe the optional calculus interface. They are not premises of Lemma lem:onelayer, Lemma lem:dod, or Theorem thm:cone, which are channel theorems. A concrete calculus must discharge them on its own stated typing and evaluation domain.

E1: Termination.

Selected well-typed programs terminate. A strongly normalizing calculus supplies this at the reduction level; a finite acyclic instruction tree supplies it for the explicit fragment here. To obtain a finite evaluation tree from strong normalization one also uses the finite-branching evaluation interface. External idle ticks are not reductions.

E2: Confluence and disjoint commutation.

The complete denotation is independent of legal evaluation strategy. Disjoint enabled quantum operations commute. Global confluence must be supplied separately: commutation of only disjoint redexes does not logically imply confluence for every possible pair of enabled redexes. The source comparison is Landmark I thm:confluence; fixed-network channel ordering is the different statement in En03-A thm:retiming CheungI,CheungEn03.

E3: Internal no-signalling.

Complete programs on disjoint owned quantum and classical interfaces cannot change each other's unconditioned output law. The source comparison is Landmark I thm:internal-ns CheungI. On the substrate, complete ownership and controller support remain explicit modeling conditions.

E4: Records.

Destructive measurement, coherent recording, and surviving quantum interfaces are distinguished. The exact identity required here is Proposition prop:drop, with its context restriction. Compare Landmark I def:record and En03-A def:recording, def:nondestructive CheungI,CheungEn03. A record-only uniqueness or compatibility theorem is not an unrestricted residual-instrument theorem.

E5: Local complete-instrument semantics.

The program's first-order instrument depends only on its complete input state and is affine on unnormalized hybrid states. No-cloning and ensemble indistinguishability follow at that semantic level. Landmark I's lem:path, thm:adequacy, and thm:nocloning provide the source comparison CheungI. Its prop:classical-recovery is an additional classical-record reconstruction obstruction, not the statement of affinity itself.

E6: Mixed states and admitted adaptive control.

The instrument extends linearly to mixed inputs and tensorially to untouched references. Finite adaptive and randomized strategies are admitted when their complete classical histories and controls are included in the interface. Arbitrary state-inspecting or remote-history-inspecting schedulers are not covered. Proposition prop:path proves this extension for the explicit finite fragment; compare En04-A and Hawk04-B CheungEn04,CheungHawk04B.

The implementation results additionally require sequential and parallel compositionality, well-typed wiring, and sufficient declared routing capacity. These conditions are not consequences of the spatial cone. Landmark I's circuit adequacy concerns its available gate library; it is not an exact compilation theorem for every arbitrary block instrument.