Procedures: boundaries

What the construct does NOT do: limits, reserved values, neighbouring constructs and the selection rule.

OverviewBoundariesCorpus formsPitfalls

Does not do

• Not mutate state. Procedure state is not mutated: a transition creates an EnteredState event, current_state is computed from history. Anyone waiting for a cell with assignment mistakes the model.
• Not execute law.procedure as part of the minimal semantics. The profile is a companion: fully lowered into events, institutional relations and rules.
• Not read another history’s total. An inter-procedure guard sees another instance’s state before time(e_k) (strict prefix), not the total: “completed” does not become true retroactively.
• Not tell “did not happen” from “was not computed” inside the fold. Hence order refusals (SIMULTANEOUS_EVENTS, CARRIER_REUSED) are loud fatal on the document, not local: the consumer via not_known(valid_transition(...)) must tell the outcomes apart.
• Not execute a guard on an uncomputed conclusion. A rule is not carried down; executing a guard on the uncomputed means answering about the law over an empty relation (fatal instead of an answer).
• Not change the law along history. One document — one edition; programHash is a function of the program, not of history.

Reserved and closed

• A member name is bare, unique within the package (LDC-E1351); a member’s StableId is <P>/<Name>.
• on — only a declared event or action, otherwise LDC-E1344; a non-event constructor in carrier position — LDC-E1347; an event constructor requires id/time and all undeclared fields (LDC-E1343).
• join — all/any/quorum(n)/predicate; quorum(n) outside 1..m, join without regions, a region without initial/terminal — LDC-E1345.
• completed(P) without an instance name — LDC-E1349.
• initial — one per automaton/region; from/to — onto declared states; no transition out of terminal (LDC-E1311–E1313).

Neighbours and the selection rule

• Procedure vs rules: state order — procedure; independent conditions — rules. See the selection table in README.md.
• on E vs no on: domain event vs business step (synthetic <P>Step). The clause narrows, it does not introduce a carrier requirement.
• when vs requires: world facts vs procedure completion.
• entered_state vs current_state vs initial_state: entry by this / end projection / start without a carrier.
• Fold vs norm phase: the fold is one stratum below norm formation; power effects and status atoms are entirely above. The defeasible layer is split by L1 groups, not wholesale.
• Process layer vs core: frames across editions, decision journals — tooling; the core fold is in one edition.
• Procedure state vs norm stage (stage): a state is an instance position in the case automaton (current_state); a stage is a phase of a norm’s life, a neighbouring construct, not a case predicate.