Canonical representatives via complete development

Representative selection for OperEq-classes should be given by the complete-development function cd (iterated as cd_loop_fuel) on the HasNF fragment, not by unconstrained choice of a dummy. Unique normal forms make that choice well-defined. For non-WN terms, nf_of_term falls back to Quotient.exists_rep choice (still OperEq-related).

def ISAR.cd_rep (t : ISKSubtype) : ISKSubtype

One complete-development step, packed as an ISKSubtype.

Equations

• ISAR.cd_rep t = ⟨ISAR.cd t.val, ⋯⟩

theorem ISAR.OperEq_cd_rep (t : ISKSubtype) : OperEq (cd_rep t) t

def ISAR.canonical_nf_fuel (fuel : Nat) (t : ISKSubtype) : ISKSubtype

Fuelled complete development as an explicit choice function on terms.

Equations

• ISAR.canonical_nf_fuel fuel t = ISAR.cd_loop_fuel fuel t

theorem ISAR.canonical_nf_fuel_OperEq (fuel : Nat) (t : ISKSubtype) : OperEq (canonical_nf_fuel fuel t) t

def ISAR.canonical_nf (t : ISKSubtype) (_ht : LinearIKTerm t.val) : ISKSubtype

Linear fragment: enough fuel is term_size, and the result is a normal form.

Equations

• ISAR.canonical_nf t _ht = ISAR.cd_loop_fuel (ISAR.sufficient_fuel t) t

theorem ISAR.canonical_nf_OperEq (t : ISKSubtype) (ht : LinearIKTerm t.val) : OperEq (canonical_nf t ht) t

theorem ISAR.canonical_nf_normal (t : ISKSubtype) (ht : LinearIKTerm t.val) : NormalI (canonical_nf t ht).val

theorem ISAR.IRed_of_OperEq_normal {t n : ISKSubtype} (h : OperEq n t) (hn : NormalI n.val) : IRed t.val n.val

theorem ISAR.IRed_canonical_nf (t : ISKSubtype) (ht : LinearIKTerm t.val) : IRed t.val (canonical_nf t ht).val

theorem ISAR.canonical_nf_unique {t u : ISKSubtype} (ht : LinearIKTerm t.val) (hu : LinearIKTerm u.val) (h : OperEq t u) : (canonical_nf t ht).val = (canonical_nf u hu).val

OperEq-classes share a unique normal form; canonical_nf is that representative.

theorem ISAR.canonical_nf_unique_subtype {t u : ISKSubtype} (ht : LinearIKTerm t.val) (hu : LinearIKTerm u.val) (h : OperEq t u) : canonical_nf t ht = canonical_nf u hu

theorem ISAR.cd_is_OperEq_representative (fuel : Nat) (t : ISKSubtype) : OperEq (cd_loop_fuel fuel t) t

OperEq between a fuelled development and the original term — the representative theorem used by computable kernels (ComputableISAR_Kernel).

theorem ISAR.nf_of_term_OperEq_of_HasNF (t : ISKSubtype) (ht : HasNF t) : OperEq (nf_of_term t) t

Under HasNF, the AC nf_of_term representative is OperEq-related to t.

theorem ISAR.canonical_rep_eq_of_HasNF (t : ISKSubtype) (ht : HasNF t) : OperEq (InvariantLayer.canonical_rep (Quotient.mk operEqSetoid t)) t

theorem ISAR.HasNF_of_LinearIKTerm (t : ISKSubtype) (ht : LinearIKTerm t.val) : HasNF t

Linear terms always have a normal form via canonical_nf.

theorem ISAR.canonical_rep_eq_of_LinearIKTerm (t : ISKSubtype) (ht : LinearIKTerm t.val) : OperEq (InvariantLayer.canonical_rep (Quotient.mk operEqSetoid t)) t

def ISAR.section_fuel (fuel : Nat) (t : ISKSubtype) : ISKSubtype

