structure ISAR.IOB (Carrier : Type) : Type

The Presuppositional IOB Triad on a carrier.

• I : Carrier
• O : Carrier → Carrier → Carrier
• B : Carrier → Carrier

structure ISAR.AdmissibleSARI (Carrier : Type) (O : Carrier → Carrier → Carrier) : Type

An Admissible SARI structure on a carrier, constrained by confluence, fixed-point identities, and pairing closure equations.

• S : Carrier → Prop
• A : Carrier → Carrier → Prop
• R : Carrier → Carrier → Prop
• I : Carrier → Prop
• confluent (c c1 c2 : Carrier) : self.R c c1 → self.R c c2 → ∃ (c3 : Carrier), Relation.ReflTransGen self.R c1 c3 ∧ Relation.ReflTransGen self.R c2 c3
• fixed_point (c : Carrier) : self.I c ↔ ∀ (c' : Carrier), ¬self.R c c'
• pairing_closure (c1 c2 : Carrier) : self.S c1 → self.S c2 → self.S (O c1 c2)

structure ISAR.AdmCarrier : Type 1

The category Adm of Admissible Carriers. An object consists of a carrier, an IOB triad, and a self-composition functor compatibility.

• Carrier : Type
• iob : IOB self.Carrier
• F : self.Carrier → self.Carrier
• is_fixed_point (c : self.Carrier) : self.F c = c

def ISAR.OperationalEq {C : Type} (step : C → C → Prop) (c1 c2 : C) : Prop

Operational equality relation induced by reduction/rewriting.

Equations

• ISAR.OperationalEq step c1 c2 = ∃ (c3 : C), Relation.ReflTransGen step c1 c3 ∧ Relation.ReflTransGen step c2 c3

theorem ISAR.oper_eq_refl {C : Type} (step : C → C → Prop) (c : C) : OperationalEq step c c

theorem ISAR.oper_eq_symm {C : Type} (step : C → C → Prop) {c1 c2 : C} (h : OperationalEq step c1 c2) : OperationalEq step c2 c1

theorem ISAR.oper_eq_trans {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) {c1 c2 c3 : C} (h1 : OperationalEq step c1 c2) (h2 : OperationalEq step c2 c3) : OperationalEq step c1 c3

def ISAR.operSetoid {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) : Setoid C

Setoid structure on a carrier under operational equivalence.

Equations

• ISAR.operSetoid step confluent = { r := ISAR.OperationalEq step, iseqv := ⋯ }

inductive ISAR.Statehood (C : AdmCarrier) : C.Carrier → Prop

Inductive Statehood predicate on an AdmCarrier. States are inductively generated from the identity under the self-application operator O.

• identity {C : AdmCarrier} : Statehood C C.iob.I
• application {C : AdmCarrier} (x y : C.Carrier) : Statehood C x → Statehood C y → Statehood C (C.iob.O x y)

structure ISAR.QuotientCarrier (C : AdmCarrier) (step : C.Carrier → C.Carrier → Prop) (confluent : ∀ (s s1 s2 : C.Carrier), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C.Carrier), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) : Type 1

The induced quotient carrier structure, containing the emergent AdmissibleSARI and next-level IOB structures.

• Carrier : Type
• iob : IOB self.Carrier
• sari : AdmissibleSARI self.Carrier self.iob.O

def ISAR.recurrence_step (C : AdmCarrier) (step : C.Carrier → C.Carrier → Prop) (confluent : ∀ (s s1 s2 : C.Carrier), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C.Carrier), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (O_compat : ∀ (c1 c2 d1 d2 : C.Carrier), OperationalEq step c1 d1 → OperationalEq step c2 d2 → OperationalEq step (C.iob.O c1 c2) (C.iob.O d1 d2)) (B_compat : ∀ (c d : C.Carrier), OperationalEq step c d → OperationalEq step (C.iob.B c) (C.iob.B d)) : QuotientCarrier C step confluent

The Recurrence Step construction: If a carrier C admits an IOB structure and is closed under self-application, its operational quotient constructively yields an SARI-typed operational structure and a new IOB embedding.

Equations

• One or more equations did not get rendered due to their size.

theorem ISAR.step_same_quotient {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) {c1 c2 : C} (h : step c1 c2) : ⟦c1⟧ = ⟦c2⟧

A one-step reduction identifies quotient classes, so R (which requires q1 ≠ q2) is empty.

