M0-spec.md

M0 — Frozen specification

This is the contract the proof commits to. It is deliberately narrower than "the paper's Fig. 4 verbatim"; the deviations are listed and justified below.

The theorem

Let ⟶ be the single-step reduction relation: the compatible (congruence) closure of the eleven rule schemas below, over Term (formations ⟦B⟧, applications e(τ↦e'), dispatches e.τ, the locators Φ/ξ, and the terminator ⊥). Let ⟶∗ be its reflexive-transitive closure.

Confluence (Church–Rosser). For all well-formed e (WF e) and all e₁, e₂: if e ⟶∗ e₁ and e ⟶∗ e₂, then there exists e₃ with e₁ ⟶∗ e₃ and e₂ ⟶∗ e₃.

In Lean: a WF-relativized confluence, WF e → e ⟶∗ e₁ → e ⟶∗ e₂ → ∃ e₃, … (WF is PhiConfluence.WF from WellFormed.lean: a formation's domain is duplicate-free and free of positional αᵢ keys). It is proved by the diamond property of a parallel-reduction relation Par (Takahashi complete development) transported via Relation.church_rosser. The system is non-terminating, so this is not done with Newman's lemma.

Why WF-scoped (and not the unconditional Confluent Step). WF has two clauses, and they carry different weight — worth stating precisely:

• legalKey (no positional αᵢ as a formation key) is necessary for confluence. The counterexample that makes unconditional Confluent Step false once alpha is present is a legalKey violation: a malformed ⟦B₁, αᵢ↦e₁, B₂⟧(αᵢ↦e₂) whose void slot sits at ordinal i lets alpha rename the argument (→ an object) while over fires (→ ⊥), and object vs ⊥ never join (deviation #8). The diamond proof consumes exactly this clause (lookup_alpha_absent_of_wf, the alpha case of par_triangle). Faithful, too: phino's parser bars αᵢ formation keys.
• Nodup (unique keys, Def. Binding 4.8) is a faithfulness clause, not a demonstrated confluence-necessity. No duplicate-key non-joinable fork is known, and the diamond proof binds the Nodup field of WF.form but never uses it (only legalKey). Nodup is carried because it matches the paper's Def. Binding and makes our first-match lookup coincide with phino's matcher (deviation #6) — and because WF.step/WF.par preserve it. So "WF is necessary" is precise for legalKey; for Nodup it is faithfulness, not necessity.

So WF-scoping re-imposes exactly the paper's own grammar restrictions our looser Binding drops. (Note the paper proves no confluence theorem at all; it presupposes confluence when defining ≡ as "normal forms are syntactically identical". We prove it, WF-scoped because our encoding is looser than the grammar.)

phino's duplicate-ρ printer bug — resolved (phino #748). Earlier, phino's printer injected a duplicate void ρ, so ⟦ρ↦⟦⟧⟧ printed as ⟦ρ↦⟦ρ↦∅⟧, ρ↦∅⟧ (two ρ keys) — non-Nodup, contradicting the Def. Binding its own parser enforces. Fixed in phino #748 ("dont inject duplicate void rho in salty printing"); phino now emits the single-ρ form our model already produces (canon ⟦ρ↦⟦⟧⟧ = ⟦ρ↦⟦ρ↦∅⟧⟧). We never reproduced the bug (it would break Nodup and the lookup-vs-matcher agreement), so model and phino now agree here. (As of M4.2b, alpha IS in Step, so WF is now load-bearing: the headline confluence carries WF e and is proved via the WF-relativized diamond ParWF a b := WF a ∧ Par a b. The earlier alpha-free fragment was unconditionally confluent; that unconditional step_confluent was retired when alpha landed.)

Rule ⇄ constructor table

Source of truth: the paper (reduction figure, operators.tex); phino's resources/*.yaml (phino explain --normalize) is the secondary interpretation that renders into it. nf e means "e is in normal form" (no rule matches anywhere in e); |B₁| is the number of bindings before the focus; C(·⊳·) is contextualization (Fig. "Contextualization by induction").

phino rule	Lean Step constructor	Pattern → result	Side condition
dot	Step.dot	⟦B₁,τ↦e₁,B₂⟧.τ → C(e₁⊳⟦…⟧)(ρ↦…)	nf e₁
copy	Step.copy	⟦B₁,τ↦∅,B₂⟧(τ↦e₁) → ⟦B₁,τ↦e₁,B₂⟧	ξFree e₁ ∧ nf e₁ (ξ-free KEPT; scope/contextualize vacuous — dev. #7)
alpha	Step.alpha	⟦B₁,τ₁↦∅,B₂⟧(τ₂↦e) → ⟦B₁,τ₁↦∅,B₂⟧(τ₁↦e)	index τ₂ = domain(B₁) (†)
phi	Step.phi	⟦B⟧.τ → ⟦B⟧.φ.τ	φ∈B ∧ τ∉B
stay	Step.stay	⟦B₁,ρ↦e₁,B₂⟧(ρ↦e₂) → ⟦B₁,ρ↦e₁,B₂⟧	—
over	Step.over	⟦B₁,τ↦e₁,B₂⟧(τ↦e₂) → ⊥	τ≠ρ (attached slot)
stop	Step.stop	⟦B⟧.τ → ⊥	τ∉B ∧ φ∉B ∧ λ∉B
null	Step.null	⟦B₁,τ↦∅,B₂⟧.τ → ⊥	— (void slot)
miss	Step.miss	⟦B⟧(τ↦e) → ⊥	τ∉B ∧ τ not positional αᵢ
dd	Step.dd	⊥.τ → ⊥	—
dc	Step.dc	⊥(τ↦e) → ⊥	—

(†) alpha's index counts the domain (assets excluded) — phino #749. Step.alpha matches voidAtOrdinal bs i = the key of the i-th non-asset binding when that binding is void, so a Δ/λ asset before the void slot does not shift the ordinal. This is the paper's Def. Ordinal / Def. Domain (the domain excludes assets) and phino post-#749 ("count alpha index over domain excluding assets" — alpha.yaml's index = domain condition). Earlier phino (and its generated figure) counted assets raw (|B₁| = length bds), contradicting the paper's own prose and worked example (tab:ordinals: ordinal of x in ⟦L>Fn, x↦…⟧ is 0); #749 fixed phino to match the prose, and Step.alpha matches the fixed semantics. The regenerated Rules.lean now shows index(τ₂) = domain(B₁).

Plus the four congruence constructors Step.congDispatch, Step.congAppFn, Step.congAppArg, Step.congForm — covering every recursive Term position (dispatch subject, application subject, application argument, and a formation binding's value), so reduction may occur anywhere, matching the paper (operators.tex: "rules may be applied in any order"). Step.congForm uses the paper's ⟦B₁,τ↦e,B₂⟧ splitting.

Disjointness (the root rules are mutually exclusive on a given redex, with the noted exceptions):

• dispatch ⟦B⟧.τ is split by dot (τ attached) / null (τ void) / phi (τ absent, φ present) / stop (τ absent, φ,λ absent); ⊥.τ is dd. Terms outside all cases (e.g. Φ.τ, ξ.τ) are stuck — this is a partition of reducible dispatch redexes, not of all terms.
• application ⟦B⟧(τ↦e) is split by stay (τ=ρ attached) / over (τ≠ρ attached) / copy (τ void, args normal) / alpha (positional αᵢ, void at ordinal i) / miss (τ absent, non-α); ⊥(…) is dc. Exception: alpha and copy can both match when the applied attribute is a positional αᵢ whose ordinal slot is void — a genuine (and expected-joinable) critical pair, not a clean partition.

How our model relates to the paper

We match the current paper, whose Fig. 4 is generated from current phino (phino explain --normalize). The items below record (a) where older/published forms differed, (b) scoping choices for the confluence theorem, and (c) standing assumptions — not gaps against the current paper.

1. over requires an attached τ. The current Fig. 4 (generated from phino) and our over both use the disjoint attached-slot form ⟦B₁,τ↦e₁,B₂⟧(τ↦e₂). A naive reading of the membership predicate τ∈b (defined in Def. 4.9, Formation — it holds for void keys too) would license a looser over overlapping copy on a void slot (object vs ⊥, which never join); the published arXiv v9 PDF, built with an older phino, rendered exactly that looser form. We follow the current, disjoint form. (Worth keeping the ∈-based prose from suggesting the loose reading.)
2. dot/copy are nf-guarded. They fire only when the relevant sub-expression is already normal. This forces an inner-first order, makes each rule single-path, and removes the dot↔copy ordering ambiguity. It also makes ⟶ a conditional relation with non-monotone guards — the main proof subtlety.
3. Small-step copy (not big-step). The current paper's copy (generated from phino) is already the small-step nf-guarded form we use. Older/published forms (arXiv v9) had a big-step Rcopy that normalizes its argument to n inside the rule (C(e⊳eς) ⟶∗ n), presupposing uniqueness of normal forms (= confluence). We follow the current small-step form, avoiding the circularity; against the current paper there is nothing to reconcile, and the superseded big-step form is not modelled.
4. λ/Δ atoms are outside the normalization relation ⟶. They have no rule among the eleven (phino's resources/*.yaml has none). Their reduction is the paper's separate Morphing (fig:morphing — Mlambda calls a host atom f by value) and Dataization (fig:dataization) partial functions: stateful, side-effecting, host-dependent — functions, not a term-rewriting relation (so the relevant property there is determinism, not confluence). Confluence of ⟶ therefore neither needs nor includes them; λ/Δ are represented as inert atoms (Binding.lambda/ Binding.delta) that never fire. This is a permanent scope boundary set by the paper's own structure (normalization vs. morphing/dataization are separate sections), not unfinished work.
5. ρ-feedback (landed). dot's ρ-introduction (which makes the system non-terminating) landed in Step/Par at M4.3 with the nf-guard and contextualize (receiver = the dispatched formation, so no scope). copy landed at M4.4 (see #7). alpha landed at M4.2b (positional; now modelled by voidAtOrdinal — the domain ordinal, assets skipped, matching the paper and phino post-#749 — see note †). So all eleven rules are now in Step/Par, and confluence covers them. (Earlier drafts said "M1–M2 use a simplified dot" — there was never a simplified dot; it arrived at M4.3 with full ρ-feedback.)
6. Unique-key well-formedness (Def. 4.8). Formations are assumed to have unique attribute keys; under that invariant our first-match lookup coincides with phino's any-position match. Documented in Attributes.lean; to be carried as a hypothesis / indexed type once formation-rebuilding rules arrive. (This is deviation #6 above; the design rationale is in docs/DESIGN.md §4/§6.)
7. copy's guards are ξFree e₁ ∧ nf e₁ — we KEEP phino's ξ-free (this REVERSES the earlier draft of this note, settled at M4.4 by the author). Step.copy (Step.lean) is the local slot-fill ⟦B₁,τ↦∅,B₂⟧(τ↦e₁) → ⟦B₁,τ↦e₁,B₂⟧ guarded by ξFree e₁ then nf e₁ — no scope, no contextualize. Rationale: phino's printed figure renders copy with nf(e₁) only (its renderer strips the ξ condition), but phino's engine enforces ξ-free; and under ξ-freeness, contextualize(e₁, scope) = e₁ is proved (contextualize_eq_self, Parallel.lean, [propext]), so the figure's scope/contextualize are operationally vacuous and dropping them is exact, not a weakening. Keeping ξ-free also (a) keeps copy a local rule needing no context-dependent scope, (b) puts copy inside the de-risked/fuzzed fragment (the de-risk assumed ξ-freeness), and (c) makes difftest valid (the ξ-dropped copy diverges on ⟦x↦∅⟧(x↦ξ) via scope re-injection). The author is correcting the paper figure + phino to this form, so this is a 1:1 match, not a deviation. The single nf is ξFree-aware in its void-application case (it is not a copy-specific nf — it is the one nf encoding copy's guard, exactly as phino's one isNF does).
8. Formation keys are non-positional attributes only. The paper grammar (syntax.tex) puts positional αᵢ solely in application-argument pairs; a formation binding's key is an Attribute ∈ {φ, ρ, label}. Our Binding accepts any Attr (including Attr.alpha), so a malformed formation with an αᵢ key is representable. Harmless in the ⊥-fragment (no rule builds one; lookup is key-agnostic); to be enforced as a well-formedness side-condition alongside the unique-key invariant when alpha/copy/dot arrive.
9. Every formation carries an implicit parent ρ (modelled, not a deviation). The paper (foundations.tex, Def. Parent) and phino give every formation a parent ρ, void until set — the paper grammar does not mandate it, so it is supplied semantically (phino appends ρ↦∅ where absent, recursively). We model this with canon (Canonical.lean), which injects ρ exactly as phino does; canon_canonical/wf_canon/step_canonical prove it is established, WF-preserving, and closed under reduction. Canonical terms are WF, so the headline governs them — the result is confluence of phino's actual calculus, ρ included (not a ρ-free fragment). difftest confirms the match on real formation results. Full account: DESIGN.md §9.