Fuelled section on concrete terms (fully computable; no quotient out).

Equations

• ISAR.section_fuel fuel t = ISAR.cd_loop_fuel fuel t

theorem ISAR.section_fuel_OperEq (fuel : Nat) (t : ISKSubtype) : OperEq (section_fuel fuel t) t

theorem ISAR.canonical_rep_eq (t : ISKSubtype) : OperEq (InvariantLayer.canonical_rep (Quotient.mk operEqSetoid t)) t

Unrestricted coherence of canonical_rep: always OperEq-related to the class. Proved once nf_of_term uses NF when available and a class representative via Quotient.exists_rep otherwise (never the old false ⟨norm,_⟩ fallback). Preferred explicit section on the linear fragment remains canonical_nf / cd_loop_fuel.

theorem ISAR.canonical_rep_sound (q : InvariantLayer) : Quotient.mk operEqSetoid q.canonical_rep = q

Finite cd as a unique section — and the ¬SN obstruction

HasNF is weak normalization: some IRed sequence hits a unique NF (confluence). SKI is not SN, so term_size is not a fuel bound once sβ can grow. Iterated cd is still a normalizing strategy: a length-indexed strip against complete development shows that any parallel chain to an NF yields a fuel for cd_loop_fuel. For ¬HasNF, no fuel yields NormalI (expected: SKI is not SN); that is not a gap. nf_of_term remains the AC section used by canonical_rep (Classical.choose on HasNF, exists_rep otherwise) and is not claimed computable. The linear fragment additionally gives an explicit bound term_size.

inductive ISAR.ParN : Nat → ITerm → ITerm → Prop

Length-indexed parallel reduction (head form, for induction on the first step).

• zero (t : ITerm) : ParN 0 t t
• succ {k : Nat} {t u v : ITerm} : ParStep t u → ParN k u v → ParN (k + 1) t v

theorem ISAR.ParStep_eq_of_NormalI {n u : ITerm} (hn : NormalI n) (h : ParStep n u) : n = u

theorem ISAR.ParN_trans {k m : Nat} {t u v : ITerm} (h1 : ParN k t u) (h2 : ParN m u v) : ParN (k + m) t v

theorem ISAR.ParN_single {t u : ITerm} (h : ParStep t u) : ParN 1 t u

theorem ISAR.ParN_of_ParTransGen {t n : ITerm} (h : Relation.ReflTransGen ParStep t n) : ∃ (k : Nat), ParN k t n