def ISAR.recurrence_R {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (q1 q2 : Quotient (operSetoid step confluent)) : Prop

Recurrence R: a step between distinct OperEq classes.

Equations

• ISAR.recurrence_R step confluent q1 q2 = ∃ (c1 : C) (c2 : C), q1 = ⟦c1⟧ ∧ q2 = ⟦c2⟧ ∧ step c1 c2 ∧ q1 ≠ q2

def ISAR.recurrence_I {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (q : Quotient (operSetoid step confluent)) : Prop

I is “no outgoing R”.

Equations

• ISAR.recurrence_I step confluent q = ∀ (q' : Quotient (ISAR.operSetoid step confluent)), ¬ISAR.recurrence_R step confluent q q'

theorem ISAR.R_empty {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (q1 q2 : Quotient (operSetoid step confluent)) : ¬recurrence_R step confluent q1 q2

Machine-checked: step_same_quotient plus q1 ≠ q2 makes R uninhabited. Do not change OperationalEq to inhabit R — that would break the quotient.

theorem ISAR.I_true {C : Type} (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (q : Quotient (operSetoid step confluent)) : recurrence_I step confluent q

structure ISAR.AdmissibleKernelextends ISAR.Kernel : Type 1

An Admissible Kernel extends the base Kernel with the Operational SARI Quartet.

• Carrier : Type
• view_of : ISKSubtype → self.Carrier
• view_eq : self.Carrier → self.Carrier → Prop
• is_equiv : Equivalence self.view_eq
• sound (t u : ISKSubtype) : OperEq t u → self.view_eq (self.view_of t) (self.view_of u)
• decode : self.Carrier → ISKSubtype
• decode_view (t : ISKSubtype) : OperEq (self.decode (self.view_of t)) t
• view_eq_decode (c : self.Carrier) : self.view_eq (self.view_of (self.decode c)) c
• decode_eq (c1 c2 : self.Carrier) : self.view_eq c1 c2 → OperEq (self.decode c1) (self.decode c2)
• O : self.Carrier → self.Carrier → self.Carrier
• sari : AdmissibleSARI self.Carrier self.O

def ISAR.decode_to_InvariantLayer {C : Type} (decode : C → ISKSubtype) (step : C → C → Prop) (confluent : ∀ (s s1 s2 : C), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (decode_eq : ∀ (c1 c2 : C), OperationalEq step c1 c2 → OperEq (decode c1) (decode c2)) (q : Quotient (operSetoid step confluent)) : InvariantLayer

Lift a carrier decode into the OperEq quotient. AC-free: uses decode_eq only.

Equations

• ISAR.decode_to_InvariantLayer decode step confluent decode_eq q = Quotient.lift (fun (c : C) => ISAR.toInvariantLayer (decode c)) ⋯ q

noncomputable def ISAR.recurrence_to_Kernel (C : AdmCarrier) (step : C.Carrier → C.Carrier → Prop) (confluent : ∀ (s s1 s2 : C.Carrier), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : C.Carrier), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) (O_compat : ∀ (c1 c2 d1 d2 : C.Carrier), OperationalEq step c1 d1 → OperationalEq step c2 d2 → OperationalEq step (C.iob.O c1 c2) (C.iob.O d1 d2)) (B_compat : ∀ (c d : C.Carrier), OperationalEq step c d → OperationalEq step (C.iob.B c) (C.iob.B d)) (view_of : ISKSubtype → C.Carrier) (decode : C.Carrier → ISKSubtype) (sound : ∀ (t u : ISKSubtype), OperEq t u → OperationalEq step (view_of t) (view_of u)) (decode_view : ∀ (t : ISKSubtype), OperEq (decode (view_of t)) t) (view_eq_decode : ∀ (c : C.Carrier), OperationalEq step (view_of (decode c)) c) (decode_eq : ∀ (c1 c2 : C.Carrier), OperationalEq step c1 c2 → OperEq (decode c1) (decode c2)) : AdmissibleKernel

Universal Mapping Theorem: Constructs a category-theoretic AdmissibleKernel from the recurrence quotient space Q of an AdmCarrier C, given a sound and coherent projection/embedding mapping to ISKSubtype.

Decode no longer uses Quotient.out on the carrier quotient. It lifts decode into InvariantLayer (AC-free), then selects an ISK representative via canonical_rep (NF choice; still noncomputable in general, but given by cd/Classical.choose on the OperEq side — see CanonicalRepresentative.lean for the explicit cd_loop_fuel path).

Equations

• One or more equations did not get rendered due to their size.