theorem ISAR.ParN_strip {k : Nat} {t u n : ITerm} (h : ParStep t u) (p : ParN k t n) : ∃ (n' : ITerm), ParN k u n' ∧ ParStep n n'

Diamond strip: one parallel step vs a k-chain, length preserved.

theorem ISAR.cd_loop_fuel_eq_of_cd_eq (fuel : Nat) (t : ISKSubtype) (h : t.val = cd t.val) : cd_loop_fuel fuel t = t

theorem ISAR.cd_loop_fuel_normal_of_ParN (t : ISKSubtype) (n : ITerm) (k : Nat) (p : ParN k t.val n) (hn : NormalI n) : NormalI (cd_loop_fuel k t).val

Gross–Knuth: a parallel chain of length k to an NF is fuel for cd_loop_fuel.

theorem ISAR.unique_normal_form_of_HasNF (t : ISKSubtype) (ht : HasNF t) : ∃ (n : ISKSubtype), (IRed t.val n.val ∧ NormalI n.val) ∧ ∀ (m : ISKSubtype), IRed t.val m.val ∧ NormalI m.val → m = n

HasNF classes have a unique normal-form representative.

theorem ISAR.HasNF_of_cd_loop_fuel_normal (t : ISKSubtype) {fuel : Nat} (hn : NormalI (cd_loop_fuel fuel t).val) : HasNF t

Any fuel that lands on a normal form is a HasNF witness.

theorem ISAR.cd_loop_fuel_not_normal_of_not_HasNF (t : ISKSubtype) (ht : ¬HasNF t) (fuel : Nat) : ¬NormalI (cd_loop_fuel fuel t).val

Obstruction: if there is no NF, finite complete development never produces one.

theorem ISAR.not_HasNF_no_finite_cd_NF (t : ISKSubtype) (ht : ¬HasNF t) (fuel : Nat) : ¬NormalI (cd_loop_fuel fuel t).val

theorem ISAR.finite_cd_reaches_NF_iff (t : ISKSubtype) : HasNF t ↔ ∃ (k : Nat), NormalI (cd_loop_fuel k t).val

Weak normalization iff some finite iterate of cd is a normal form.

theorem ISAR.HasNF_cd_loop_fuel (t : ISKSubtype) (ht : HasNF t) : ∃ (k : Nat), NormalI (cd_loop_fuel k t).val

theorem ISAR.finite_cd_reaches_NF_iff_of_Linear (t : ISKSubtype) (_ht : LinearIKTerm t.val) : HasNF t ↔ ∃ (k : Nat), NormalI (cd_loop_fuel k t).val

Linear fragment: same iff, with explicit fuel term_size.

theorem ISAR.sufficient_fuel_reaches_NF_of_Linear (t : ISKSubtype) (ht : LinearIKTerm t.val) : NormalI (cd_loop_fuel (sufficient_fuel t) t).val

theorem ISAR.canonical_nf_unique_section (t : ISKSubtype) (ht : LinearIKTerm t.val) (n : ISKSubtype) (hn : IRed t.val n.val ∧ NormalI n.val) : n.val = (canonical_nf t ht).val

On the linear fragment the fuelled section is the unique NF.

theorem ISAR.cd_loop_fuel_unique_section_of_HasNF (t : ISKSubtype) (ht : HasNF t) (n : ISKSubtype) (hn : IRed t.val n.val ∧ NormalI n.val) : ∃ (k : Nat), (cd_loop_fuel k t).val = n.val

Under HasNF, some fuel of cd is the unique NF (not merely some NF).

def ISAR.nf_of_HasNF_fuel (t : ISKSubtype) (k : Nat) (_hk : NormalI (cd_loop_fuel k t).val) : ISKSubtype

Explicit Gross–Knuth section: the fuel is a parameter, not a chosen NF.

Equations

• ISAR.nf_of_HasNF_fuel t k _hk = ISAR.cd_loop_fuel k t

theorem ISAR.nf_of_HasNF_fuel_normal (t : ISKSubtype) (k : Nat) (hk : NormalI (cd_loop_fuel k t).val) : NormalI (nf_of_HasNF_fuel t k hk).val

theorem ISAR.nf_of_HasNF_fuel_OperEq (t : ISKSubtype) (k : Nat) (hk : NormalI (cd_loop_fuel k t).val) : OperEq (nf_of_HasNF_fuel t k hk) t

noncomputable def ISAR.nf_of_HasNF (t : ISKSubtype) (ht : HasNF t) : ISKSubtype

Computational HasNF section: choice picks fuel, then the representative is cd_loop_fuel. Still not a computable nf_of_term; that AC section is what canonical_rep uses. ¬HasNF remains exists_rep there (expected, not a gap).

Equations

• ISAR.nf_of_HasNF t ht = ISAR.cd_loop_fuel (Classical.choose ⋯) t

theorem ISAR.nf_of_HasNF_normal (t : ISKSubtype) (ht : HasNF t) : NormalI (nf_of_HasNF t ht).val

theorem ISAR.nf_of_HasNF_OperEq (t : ISKSubtype) (ht : HasNF t) : OperEq (nf_of_HasNF t ht) t

theorem ISAR.nf_of_HasNF_eq_nf_of_term (t : ISKSubtype) (ht : HasNF t) : (nf_of_HasNF t ht).val = (nf_of_term t).val