Kannō-Sōe Mutual Dependence (KSMD) context snapshot Source commit: 62ec30b Built at: 2026-08-31T09:27:11.198Z Repository snapshot of https://github.com/kanno-soe/kanno-soe. Selected modules: Code, Exposition Files: - KannoSoe/Signature/Interpenetration.lean - KannoSoe/Signature/Rules.lean - KannoSoe/Signature/V2.lean - KannoSoe/Meta/Audit.lean - KannoSoe/Meta/Examples.lean - KannoSoe/Meta/InterpenetrationExamples.lean - KannoSoe/Meta/ReachabilityExamples.lean - KannoSoe/Meta.lean - KannoSoe/Signature.lean - Exposition/Preamble.md - Exposition/Theory.md ===== CONTEXT ===== ===== FILE: KannoSoe/Signature/Interpenetration.lean ===== import KannoSoe.Signature.V2 /-! # Interpenetration by elaboration This module adds a fresh designatum to an elaboration system and studies two ways of using it. The declarations below are formal model structure. The words *web*, *closed*, and *open* in documentation are supplied readings of that structure; no declaration attributes understanding, consciousness, or personhood to a designatum. `Elaboration.prime E` uses `none : Option D` as a fresh web-designatum. It lifts every old clause along `some` and gives each lifted old designatum an additional clause whose components are itself and `none`. The construction is additive and remains agnostic about the interdependence bundled in an elaboration target. `Elaboration.primeOpen E` additionally lets `none` elaborate back to every lifted old designatum. The closed and open systems can differ for `Reaches`, as the witness below shows, but not for `Joinable`. `Temporality.liftOption T` separately preserves a supplied `Before` relation between embedded old designata, transports their temporal certificates, and leaves `none` outside that relation. It is an optional temporal overlay on the primed carrier, not temporality derived by priming. -/ universe u v private theorem list_mem_map_of_mem {A : Type u} {B : Type v} {f : A → B} {a : A} {xs : List A} (h : a ∈ xs) : f a ∈ xs.map f := by induction h with | head xs => exact .head _ | tail x _ ih => exact .tail (f x) ih private theorem exists_of_list_mem_map {A : Type u} {B : Type v} {f : A → B} {b : B} {xs : List A} (h : b ∈ xs.map f) : ∃ a, a ∈ xs ∧ f a = b := by induction xs with | nil => cases h | cons x xs ih => cases h with | head => exact ⟨x, .head _, rfl⟩ | tail _ htail => obtain ⟨a, ha, hab⟩ := ih htail exact ⟨a, .tail x ha, hab⟩ /-! ## Mapping components and raw targets -/ namespace Component /-- Direct image of a component along a map of designata. -/ def map {D : Type u} {D' : Type v} (f : D → D') (c : Component D) : Component D' where carrier d' := ∃ d, d ∈ c ∧ f d = d' nonempty := by obtain ⟨d, hd⟩ := c.nonempty exact ⟨f d, d, hd, rfl⟩ @[simp] theorem mem_map_iff {D : Type u} {D' : Type v} (f : D → D') (c : Component D) (d' : D') : d' ∈ c.map f ↔ ∃ d, d ∈ c ∧ f d = d' := Iff.rfl theorem mem_map {D : Type u} {D' : Type v} {f : D → D'} {c : Component D} {d : D} (h : d ∈ c) : f d ∈ c.map f := ⟨d, h, rfl⟩ end Component namespace Interdependence /-- Transport an interdependence along a map of designata. -/ def map {D : Type u} {D' : Type v} (L : Interdependence D) (f : D → D') : Interdependence D' where Interdependent c₁' c₂' := ∃ c₁ c₂, L.Interdependent c₁ c₂ ∧ c₁' = c₁.map f ∧ c₂' = c₂.map f symm := by rintro c₁' c₂' ⟨c₁, c₂, h₁₂, hc₁, hc₂⟩ exact ⟨c₂, c₁, L.symm h₁₂, hc₂, hc₁⟩ theorem Chained.map {D : Type u} {D' : Type v} {L : Interdependence D} {components : List (Component D)} (f : D → D') (h : L.Chained components) : (L.map f).Chained (components.map (Component.map f)) := by induction h with | nil => exact .nil | single c₁ => exact .single (c₁.map f) | cons h₁₂ _ ih => exact .cons ⟨_, _, h₁₂, rfl, rfl⟩ ih end Interdependence namespace RawMutualDependence /-- Map every component of a raw target. The new interdependence is an explicit parameter: component transport cannot, and need not, manufacture an interdependence. -/ def mapComponents {D : Type u} {D' : Type v} (rawM : RawMutualDependence D) (f : D → D') (L : Interdependence D') : RawMutualDependence D' where interdependence := L c₁ := rawM.c₁.map f middle := rawM.middle.map (Component.map f) cₙ := rawM.cₙ.map f @[simp] theorem components_mapComponents {D : Type u} {D' : Type v} (rawM : RawMutualDependence D) (f : D → D') (L : Interdependence D') : (rawM.mapComponents f L).components = rawM.components.map (Component.map f) := by simp [mapComponents, components] end RawMutualDependence namespace MutualDependence /-- Transport a certified mutual dependence along a map of designata. -/ def map {D : Type u} {D' : Type v} (m : MutualDependence D) (f : D → D') : MutualDependence D' where toRaw := m.toRaw.mapComponents f (m.interdependence.map f) holds := by rw [RawMutualDependence.Holds, RawMutualDependence.components_mapComponents] exact m.holds.map f @[simp] theorem c₁_map {D : Type u} {D' : Type v} (m : MutualDependence D) (f : D → D') : (m.map f).c₁ = m.c₁.map f := rfl @[simp] theorem cₙ_map {D : Type u} {D' : Type v} (m : MutualDependence D) (f : D → D') : (m.map f).cₙ = m.cₙ.map f := rfl end MutualDependence namespace Temporal /-- Transport a temporal certificate along a map of designata. -/ def map {D : Type u} {D' : Type v} {x y : D} (h : Temporal D x y) (f : D → D') : Temporal D' (f x) (f y) := by obtain ⟨m, hx, hy⟩ := h exact .ofMutualDependence (m.map f) (Component.mem_map hx) (Component.mem_map hy) end Temporal /-! ## Additive extension and monotonicity -/ namespace Elaboration /-- Pointwise inclusion of elaboration clauses on a fixed domain. -/ def Extends {D : Type u} (E E' : Elaboration D) : Prop := ∀ ⦃d rawM⦄, E.Elab d rawM → E'.Elab d rawM instance {D : Type u} : LE (Elaboration D) := ⟨Extends⟩ /-- Adding elaboration clauses can only add reachability. -/ theorem Reaches.mono {D : Type u} {E E' : Elaboration D} (hExt : E ≤ E') {d e : D} (h : E.Reaches d e) : E'.Reaches d e := by induction h with | refl d => exact .refl d | step hElab hcomponent hmem _ ih => exact .step (hExt hElab) hcomponent hmem ih /-- Adding elaboration clauses can only add joinability. -/ theorem Joinable.mono {D : Type u} {E E' : Elaboration D} (hExt : E ≤ E') {a b : D} (h : E.Joinable a b) : E'.Joinable a b := by obtain ⟨w, ha, hb⟩ := h exact ⟨w, ha.mono hExt, hb.mono hExt⟩ /-! ## Priming and saturation -/ /-- Adjoin `none` as a fresh designatum, lift all old clauses along `some`, and add for every old `d` a clause with components `{some d}` and `{none}`. The lifted worldly bodies and bracket body are intentionally simultaneous alternatives for one source: their plurality is the content, not slack. Only `components` is constrained. In particular, the definition neither fixes the target's bundled interdependence nor asserts that the target holds. -/ def prime {D : Type u} (E : Elaboration D) : Elaboration (Option D) where Elab od rawM := match od with | none => False | some d => (∃ oldM, E.Elab d oldM ∧ rawM.components = oldM.components.map (Component.map Option.some)) ∨ rawM.components = [Component.singleton (some d), Component.singleton none] /-- Old reachability is preserved by the embedding into a primed system. -/ theorem Reaches.prime {D : Type u} {E : Elaboration D} {d e : D} (h : E.Reaches d e) : (Elaboration.prime E).Reaches (some d) (some e) := by induction h with | refl d => exact .refl (some d) | @step d e f rawM a hElab hcomponent hmem _ ih => let mapped := rawM.mapComponents Option.some (Interdependence.ofElaboration (Elaboration.prime E)) exact Reaches.step (rawM := mapped) (a := a.map Option.some) (Or.inl ⟨rawM, hElab, by simp [mapped]⟩) (by rw [RawMutualDependence.components_mapComponents] exact list_mem_map_of_mem hcomponent) (Component.mem_map hmem) ih /-- Every designatum in a primed system reaches the fresh designatum. -/ theorem prime_reaches_web {D : Type u} (E : Elaboration D) (d : Option D) : (prime E).Reaches d none := by cases d with | none => exact .refl none | some d => let rawM := RawMutualDependence.pair (Interdependence.ofElaboration (prime E)) (Component.singleton (some d)) (Component.singleton none) exact Reaches.single (rawM := rawM) (a := Component.singleton none) (Or.inr (by simp [rawM])) (by simp [rawM]) (by simp) /-- `Joinable` is total after one priming. -/ theorem prime_joinable_total {D : Type u} (E : Elaboration D) (a b : Option D) : (prime E).Joinable a b := ⟨none, prime_reaches_web E a, prime_reaches_web E b⟩ /-- Total joinability makes `Joinable` transitive in the primed tier. -/ theorem prime_joinable_transitive {D : Type u} (E : Elaboration D) : ∀ ⦃a b c : Option D⦄, (prime E).Joinable a b → (prime E).Joinable b c → (prime E).Joinable a c := by intro a _ c _ _ exact prime_joinable_total E a c /-- Every pair of nonempty components is interdependent in the primed tier. -/ theorem prime_interdependent_total {D : Type u} (E : Elaboration D) (c₁ c₂ : Component (Option D)) : (prime E).Interdependent c₁ c₂ := by obtain ⟨a, ha⟩ := c₁.nonempty obtain ⟨b, hb⟩ := c₂.nonempty exact ⟨fun x _ => ⟨b, hb, prime_joinable_total E x b⟩, fun y _ => ⟨a, ha, prime_joinable_total E a y⟩⟩ private theorem chained_of_total {D : Type u} {L : Interdependence D} (h : ∀ c₁ c₂, L.Interdependent c₁ c₂) : ∀ cs : List (Component D), L.Chained cs | [] => .nil | [c] => .single c | c₁ :: c₂ :: rest => .cons (h c₁ c₂) (chained_of_total h (c₂ :: rest)) /-- After re-tagging by the primed interdependence, every raw dependence holds. This is a statement about saturation of the primed formal tier, not about the status of an unprimed act-time elaboration. -/ theorem prime_certification_trivial {D : Type u} (E : Elaboration D) (rawM : RawMutualDependence (Option D)) : (prime E).certify rawM |>.Holds := by apply chained_of_total intro c₁ c₂ exact prime_interdependent_total E c₁ c₂ /-- There is an elaboration with a genuinely non-joinable old pair whose images are joinable after priming. Thus the saturated tier cannot replace the diagnostic base tier without losing information. -/ theorem exists_tier_noncollapse : ∃ (D : Type) (E : Elaboration D) (a b : D), ¬ E.Joinable a b ∧ (prime E).Joinable (some a) (some b) := by obtain ⟨D, E, a, _, c, _, _, _, _, _, hnac⟩ := Joinable.exists_nontransitive_mutualDependence exact ⟨D, E, a, c, hnac, prime_joinable_total E (some a) (some c)⟩ /-! ## Closed and open brackets -/ private theorem prime_reaches_some_aux {D : Type u} {E : Elaboration D} {start target : Option D} (h : (prime E).Reaches start target) : ∀ {b : D}, target = some b → ∃ a, start = some a ∧ E.Reaches a b := by induction h with | refl d => intro b hd exact ⟨b, hd, .refl b⟩ | @step d e f rawM c hElab hcomponent hmem _ ih => intro b hf obtain ⟨e₀, he, hreach⟩ := ih hf subst e cases d with | none => simp [prime] at hElab | some d => rcases hElab with ⟨oldM, hOld, hcomponents⟩ | hcomponents · rw [hcomponents] at hcomponent obtain ⟨oldC, holdC, hc⟩ := exists_of_list_mem_map hcomponent subst c obtain ⟨e', he', heq⟩ := hmem simp only [Option.some.injEq] at heq subst e' exact ⟨d, rfl, Reaches.step hOld holdC he' hreach⟩ · rw [hcomponents] at hcomponent simp only [List.mem_cons, List.not_mem_nil, or_false] at hcomponent rcases hcomponent with rfl | rfl · simp only [Component.mem_singleton_iff, Option.some.injEq] at hmem subst e₀ exact ⟨d, rfl, hreach⟩ · simp at hmem /-- A path ending at an old image in the closed prime starts at an old image. -/ theorem prime_reaches_some {D : Type u} {E : Elaboration D} {start : Option D} {b : D} (h : (prime E).Reaches start (some b)) : ∃ a, start = some a ∧ E.Reaches a b := prime_reaches_some_aux h rfl /-- The closed prime adds the web as a reachable endpoint but adds no old-to-old reachability. -/ theorem prime_reaches_some_iff {D : Type u} (E : Elaboration D) (a b : D) : (prime E).Reaches (some a) (some b) ↔ E.Reaches a b := by constructor · intro h obtain ⟨a', ha', hab⟩ := prime_reaches_some h have haa : a = a' := Option.some.inj ha' exact haa ▸ hab · intro h exact Reaches.prime h /-- Open the bracket by adding, for each old `d`, a clause from `none` back to `some d`. The web intentionally has one two-component body per old designatum; this plurality is the hub encoding. As with `prime`, only component lists are constrained. -/ def primeOpen {D : Type u} (E : Elaboration D) : Elaboration (Option D) where Elab d rawM := (prime E).Elab d rawM ∨ (d = none ∧ ∃ old : D, rawM.components = [Component.singleton none, Component.singleton (some old)]) theorem prime_le_primeOpen {D : Type u} (E : Elaboration D) : prime E ≤ primeOpen E := by intro d rawM h exact Or.inl h /-- In the open prime, the web reaches every designatum. -/ theorem primeOpen_reaches_from_web {D : Type u} (E : Elaboration D) (d : Option D) : (primeOpen E).Reaches none d := by cases d with | none => exact .refl none | some d => let rawM := RawMutualDependence.pair (Interdependence.ofElaboration (primeOpen E)) (Component.singleton none) (Component.singleton (some d)) exact Reaches.single (rawM := rawM) (a := Component.singleton (some d)) (Or.inr ⟨rfl, d, by simp [rawM]⟩) (by simp [rawM]) (by simp) theorem primeOpen_reaches_total {D : Type u} (E : Elaboration D) (a b : Option D) : (primeOpen E).Reaches a b := (prime_reaches_web E a).mono (prime_le_primeOpen E) |>.trans (primeOpen_reaches_from_web E b) theorem primeOpen_joinable_total {D : Type u} (E : Elaboration D) (a b : Option D) : (primeOpen E).Joinable a b := (primeOpen_reaches_total E a b).joinable /-- Opening or closing the bracket is invisible to `Joinable`. -/ theorem primeOpen_joinable_iff_prime {D : Type u} (E : Elaboration D) (a b : Option D) : (primeOpen E).Joinable a b ↔ (prime E).Joinable a b := ⟨fun _ => prime_joinable_total E a b, fun h => h.mono (prime_le_primeOpen E)⟩ /-- `Reaches` does distinguish an open bracket from a closed one: a pair exists whose old reachability is absent, hence whose closed-prime reachability is absent, while open-prime reachability is present. -/ theorem exists_prime_open_reaches_distinction : ∃ (D : Type) (E : Elaboration D) (a b : D), ¬ (prime E).Reaches (some a) (some b) ∧ (primeOpen E).Reaches (some a) (some b) := by obtain ⟨D, E, a, _, c, _, _, _, _, _, hnac⟩ := Joinable.exists_nontransitive_mutualDependence refine ⟨D, E, a, c, ?_, primeOpen_reaches_total E (some a) (some c)⟩ rw [prime_reaches_some_iff] exact fun h => hnac h.joinable /-! ## One-prime exhaustion -/ /-- After one closed priming, a second closed priming adds no `Reaches` content between first-tier designata. It adds a further name and hub, but no path between the points embedded by the second `some`. -/ theorem prime_reaches_exhausted_on_image {D : Type u} (E : Elaboration D) (a b : Option D) : (prime (prime E)).Reaches (some a) (some b) ↔ (prime E).Reaches a b := prime_reaches_some_iff (prime E) a b /-- The analogous image statement for `Joinable` is only a corollary-level fact: both sides are already total after their first respective priming. -/ theorem prime_joinable_exhausted_on_image {D : Type u} (E : Elaboration D) (a b : Option D) : (prime (prime E)).Joinable (some a) (some b) ↔ (prime E).Joinable a b := ⟨fun _ => prime_joinable_total E a b, fun _ => prime_joinable_total (prime E) (some a) (some b)⟩ end Elaboration /-! ## Conservative temporality on a primed carrier -/ namespace Temporality /-- Preserve a base `Before` relation between `some` images while leaving the fresh `none` designatum temporally isolated. This is an optional overlay for the carrier used by priming; `Elaboration.prime` itself supplies no temporality. -/ def liftOption {D : Type u} (T : Temporality D) : Temporality (Option D) where Before | some x, some y => T.Before x y | _, _ => False trans := by intro x y z hxy hyz cases x with | none => exact False.elim hxy | some x => cases y with | none => exact False.elim hxy | some y => cases z with | none => exact False.elim hyz | some z => exact T.trans hxy hyz irrefl := by intro x cases x with | none => exact fun h => h | some x => exact T.irrefl x certify := by intro x y h cases x with | none => exact False.elim h | some x => cases y with | none => exact False.elim h | some y => exact (T.certify h).map Option.some /-- The lifted `Before` relation agrees with the base relation on old images. -/ @[simp] theorem liftOption_before_some_some_iff {D : Type u} (T : Temporality D) {x y : D} : (liftOption T).Before (some x) (some y) ↔ T.Before x y := Iff.rfl @[simp] theorem liftOption_not_before_none {D : Type u} (T : Temporality D) (x : Option D) : ¬ (liftOption T).Before x none := by cases x <;> exact fun h => h @[simp] theorem liftOption_not_none_before {D : Type u} (T : Temporality D) (y : Option D) : ¬ (liftOption T).Before none y := by cases y <;> exact fun h => h end Temporality ===== FILE: KannoSoe/Signature/Rules.lean ===== import KannoSoe.Signature.V2 /-! # Finite elaboration rules and verified decision procedures `ElabRule` is a finite presentation of an elaboration clause. The decision procedures below compute the reach closure through every component, using structural fuel, and are connected back to the relational signature by iff theorems. They use ordinary `decide`; no native-code evaluator participates in the proofs. -/ universe u /-- A finite elaboration clause with at least two nonempty components. -/ structure ElabRule (D : Type u) where source : D components : List (List D) two_le : 2 ≤ components.length := by decide nonempty : ∀ c ∈ components, c ≠ [] := by decide namespace Component /-- Turn a list of nonempty designatum lists into components. -/ def ofDesignataList {D : Type u} (components : List (List D)) (nonempty : ∀ c ∈ components, c ≠ []) : List (Component D) := components.pmap (fun c hc => Component.ofDesignata c hc) nonempty @[simp] theorem ofDesignataList_nil {D : Type u} (nonempty : ∀ c ∈ ([] : List (List D)), c ≠ []) : ofDesignataList [] nonempty = [] := rfl @[simp] theorem ofDesignataList_cons {D : Type u} (c : List D) (components : List (List D)) (nonempty : ∀ c' ∈ c :: components, c' ≠ []) : ofDesignataList (c :: components) nonempty = Component.ofDesignata c (nonempty c (by simp)) :: ofDesignataList components (fun c' hc' => nonempty c' (by simp [hc'])) := by simp [ofDesignataList] end Component namespace ElabRule theorem components_ne_nil {D : Type u} (rule : ElabRule D) : rule.components ≠ [] := by intro h have htwo := rule.two_le simp [h] at htwo def first {D : Type u} (rule : ElabRule D) : List D := rule.components.head rule.components_ne_nil def last {D : Type u} (rule : ElabRule D) : List D := rule.components.getLast rule.components_ne_nil @[simp] theorem first_mem {D : Type u} (rule : ElabRule D) : rule.first ∈ rule.components := by exact List.head_mem rule.components_ne_nil @[simp] theorem last_mem {D : Type u} (rule : ElabRule D) : rule.last ∈ rule.components := by exact List.getLast_mem rule.components_ne_nil theorem first_ne_nil {D : Type u} (rule : ElabRule D) : rule.first ≠ [] := rule.nonempty rule.first rule.first_mem theorem last_ne_nil {D : Type u} (rule : ElabRule D) : rule.last ≠ [] := rule.nonempty rule.last rule.last_mem /-- Component lists strictly between the first and last lists. -/ def middle {D : Type u} (rule : ElabRule D) : List (List D) := rule.components.tail.dropLast theorem middle_nonempty {D : Type u} (rule : ElabRule D) : ∀ c ∈ rule.middle, c ≠ [] := by intro c hc apply rule.nonempty c exact List.mem_of_mem_tail (List.dropLast_subset _ hc) def firstComponent {D : Type u} (rule : ElabRule D) : Component D := Component.ofDesignata rule.first rule.first_ne_nil def lastComponent {D : Type u} (rule : ElabRule D) : Component D := Component.ofDesignata rule.last rule.last_ne_nil def middleComponents {D : Type u} (rule : ElabRule D) : List (Component D) := Component.ofDesignataList rule.middle rule.middle_nonempty /-- The canonical raw body represented by a rule for a supplied interdependence. -/ def toRaw {D : Type u} (rule : ElabRule D) (L : Interdependence D) : RawMutualDependence D where interdependence := L c₁ := rule.firstComponent middle := rule.middleComponents cₙ := rule.lastComponent @[simp] theorem c₁_toRaw {D : Type u} (rule : ElabRule D) (L : Interdependence D) : (rule.toRaw L).c₁ = rule.firstComponent := rfl @[simp] theorem cₙ_toRaw {D : Type u} (rule : ElabRule D) (L : Interdependence D) : (rule.toRaw L).cₙ = rule.lastComponent := rfl @[simp] theorem components_toRaw {D : Type u} (rule : ElabRule D) (L : Interdependence D) : (rule.toRaw L).components = rule.firstComponent :: rule.middleComponents ++ [rule.lastComponent] := rfl /-- The rule's component lists decomposed into first, middle, and last. -/ def displayedComponents {D : Type u} (rule : ElabRule D) : List (List D) := rule.first :: rule.middle ++ [rule.last] theorem tail_ne_nil {D : Type u} (rule : ElabRule D) : rule.components.tail ≠ [] := by cases hcomponents : rule.components with | nil => have htwo := rule.two_le simp [hcomponents] at htwo | cons first rest => cases rest with | nil => have htwo := rule.two_le simp [hcomponents] at htwo | cons second rest => simp /-- The displayed decomposition contains exactly the supplied component lists. -/ theorem displayedComponents_eq_components {D : Type u} (rule : ElabRule D) : rule.displayedComponents = rule.components := by simp only [displayedComponents, first, middle, last] rw [← List.getLast_tail rule.tail_ne_nil, List.cons_append, List.dropLast_concat_getLast rule.tail_ne_nil] exact List.cons_head_tail rule.components_ne_nil /-- Every designatum occurring in any component of a rule. -/ def designata {D : Type u} (rule : ElabRule D) : List D := rule.components.flatten theorem displayedComponents_nonempty {D : Type u} (rule : ElabRule D) : ∀ c ∈ rule.displayedComponents, c ≠ [] := by intro c hc rcases List.mem_cons.mp hc with rfl | hc · exact rule.first_ne_nil · rcases List.mem_append.mp hc with hc | hc · exact rule.middle_nonempty c hc · have hc' : c = rule.last := by simpa using hc subst c exact rule.last_ne_nil theorem components_toRaw_eq_ofDesignataList {D : Type u} (rule : ElabRule D) (L : Interdependence D) : (rule.toRaw L).components = Component.ofDesignataList rule.displayedComponents rule.displayedComponents_nonempty := by simp [displayedComponents, toRaw, RawMutualDependence.components, firstComponent, middleComponents, lastComponent, Component.ofDesignataList] theorem components_toRaw_eq_ofComponents {D : Type u} (rule : ElabRule D) (L : Interdependence D) : (rule.toRaw L).components = Component.ofDesignataList rule.components rule.nonempty := by simpa only [displayedComponents_eq_components] using rule.components_toRaw_eq_ofDesignataList L end ElabRule namespace Elaboration /-- Present an elaboration relation by a finite list of rules. -/ def ofRules {D : Type u} (rules : List (ElabRule D)) : Elaboration D where Elab d rawM := ∃ rule ∈ rules, d = rule.source ∧ rawM.components = (rule.toRaw rawM.interdependence).components namespace Rules variable {D : Type u} [DecidableEq D] /-- Immediate component successors of a designatum in a finite rule system. -/ def succs (rules : List (ElabRule D)) (d : D) : List D := rules.flatMap fun rule => if rule.source = d then rule.designata else [] /-- Every designatum mentioned as a source or component member. -/ def mentionedDesignata (rules : List (ElabRule D)) : List D := (rules.flatMap fun rule => rule.source :: rule.designata).eraseDups /-- Add all immediate successors of the current reached set. -/ def expand (rules : List (ElabRule D)) (reached : List D) : List D := (reached ++ reached.flatMap (succs rules)).eraseDups /-- Structurally fuelled saturation, stopping early at a fixed point. -/ def saturate (rules : List (ElabRule D)) : Nat → List D → List D | 0, reached => reached | fuel + 1, reached => let expanded := expand rules reached if expanded ⊆ reached then reached else saturate rules fuel expanded /-- Designata in the finite universe not yet present in a reached set. -/ def unseen (rules : List (ElabRule D)) (reached : List D) : List D := (mentionedDesignata rules).filter fun d => decide (d ∉ reached) /-- The verified finite reach closure of a seed. -/ def reachSet (rules : List (ElabRule D)) (seed : D) : List D := saturate rules (mentionedDesignata rules).length [seed] theorem mem_succs_iff {rules : List (ElabRule D)} {d x : D} : x ∈ succs rules d ↔ ∃ rule ∈ rules, rule.source = d ∧ x ∈ rule.designata := by simp only [succs, List.mem_flatMap] constructor · rintro ⟨rule, hrule, hx⟩ by_cases hsource : rule.source = d · exact ⟨rule, hrule, hsource, by simpa [hsource] using hx⟩ · simp [hsource] at hx · rintro ⟨rule, hrule, hsource, hx⟩ exact ⟨rule, hrule, by simpa [hsource] using hx⟩ theorem mem_universe_of_mem_designata {rules : List (ElabRule D)} {rule : ElabRule D} (hrule : rule ∈ rules) {x : D} (hx : x ∈ rule.designata) : x ∈ mentionedDesignata rules := by apply List.mem_eraseDups.mpr apply List.mem_flatMap.mpr exact ⟨rule, hrule, List.Mem.tail _ hx⟩ theorem mem_universe_of_mem_succs {rules : List (ElabRule D)} {d x : D} (hx : x ∈ succs rules d) : x ∈ mentionedDesignata rules := by obtain ⟨rule, hrule, _, hxdesignata⟩ := mem_succs_iff.mp hx exact mem_universe_of_mem_designata hrule hxdesignata theorem reaches_of_mem_succs {rules : List (ElabRule D)} {d x : D} (hx : x ∈ succs rules d) : (ofRules rules).Reaches d x := by obtain ⟨rule, hrule, hsource, hxdesignata⟩ := mem_succs_iff.mp hx let rawM := rule.toRaw (Interdependence.ofElaboration (ofRules rules)) have hElab : (ofRules rules).Elab d rawM := by exact ⟨rule, hrule, hsource.symm, rfl⟩ obtain ⟨component, hcomponent, hx⟩ := List.mem_flatten.mp hxdesignata let a := Component.ofDesignata component (rule.nonempty component hcomponent) exact Reaches.single (rawM := rawM) (a := a) hElab (by rw [ElabRule.components_toRaw_eq_ofComponents] exact List.mem_pmap_of_mem hcomponent) (by simpa [a] using hx) theorem mem_succs_of_elab_component {rules : List (ElabRule D)} {d x : D} {rawM : RawMutualDependence D} {a : Component D} (hElab : (ofRules rules).Elab d rawM) (hcomponent : a ∈ rawM.components) (hx : x ∈ a) : x ∈ succs rules d := by obtain ⟨rule, hrule, hsource, hcomponents⟩ := hElab apply mem_succs_iff.mpr refine ⟨rule, hrule, hsource.symm, ?_⟩ have ha : a ∈ Component.ofDesignataList rule.components rule.nonempty := by rw [← ElabRule.components_toRaw_eq_ofComponents, ← hcomponents] exact hcomponent obtain ⟨component, hcomponent', haeq⟩ := List.mem_pmap.mp ha rw [← haeq] at hx exact List.mem_flatten.mpr ⟨component, hcomponent', by simpa using hx⟩ @[simp] theorem mem_expand_iff {rules : List (ElabRule D)} {reached : List D} {x : D} : x ∈ expand rules reached ↔ x ∈ reached ∨ ∃ d ∈ reached, x ∈ succs rules d := by simp [expand] theorem subset_expand (rules : List (ElabRule D)) (reached : List D) : reached ⊆ expand rules reached := by intro x hx exact mem_expand_iff.mpr (Or.inl hx) theorem mem_universe_of_mem_expand_not_mem {rules : List (ElabRule D)} {reached : List D} {x : D} (hx : x ∈ expand rules reached) (hnot : x ∉ reached) : x ∈ mentionedDesignata rules := by rcases mem_expand_iff.mp hx with hx | ⟨d, _, hsucc⟩ · exact (hnot hx).elim · exact mem_universe_of_mem_succs hsucc private theorem exists_mem_not_mem_of_not_subset {xs ys : List D} (h : ¬xs ⊆ ys) : ∃ x, x ∈ xs ∧ x ∉ ys := by induction xs with | nil => simp at h | cons x xs ih => by_cases hx : x ∈ ys · have htail : ¬xs ⊆ ys := by intro hsubset exact h (List.cons_subset.mpr ⟨hx, hsubset⟩) obtain ⟨y, hyxs, hy⟩ := ih htail exact ⟨y, List.Mem.tail x hyxs, hy⟩ · exact ⟨x, List.Mem.head xs, hx⟩ private theorem length_filter_le_of_imp {α : Type u} {l : List α} {p q : α → Bool} (himp : ∀ x, p x = true → q x = true) : (l.filter p).length ≤ (l.filter q).length := by induction l with | nil => simp | cons x xs ih => have ih' := ih cases hp : p x <;> cases hq : q x <;> simp_all <;> omega private theorem length_filter_lt_of_imp_of_exists {α : Type u} {l : List α} {p q : α → Bool} (himp : ∀ x, p x = true → q x = true) (hexists : ∃ x ∈ l, q x = true ∧ p x = false) : (l.filter p).length < (l.filter q).length := by induction l with | nil => simp at hexists | cons x xs ih => have hle := length_filter_le_of_imp (l := xs) himp rcases hexists with ⟨y, hy, hqy, hpy⟩ rcases List.mem_cons.mp hy with hy | hy · subst y cases hp : p x <;> cases hq : q x <;> simp_all <;> omega · have ihExists : ∃ y ∈ xs, q y = true ∧ p y = false := ⟨y, hy, hqy, hpy⟩ have ih' := ih ihExists cases hp : p x <;> cases hq : q x <;> simp_all <;> omega theorem unseen_expand_lt {rules : List (ElabRule D)} {reached : List D} (hnot : ¬expand rules reached ⊆ reached) : (unseen rules (expand rules reached)).length < (unseen rules reached).length := by obtain ⟨x, hxexpanded, hxnot⟩ := exists_mem_not_mem_of_not_subset hnot have hxuniverse := mem_universe_of_mem_expand_not_mem hxexpanded hxnot apply length_filter_lt_of_imp_of_exists · intro y hy simp only [decide_eq_true_eq] at hy ⊢ intro hyreached exact hy (subset_expand rules reached hyreached) · exact ⟨x, hxuniverse, by simp [hxnot, hxexpanded]⟩ theorem expand_subset_of_unseen_eq_zero {rules : List (ElabRule D)} {reached : List D} (hzero : (unseen rules reached).length = 0) : expand rules reached ⊆ reached := by intro x hxexpanded by_cases hx : x ∈ reached · exact hx · have hxuniverse := mem_universe_of_mem_expand_not_mem hxexpanded hx have hxunseen : x ∈ unseen rules reached := by simp [unseen, hxuniverse, hx] have hpos := List.length_pos_of_mem hxunseen omega theorem saturate_stable (rules : List (ElabRule D)) (fuel : Nat) (reached : List D) (hbound : (unseen rules reached).length ≤ fuel) : expand rules (saturate rules fuel reached) ⊆ saturate rules fuel reached := by induction fuel generalizing reached with | zero => simp only [saturate] apply expand_subset_of_unseen_eq_zero omega | succ fuel ih => simp only [saturate] let expanded := expand rules reached by_cases hstable : expanded ⊆ reached · simp [expanded, hstable] · simp [expanded, hstable] apply ih have hprogress := unseen_expand_lt (rules := rules) hstable omega theorem reachSet_stable (rules : List (ElabRule D)) (seed : D) : expand rules (reachSet rules seed) ⊆ reachSet rules seed := by unfold reachSet apply saturate_stable exact List.length_filter_le _ _ theorem expand_reaches {rules : List (ElabRule D)} {seed : D} {reached : List D} (hreach : ∀ x ∈ reached, (ofRules rules).Reaches seed x) : ∀ x ∈ expand rules reached, (ofRules rules).Reaches seed x := by intro x hx rcases mem_expand_iff.mp hx with hx | ⟨d, hd, hsucc⟩ · exact hreach x hx · exact (hreach d hd).trans (reaches_of_mem_succs hsucc) theorem mem_saturate_reaches {rules : List (ElabRule D)} {seed : D} (fuel : Nat) (reached : List D) (hreach : ∀ x ∈ reached, (ofRules rules).Reaches seed x) : ∀ x ∈ saturate rules fuel reached, (ofRules rules).Reaches seed x := by induction fuel generalizing reached with | zero => simpa [saturate] using hreach | succ fuel ih => simp only [saturate] let expanded := expand rules reached by_cases hstable : expanded ⊆ reached · simp [expanded, hstable] exact hreach · simp [expanded, hstable] exact ih expanded (expand_reaches hreach) theorem mem_reachSet_reaches {rules : List (ElabRule D)} {seed x : D} (hx : x ∈ reachSet rules seed) : (ofRules rules).Reaches seed x := by unfold reachSet at hx exact mem_saturate_reaches (rules := rules) (mentionedDesignata rules).length [seed] (by intro y hy have hy' : y = seed := by simpa using hy subst y exact .refl seed) x hx theorem subset_saturate (rules : List (ElabRule D)) (fuel : Nat) (reached : List D) : reached ⊆ saturate rules fuel reached := by induction fuel generalizing reached with | zero => exact List.Subset.refl reached | succ fuel ih => simp only [saturate] let expanded := expand rules reached by_cases hstable : expanded ⊆ reached · simp [expanded, hstable] · simp [expanded, hstable] exact (subset_expand rules reached).trans (ih expanded) theorem seed_mem_reachSet (rules : List (ElabRule D)) (seed : D) : seed ∈ reachSet rules seed := by unfold reachSet exact subset_saturate rules (mentionedDesignata rules).length [seed] (by simp) theorem reachSet_closed {rules : List (ElabRule D)} {seed d x : D} (hd : d ∈ reachSet rules seed) (hx : x ∈ succs rules d) : x ∈ reachSet rules seed := by apply reachSet_stable rules seed exact mem_expand_iff.mpr (Or.inr ⟨d, hd, hx⟩) theorem reaches_mem_of_succ_closed {rules : List (ElabRule D)} {start target : D} (h : (ofRules rules).Reaches start target) {reached : List D} (hstart : start ∈ reached) (hclosed : ∀ {d x}, d ∈ reached → x ∈ succs rules d → x ∈ reached) : target ∈ reached := by induction h with | refl _ => exact hstart | step hElab hcomponent hmem _ ih => apply ih exact hclosed hstart (mem_succs_of_elab_component hElab hcomponent hmem) theorem reaches_mem_reachSet {rules : List (ElabRule D)} {seed x : D} (hx : (ofRules rules).Reaches seed x) : x ∈ reachSet rules seed := by apply reaches_mem_of_succ_closed hx (seed_mem_reachSet rules seed) intro d x hd hsucc exact reachSet_closed hd hsucc /-- The computed closure and relational reachability coincide. -/ @[simp] theorem mem_reachSet_iff {rules : List (ElabRule D)} {seed x : D} : x ∈ reachSet rules seed ↔ (ofRules rules).Reaches seed x := ⟨mem_reachSet_reaches, reaches_mem_reachSet⟩ /-- Boolean nonempty intersection of two computed reach sets. -/ def joinableB (rules : List (ElabRule D)) (a b : D) : Bool := (reachSet rules a).any fun w => decide (w ∈ reachSet rules b) @[simp] theorem joinableB_eq_true_iff {rules : List (ElabRule D)} {a b : D} : joinableB rules a b = true ↔ (ofRules rules).Joinable a b := by simp [joinableB, Elaboration.Joinable] /-- Egli–Milner interdependence on finite designatum lists. -/ def interdependentB (rules : List (ElabRule D)) (c₁ c₂ : List D) : Bool := (c₁.all fun a => c₂.any fun b => joinableB rules a b) && (c₂.all fun b => c₁.any fun a => joinableB rules a b) @[simp] theorem interdependent_ofDesignata_iff {rules : List (ElabRule D)} {c₁ c₂ : List D} {h₁ : c₁ ≠ []} {h₂ : c₂ ≠ []} : interdependentB rules c₁ c₂ = true ↔ (ofRules rules).Interdependent (Component.ofDesignata c₁ h₁) (Component.ofDesignata c₂ h₂) := by simp [interdependentB, Elaboration.Interdependent] @[simp] theorem interdependent_singleton_iff {rules : List (ElabRule D)} {a b : D} : joinableB rules a b = true ↔ (ofRules rules).Interdependent (Component.singleton a) (Component.singleton b) := by rw [joinableB_eq_true_iff] exact Elaboration.interdependent_singleton_iff.symm /-- Pairwise chaining on finite component lists. -/ def chainedB (rules : List (ElabRule D)) : List (List D) → Bool | [] => true | [_] => true | c₁ :: c₂ :: rest => interdependentB rules c₁ c₂ && chainedB rules (c₂ :: rest) omit [DecidableEq D] in private theorem chained_cons_cons_iff {L : Interdependence D} {c₁ c₂ : Component D} {rest : List (Component D)} : L.Chained (c₁ :: c₂ :: rest) ↔ L.Interdependent c₁ c₂ ∧ L.Chained (c₂ :: rest) := by constructor · intro h cases h with | cons h₁₂ htail => exact ⟨h₁₂, htail⟩ · rintro ⟨h₁₂, htail⟩ exact .cons h₁₂ htail @[simp] theorem chained_map_ofDesignata_iff {rules : List (ElabRule D)} (components : List (List D)) (nonempty : ∀ c ∈ components, c ≠ []) : chainedB rules components = true ↔ (Interdependence.ofElaboration (ofRules rules)).Chained (Component.ofDesignataList components nonempty) := by induction components with | nil => constructor · intro _ exact .nil · intro _ rfl | cons c components ih => cases components with | nil => constructor · intro _ exact .single _ · intro _ rfl | cons c₂ rest => rw [chainedB] rw [Bool.and_eq_true] rw [interdependent_ofDesignata_iff] rw [ih (fun c' hc' => nonempty c' (by simp [hc']))] simp only [Component.ofDesignataList_cons] rw [chained_cons_cons_iff] rfl @[simp] theorem chainedB_displayedComponents_iff_holds {rules : List (ElabRule D)} (rule : ElabRule D) : chainedB rules rule.displayedComponents = true ↔ (rule.toRaw (Interdependence.ofElaboration (ofRules rules))).Holds := by change chainedB rules rule.displayedComponents = true ↔ (Interdependence.ofElaboration (ofRules rules)).Chained (rule.toRaw (Interdependence.ofElaboration (ofRules rules))).components rw [rule.components_toRaw_eq_ofDesignataList] exact chained_map_ofDesignata_iff _ _ instance instDecidableJoinableOfRules (rules : List (ElabRule D)) (a b : D) : Decidable ((ofRules rules).Joinable a b) := decidable_of_iff (joinableB rules a b = true) joinableB_eq_true_iff instance instDecidableInterdependentOfRules (rules : List (ElabRule D)) (c₁ c₂ : List D) (h₁ : c₁ ≠ []) (h₂ : c₂ ≠ []) : Decidable ((ofRules rules).Interdependent (Component.ofDesignata c₁ h₁) (Component.ofDesignata c₂ h₂)) := decidable_of_iff (interdependentB rules c₁ c₂ = true) interdependent_ofDesignata_iff instance instDecidableInterdependentSingletonOfRules (rules : List (ElabRule D)) (a b : D) : Decidable ((ofRules rules).Interdependent (Component.singleton a) (Component.singleton b)) := decidable_of_iff (joinableB rules a b = true) interdependent_singleton_iff instance instDecidableChainedOfRules (rules : List (ElabRule D)) (components : List (List D)) (nonempty : ∀ c ∈ components, c ≠ []) : Decidable ((Interdependence.ofElaboration (ofRules rules)).Chained (Component.ofDesignataList components nonempty)) := decidable_of_iff (chainedB rules components = true) (chained_map_ofDesignata_iff components nonempty) instance instDecidableRuleHolds (rules : List (ElabRule D)) (rule : ElabRule D) : Decidable ((rule.toRaw (Interdependence.ofElaboration (ofRules rules))).Holds) := decidable_of_iff (chainedB rules rule.displayedComponents = true) (chainedB_displayedComponents_iff_holds rule) end Rules end Elaboration namespace RulesSmoke inductive Point where | a | b | middle | c deriving DecidableEq, Repr abbrev rules : List (ElabRule Point) := [ { source := .a, components := [[.b], [.middle], [.c]] } ] abbrev elaboration : Elaboration Point := Elaboration.ofRules rules theorem positive : elaboration.Joinable .a .b := by decide theorem middle_component : elaboration.Joinable .a .middle := by decide theorem negative : ¬elaboration.Joinable .b .c := by decide theorem chained : (Interdependence.ofElaboration elaboration).Chained (Component.ofDesignataList [[.a], [.b]] (by decide)) := by decide end RulesSmoke ===== FILE: KannoSoe/Signature/V2.lean ===== import Std /-! # Mutual dependence, resonance, and temporality Raw types describe component structures without asserting that their interdependences hold. Certified types pair those descriptions with proofs, while `Elaboration` targets raw mutual dependences so it can remain agnostic about the validity of its targets. A interdependence derived from an elaboration (`Interdependence.ofElaboration E`) cannot appear inside the targets of `E`'s own definition; see `Elaboration.certify` and `Elaboration.SelfCertified`. Temporality/causality is an additional interpretation a domain may carry, not something mutual dependence or resonance asserts or requires. -/ universe u v /-! ## Components -/ structure Component (D : Type u) where carrier : D → Prop nonempty : ∃ d, carrier d instance {D : Type u} : Membership D (Component D) := ⟨fun a d => a.carrier d⟩ instance {D : Type u} : CoeFun (Component D) (fun _ => D → Prop) := ⟨Component.carrier⟩ namespace Component def ofDesignata {D : Type u} (designata : List D) (nonempty : designata ≠ []) : Component D where carrier := fun d => d ∈ designata nonempty := by cases designata with | nil => exact (nonempty rfl).elim | cons d rest => exact ⟨d, by simp⟩ @[simp] theorem mem_ofDesignata_iff {D : Type u} {designata : List D} {nonempty : designata ≠ []} {d : D} : d ∈ ofDesignata designata nonempty ↔ d ∈ designata := Iff.rfl def singleton {D : Type u} (d : D) : Component D := ofDesignata [d] (by simp) @[simp] theorem mem_singleton_iff {D : Type u} {d x : D} : x ∈ singleton d ↔ x = d := by simp [singleton] def pair {D : Type u} (d₁ d₂ : D) : Component D := ofDesignata [d₁, d₂] (by simp) @[simp] theorem mem_pair_iff {D : Type u} {d₁ d₂ x : D} : x ∈ pair d₁ d₂ ↔ x = d₁ ∨ x = d₂ := by simp [pair] theorem exists_mem {D : Type u} (a : Component D) : ∃ d, d ∈ a := a.nonempty /-- Components are equal when they have exactly the same members. -/ theorem ext {D : Type u} {a b : Component D} (h : ∀ d, d ∈ a ↔ d ∈ b) : a = b := by cases a with | mk carrierA nonemptyA => cases b with | mk carrierB nonemptyB => have hcarrier : carrierA = carrierB := by ext d exact h d cases hcarrier rfl end Component /-! ## Interdependence -/ structure Interdependence (D : Type u) where Interdependent : Component D → Component D → Prop symm : ∀ {c₁ c₂}, Interdependent c₁ c₂ → Interdependent c₂ c₁ namespace Interdependence inductive Chained {D : Type u} (L : Interdependence D) : List (Component D) → Prop where | nil : Chained L [] | single (c₁ : Component D) : Chained L [c₁] | cons {c₁ c₂ : Component D} {rest : List (Component D)} (h₁₂ : L.Interdependent c₁ c₂) (h : Chained L (c₂ :: rest)) : Chained L (c₁ :: c₂ :: rest) theorem Chained.tail {D : Type u} {L : Interdependence D} {c₁ : Component D} {l : List (Component D)} (h : L.Chained (c₁ :: l)) : L.Chained l := by cases h with | single _ => exact Chained.nil | cons _ h => exact h theorem Chained.of_append_right {D : Type u} {L : Interdependence D} : ∀ (l₁ : List (Component D)) {l₂ : List (Component D)}, L.Chained (l₁ ++ l₂) → L.Chained l₂ | [], _, h => h | c₁ :: rest, l₂, h => by rw [List.cons_append] at h exact Chained.of_append_right rest h.tail theorem Chained.of_append_left {D : Type u} {L : Interdependence D} : ∀ (l₁ l₂ : List (Component D)), L.Chained (l₁ ++ l₂) → L.Chained l₁ | [], _, _ => Chained.nil | [c₁], _, _ => Chained.single c₁ | c₁ :: c₂ :: rest, l₂, h => by rw [List.cons_append, List.cons_append] at h cases h with | cons h₁₂ h => refine Chained.cons h₁₂ (Chained.of_append_left (c₂ :: rest) l₂ ?_) rw [List.cons_append] exact h theorem Chained.glue {D : Type u} {L : Interdependence D} : ∀ {l₁ : List (Component D)} {cₙ : Component D} {l₂ : List (Component D)}, L.Chained (l₁ ++ [cₙ]) → L.Chained (cₙ :: l₂) → L.Chained (l₁ ++ cₙ :: l₂) := by intro l₁ cₙ l₂ hleft hright induction l₁ with | nil => exact hright | cons c₁ rest ih => cases rest with | nil => change L.Chained [c₁, cₙ] at hleft cases hleft with | cons h₁ₙ _ => exact .cons h₁ₙ hright | cons c₂ rest => change L.Chained (c₁ :: c₂ :: rest ++ [cₙ]) at hleft cases hleft with | cons h₁₂ htail => exact .cons h₁₂ (ih htail) /-- Catenate two nonempty chains whose exposed endpoints are interdependent. -/ theorem Chained.catenate {D : Type u} {L : Interdependence D} {l₁ l₂ : List (Component D)} {c₁ c₂ : Component D} (h₁ : L.Chained (l₁ ++ [c₁])) (h₂ : L.Chained (c₂ :: l₂)) (h₁₂ : L.Interdependent c₁ c₂) : L.Chained ((l₁ ++ [c₁]) ++ c₂ :: l₂) := by have hthrough : L.Chained ((l₁ ++ [c₁]) ++ [c₂]) := by simpa [List.append_assoc] using (Chained.glue (l₁ := l₁) (cₙ := c₁) (l₂ := [c₂]) h₁ (.cons h₁₂ (.single c₂))) exact Chained.glue (l₁ := l₁ ++ [c₁]) (cₙ := c₂) (l₂ := l₂) hthrough h₂ /-- Reversing a chain preserves it under a symmetric interdependence. -/ theorem Chained.reverse {D : Type u} {L : Interdependence D} {components : List (Component D)} (h : L.Chained components) : L.Chained components.reverse := by induction h with | nil => exact .nil | single c => exact .single c | @cons c₁ c₂ rest h₁₂ htail ih => have htail' : L.Chained (rest.reverse ++ [c₂]) := by simpa using ih simpa [List.reverse_cons, List.append_assoc] using (Chained.glue (l₁ := rest.reverse) (cₙ := c₂) (l₂ := [c₁]) htail' (.cons (L.symm h₁₂) (.single c₁))) end Interdependence /-! ## Raw mutual dependence: data only -/ /-- Components plus their interdependence, as pure data (1:1: each value carries exactly one interdependence). At least two components by construction. This type makes no assertion; `RawMutualDependence.Holds` states it, and `MutualDependence` below bundles the proof. -/ structure RawMutualDependence (D : Type u) where interdependence : Interdependence D c₁ : Component D middle : List (Component D) cₙ : Component D namespace RawMutualDependence def components {D : Type u} (rawM : RawMutualDependence D) : List (Component D) := rawM.c₁ :: rawM.middle ++ [rawM.cₙ] @[simp] theorem c₁_mem_components {D : Type u} (rawM : RawMutualDependence D) : rawM.c₁ ∈ rawM.components := by simp [components] @[simp] theorem cₙ_mem_components {D : Type u} (rawM : RawMutualDependence D) : rawM.cₙ ∈ rawM.components := by simp [components] /-- The assertion: every two adjacent components are accepted by the bundled interdependence. -/ def Holds {D : Type u} (rawM : RawMutualDependence D) : Prop := rawM.interdependence.Chained rawM.components def pair {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) : RawMutualDependence D := ⟨L, c₁, [], c₂⟩ def triple {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ : Component D) : RawMutualDependence D := ⟨L, c₁, [c₂], c₃⟩ def quad {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ c₄ : Component D) : RawMutualDependence D := ⟨L, c₁, [c₂, c₃], c₄⟩ /-- Build raw dependence data from an explicitly nontrivial component list. -/ def ofComponents {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) : List (Component D) → RawMutualDependence D | [] => pair L c₁ c₂ | c₃ :: rest => let rawM := ofComponents L c₂ c₃ rest ⟨L, c₁, c₂ :: rawM.middle, rawM.cₙ⟩ @[simp] theorem interdependence_ofComponents {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) (rest : List (Component D)) : (ofComponents L c₁ c₂ rest).interdependence = L := by cases rest <;> rfl @[simp] theorem c₁_ofComponents {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) (rest : List (Component D)) : (ofComponents L c₁ c₂ rest).c₁ = c₁ := by cases rest <;> rfl @[simp] theorem components_ofComponents {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) (rest : List (Component D)) : (ofComponents L c₁ c₂ rest).components = c₁ :: c₂ :: rest := by induction rest generalizing c₁ c₂ with | nil => rfl | cons c₃ rest ih => change c₁ :: (c₂ :: (ofComponents L c₂ c₃ rest).middle) ++ [(ofComponents L c₂ c₃ rest).cₙ] = c₁ :: c₂ :: c₃ :: rest have tailComponents : (c₂ :: (ofComponents L c₂ c₃ rest).middle) ++ [(ofComponents L c₂ c₃ rest).cₙ] = c₂ :: c₃ :: rest := by calc _ = (ofComponents L c₂ c₃ rest).c₁ :: (ofComponents L c₂ c₃ rest).middle ++ [(ofComponents L c₂ c₃ rest).cₙ] := by exact congrArg (fun c => (c :: (ofComponents L c₂ c₃ rest).middle) ++ [(ofComponents L c₂ c₃ rest).cₙ]) (c₁_ofComponents L c₂ c₃ rest).symm _ = (ofComponents L c₂ c₃ rest).components := rfl _ = c₂ :: c₃ :: rest := ih c₂ c₃ exact congrArg (List.cons c₁) tailComponents @[simp] theorem interdependence_pair {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) : (pair L c₁ c₂).interdependence = L := rfl @[simp] theorem components_pair {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) : (pair L c₁ c₂).components = [c₁, c₂] := rfl @[simp] theorem components_triple {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ : Component D) : (triple L c₁ c₂ c₃).components = [c₁, c₂, c₃] := rfl @[simp] theorem components_quad {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ c₄ : Component D) : (quad L c₁ c₂ c₃ c₄).components = [c₁, c₂, c₃, c₄] := rfl @[simp] theorem holds_pair_iff {D : Type u} {L : Interdependence D} {c₁ c₂ : Component D} : (pair L c₁ c₂).Holds ↔ L.Interdependent c₁ c₂ := by constructor · intro h have h : L.Chained [c₁, c₂] := h cases h with | cons h₁₂ _ => exact h₁₂ · intro h show L.Chained [c₁, c₂] exact .cons h (.single c₂) @[simp] theorem holds_triple_iff {D : Type u} {L : Interdependence D} {c₁ c₂ c₃ : Component D} : (triple L c₁ c₂ c₃).Holds ↔ L.Interdependent c₁ c₂ ∧ L.Interdependent c₂ c₃ := by constructor · intro h have h : L.Chained [c₁, c₂, c₃] := h cases h with | cons h₁₂ h => cases h with | cons h₂₃ _ => exact ⟨h₁₂, h₂₃⟩ · intro h show L.Chained [c₁, c₂, c₃] exact .cons h.1 (.cons h.2 (.single c₃)) @[simp] theorem holds_quad_iff {D : Type u} {L : Interdependence D} {c₁ c₂ c₃ c₄ : Component D} : (quad L c₁ c₂ c₃ c₄).Holds ↔ L.Interdependent c₁ c₂ ∧ L.Interdependent c₂ c₃ ∧ L.Interdependent c₃ c₄ := by constructor · intro h have h : L.Chained [c₁, c₂, c₃, c₄] := h cases h with | cons h₁₂ h => cases h with | cons h₂₃ h => cases h with | cons h₃₄ _ => exact ⟨h₁₂, h₂₃, h₃₄⟩ · intro h show L.Chained [c₁, c₂, c₃, c₄] exact .cons h.1 (.cons h.2.1 (.cons h.2.2 (.single c₄))) /-- Reverse the displayed order while retaining the same symmetric interdependence. -/ def reverse {D : Type u} (rawM : RawMutualDependence D) : RawMutualDependence D where interdependence := rawM.interdependence c₁ := rawM.cₙ middle := rawM.middle.reverse cₙ := rawM.c₁ @[simp] theorem interdependence_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.interdependence = rawM.interdependence := rfl @[simp] theorem c₁_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.c₁ = rawM.cₙ := rfl @[simp] theorem middle_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.middle = rawM.middle.reverse := rfl @[simp] theorem cₙ_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.cₙ = rawM.c₁ := rfl @[simp] theorem components_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.components = rawM.components.reverse := by simp [reverse, components, List.reverse_append] @[simp] theorem reverse_reverse {D : Type u} (rawM : RawMutualDependence D) : rawM.reverse.reverse = rawM := by cases rawM simp [reverse] /-- A certified raw chain remains certified when its display is reversed. -/ theorem Holds.reverse {D : Type u} {rawM : RawMutualDependence D} (h : rawM.Holds) : rawM.reverse.Holds := by change rawM.interdependence.Chained rawM.reverse.components rw [components_reverse] exact Interdependence.Chained.reverse h theorem holds_of_contiguous {D : Type u} {whole sub : RawMutualDependence D} {pre suf : List (Component D)} (hL : sub.interdependence = whole.interdependence) (hdecomp : whole.components = pre ++ sub.components ++ suf) (hw : whole.Holds) : sub.Holds := by have h : whole.interdependence.Chained (pre ++ sub.components ++ suf) := by rw [← hdecomp] exact hw show sub.interdependence.Chained sub.components rw [hL] exact Interdependence.Chained.of_append_right pre (Interdependence.Chained.of_append_left _ suf h) def IsResonance {D : Type u} (rawM : RawMutualDependence D) : Prop := ∃ b₁ b₂ : D, rawM.middle = [Component.singleton b₁, Component.singleton b₂] theorem isResonance_quad {D : Type u} (L : Interdependence D) (c₁ : Component D) (b₁ b₂ : D) (c₄ : Component D) : (quad L c₁ (Component.singleton b₁) (Component.singleton b₂) c₄).IsResonance := ⟨b₁, b₂, rfl⟩ end RawMutualDependence /-! ## Mutual dependence: data plus proof -/ /-- The certified type downstream code should use: a raw mutual dependence together with the proof that it holds under its own interdependence. If most of your interdependence proofs are dischargeable by a tactic, give the `holds` field a default (`holds : toRaw.Holds := by your_tactic`) so construction feels field-free at most sites. -/ structure MutualDependence (D : Type u) where toRaw : RawMutualDependence D holds : toRaw.Holds namespace MutualDependence def interdependence {D : Type u} (m : MutualDependence D) : Interdependence D := m.toRaw.interdependence def c₁ {D : Type u} (m : MutualDependence D) : Component D := m.toRaw.c₁ def middle {D : Type u} (m : MutualDependence D) : List (Component D) := m.toRaw.middle def cₙ {D : Type u} (m : MutualDependence D) : Component D := m.toRaw.cₙ def components {D : Type u} (m : MutualDependence D) : List (Component D) := m.toRaw.components /-- Proof irrelevance: equality of certified dependences reduces to equality of the underlying data. -/ theorem ext {D : Type u} {a b : MutualDependence D} (h : a.toRaw = b.toRaw) : a = b := by cases a cases b cases h rfl def reverse {D : Type u} (m : MutualDependence D) : MutualDependence D := ⟨m.toRaw.reverse, m.holds.reverse⟩ @[simp] theorem toRaw_reverse {D : Type u} (m : MutualDependence D) : m.reverse.toRaw = m.toRaw.reverse := rfl @[simp] theorem interdependence_reverse {D : Type u} (m : MutualDependence D) : m.reverse.interdependence = m.interdependence := rfl @[simp] theorem c₁_reverse {D : Type u} (m : MutualDependence D) : m.reverse.c₁ = m.cₙ := rfl @[simp] theorem middle_reverse {D : Type u} (m : MutualDependence D) : m.reverse.middle = m.middle.reverse := rfl @[simp] theorem cₙ_reverse {D : Type u} (m : MutualDependence D) : m.reverse.cₙ = m.c₁ := rfl @[simp] theorem components_reverse {D : Type u} (m : MutualDependence D) : m.reverse.components = m.components.reverse := RawMutualDependence.components_reverse m.toRaw @[simp] theorem reverse_reverse {D : Type u} (m : MutualDependence D) : m.reverse.reverse = m := ext (RawMutualDependence.reverse_reverse m.toRaw) def pair {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) (h : L.Interdependent c₁ c₂) : MutualDependence D := ⟨RawMutualDependence.pair L c₁ c₂, RawMutualDependence.holds_pair_iff.mpr h⟩ def triple {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ : Component D) (h₁₂ : L.Interdependent c₁ c₂) (h₂₃ : L.Interdependent c₂ c₃) : MutualDependence D := ⟨RawMutualDependence.triple L c₁ c₂ c₃, RawMutualDependence.holds_triple_iff.mpr ⟨h₁₂, h₂₃⟩⟩ def quad {D : Type u} (L : Interdependence D) (c₁ c₂ c₃ c₄ : Component D) (h₁₂ : L.Interdependent c₁ c₂) (h₂₃ : L.Interdependent c₂ c₃) (h₃₄ : L.Interdependent c₃ c₄) : MutualDependence D := ⟨RawMutualDependence.quad L c₁ c₂ c₃ c₄, RawMutualDependence.holds_quad_iff.mpr ⟨h₁₂, h₂₃, h₃₄⟩⟩ /-- Certify an explicitly nontrivial chained list of components. -/ def ofComponents {D : Type u} (L : Interdependence D) (c₁ c₂ : Component D) (rest : List (Component D)) (holds : L.Chained (c₁ :: c₂ :: rest)) : MutualDependence D := by refine ⟨RawMutualDependence.ofComponents L c₁ c₂ rest, ?_⟩ change (RawMutualDependence.ofComponents L c₁ c₂ rest).interdependence.Chained (RawMutualDependence.ofComponents L c₁ c₂ rest).components rw [RawMutualDependence.interdependence_ofComponents, RawMutualDependence.components_ofComponents] exact holds /-- `holds_of_contiguous` as a slicing function: the sub-tuple copies the whole's interdependence, so it comes back certified with no side conditions. -/ def slice {D : Type u} (whole : MutualDependence D) (c₁ : Component D) (middle : List (Component D)) (cₙ : Component D) (pre suf : List (Component D)) (hdecomp : whole.toRaw.components = pre ++ (c₁ :: middle ++ [cₙ]) ++ suf) : MutualDependence D := ⟨⟨whole.toRaw.interdependence, c₁, middle, cₙ⟩, RawMutualDependence.holds_of_contiguous (whole := whole.toRaw) (sub := ⟨whole.toRaw.interdependence, c₁, middle, cₙ⟩) (pre := pre) (suf := suf) rfl hdecomp whole.holds⟩ /-- Concatenate two dependences by identifying an equal shared endpoint. -/ def concatenateSharedEndpoint {D : Type u} (m₁ m₂ : MutualDependence D) (hL : m₁.interdependence = m₂.interdependence) (hShared : m₁.cₙ = m₂.c₁) : MutualDependence D := by refine ⟨⟨m₁.interdependence, m₁.c₁, m₁.middle ++ m₁.cₙ :: m₂.middle, m₂.cₙ⟩, ?_⟩ have h₂ : m₁.interdependence.Chained (m₁.cₙ :: m₂.middle ++ [m₂.cₙ]) := by rw [hL, hShared] exact m₂.holds have h := Interdependence.Chained.glue (l₁ := m₁.c₁ :: m₁.middle) (cₙ := m₁.cₙ) (l₂ := m₂.middle ++ [m₂.cₙ]) m₁.holds h₂ simpa [MutualDependence.interdependence, MutualDependence.c₁, MutualDependence.middle, MutualDependence.cₙ, RawMutualDependence.Holds, RawMutualDependence.components, List.append_assoc] using h /-- Concatenate two dependences while retaining both interdependent endpoints. -/ def concatenateInterdependentEndpoints {D : Type u} (m₁ m₂ : MutualDependence D) (hL : m₁.interdependence = m₂.interdependence) (hInterdependent : m₁.interdependence.Interdependent m₁.cₙ m₂.c₁) : MutualDependence D := by refine ⟨⟨m₁.interdependence, m₁.c₁, m₁.middle ++ [m₁.cₙ, m₂.c₁] ++ m₂.middle, m₂.cₙ⟩, ?_⟩ have h₁₂ : m₁.interdependence.Chained (((m₁.c₁ :: m₁.middle) ++ [m₁.cₙ]) ++ [m₂.c₁]) := by simpa [MutualDependence.interdependence, MutualDependence.c₁, MutualDependence.middle, MutualDependence.cₙ, List.append_assoc] using (Interdependence.Chained.glue (l₁ := m₁.c₁ :: m₁.middle) (cₙ := m₁.cₙ) (l₂ := [m₂.c₁]) m₁.holds (.cons hInterdependent (.single m₂.c₁))) have h₂ : m₁.interdependence.Chained (m₂.c₁ :: m₂.middle ++ [m₂.cₙ]) := by rw [hL] exact m₂.holds have h := Interdependence.Chained.glue (l₁ := (m₁.c₁ :: m₁.middle) ++ [m₁.cₙ]) (cₙ := m₂.c₁) (l₂ := m₂.middle ++ [m₂.cₙ]) h₁₂ h₂ simpa [MutualDependence.interdependence, MutualDependence.c₁, MutualDependence.middle, MutualDependence.cₙ, RawMutualDependence.Holds, RawMutualDependence.components, List.append_assoc] using h @[simp] theorem components_concatenateInterdependentEndpoints {D : Type u} (m₁ m₂ : MutualDependence D) (hL : m₁.interdependence = m₂.interdependence) (hInterdependent : m₁.interdependence.Interdependent m₁.cₙ m₂.c₁) : (concatenateInterdependentEndpoints m₁ m₂ hL hInterdependent).components = m₁.components ++ m₂.components := by simp [concatenateInterdependentEndpoints, MutualDependence.components, MutualDependence.c₁, MutualDependence.middle, MutualDependence.cₙ, RawMutualDependence.components, List.append_assoc] def IsResonance {D : Type u} (m : MutualDependence D) : Prop := m.toRaw.IsResonance end MutualDependence /-! ## Elaboration and joinability -/ /-- An elaboration system. `Elab d rawM` asserts that `rawM` is one of the simultaneously true dependence-explanations of designatum `d`. Alternatives are plural routes through those facts, not exclusive outcomes: selecting one to witness a pair does not resolve, exclude, or collapse the others. A unique-elaboration function would instead reify the unique constitution that this relation deliberately leaves open in every case. `Elaboration` must target `RawMutualDependence`: it constrains the components of its targets and stays agnostic about both the bundled interdependence and whether the tuple holds. Requiring targets to carry `Interdependence.ofElaboration` of this same elaboration — let alone proofs under it — inside the elaboration's own definition is value-level self-reference; see `certify` and `SelfCertified`. -/ structure Elaboration (D : Type u) where Elab : D → RawMutualDependence D → Prop namespace Elaboration inductive Reaches {D : Type u} (E : Elaboration D) : D → D → Prop where | refl (d : D) : Reaches E d d | step {d e f : D} {rawM : RawMutualDependence D} {a : Component D} (hE : E.Elab d rawM) (ha : a ∈ rawM.components) (he : e ∈ a) (h : Reaches E e f) : Reaches E d f theorem Reaches.trans {D : Type u} {E : Elaboration D} {d e f : D} (h₁ : E.Reaches d e) : E.Reaches e f → E.Reaches d f := by induction h₁ with | refl _ => exact id | step hE ha he _ ih => exact fun h₂ => Reaches.step hE ha he (ih h₂) theorem Reaches.single {D : Type u} {E : Elaboration D} {d e : D} {rawM : RawMutualDependence D} {a : Component D} (hE : E.Elab d rawM) (ha : a ∈ rawM.components) (he : e ∈ a) : E.Reaches d e := Reaches.step hE ha he (Reaches.refl e) def Joinable {D : Type u} (E : Elaboration D) (a b : D) : Prop := ∃ w, E.Reaches a w ∧ E.Reaches b w theorem Joinable.refl {D : Type u} (E : Elaboration D) (a : D) : E.Joinable a a := ⟨a, Reaches.refl a, Reaches.refl a⟩ theorem Joinable.symm {D : Type u} {E : Elaboration D} {a b : D} (h : E.Joinable a b) : E.Joinable b a := by obtain ⟨w, ha, hb⟩ := h exact ⟨w, hb, ha⟩ /-- Reachability into one side of joinability transports joinability back. -/ theorem Joinable.of_reaches {D : Type u} {E : Elaboration D} {d y x : D} (hdy : E.Reaches d y) (hyx : E.Joinable y x) : E.Joinable d x := by obtain ⟨w, hyw, hxw⟩ := hyx exact ⟨w, hdy.trans hyw, hxw⟩ theorem Reaches.joinable {D : Type u} {E : Elaboration D} {a b : D} (h : E.Reaches a b) : E.Joinable a b := ⟨b, h, Reaches.refl b⟩ theorem Reaches.joinable_symm {D : Type u} {E : Elaboration D} {a b : D} (h : E.Reaches a b) : E.Joinable b a := h.joinable.symm /-- The Egli–Milner lifting of joinability to components: every designatum on either side has a joinable partner on the other. -/ def Interdependent {D : Type u} (E : Elaboration D) (c₁ c₂ : Component D) : Prop := (∀ a ∈ c₁, ∃ b ∈ c₂, E.Joinable a b) ∧ (∀ b ∈ c₂, ∃ a ∈ c₁, E.Joinable a b) theorem Interdependent.symm {D : Type u} {E : Elaboration D} {c₁ c₂ : Component D} (h : E.Interdependent c₁ c₂) : E.Interdependent c₂ c₁ := by obtain ⟨h₁, h₂⟩ := h refine ⟨fun b hb => ?_, fun a ha => ?_⟩ · obtain ⟨a, ha, hr⟩ := h₂ b hb exact ⟨a, ha, hr.symm⟩ · obtain ⟨b, hb, hr⟩ := h₁ a ha exact ⟨b, hb, hr.symm⟩ @[simp] theorem interdependent_singleton_iff {D : Type u} {E : Elaboration D} {a b : D} : E.Interdependent (Component.singleton a) (Component.singleton b) ↔ E.Joinable a b := by constructor · intro h obtain ⟨b', hb', hr⟩ := h.1 a (by simp) have hb : b' = b := by simpa using hb' subst hb exact hr · intro h refine ⟨fun a' ha' => ?_, fun b' hb' => ?_⟩ · have ha : a' = a := by simpa using ha' subst ha exact ⟨b, by simp, h⟩ · have hb : b' = b := by simpa using hb' subst hb exact ⟨a, by simp, h⟩ end Elaboration namespace Interdependence def ofElaboration {D : Type u} (E : Elaboration D) : Interdependence D where Interdependent := E.Interdependent symm := Elaboration.Interdependent.symm instance {D : Type u} : Coe (Elaboration D) (Interdependence D) := ⟨ofElaboration⟩ end Interdependence namespace Elaboration /-- Re-tag a raw dependence with the interdependence derived from `E` — the sanctioned route around the self-reference restriction. Certifying (i.e. producing a `MutualDependence`) additionally requires proving `Holds` under the derived interdependence, which is genuine work per system. -/ def certify {D : Type u} (E : Elaboration D) (rawM : RawMutualDependence D) : RawMutualDependence D := { rawM with interdependence := Interdependence.ofElaboration E } @[simp] theorem interdependence_certify {D : Type u} (E : Elaboration D) (rawM : RawMutualDependence D) : (E.certify rawM).interdependence = Interdependence.ofElaboration E := rfl @[simp] theorem components_certify {D : Type u} (E : Elaboration D) (rawM : RawMutualDependence D) : (E.certify rawM).components = rawM.components := rfl @[simp] theorem certify_pair {D : Type u} (E : Elaboration D) (L : Interdependence D) (c₁ c₂ : Component D) : E.certify (RawMutualDependence.pair L c₁ c₂) = RawMutualDependence.pair (Interdependence.ofElaboration E) c₁ c₂ := rfl @[simp] theorem certify_triple {D : Type u} (E : Elaboration D) (L : Interdependence D) (c₁ c₂ c₃ : Component D) : E.certify (RawMutualDependence.triple L c₁ c₂ c₃) = RawMutualDependence.triple (Interdependence.ofElaboration E) c₁ c₂ c₃ := rfl @[simp] theorem certify_quad {D : Type u} (E : Elaboration D) (L : Interdependence D) (c₁ c₂ c₃ c₄ : Component D) : E.certify (RawMutualDependence.quad L c₁ c₂ c₃ c₄) = RawMutualDependence.quad (Interdependence.ofElaboration E) c₁ c₂ c₃ c₄ := rfl @[simp] theorem certify_reverse {D : Type u} (E : Elaboration D) (rawM : RawMutualDependence D) : E.certify rawM.reverse = (E.certify rawM).reverse := rfl /-- Well-formedness of a completed system: every emitted raw dependence carries the interdependence derived from the elaboration itself. Provable about a finished `E`; not expressible inside `E`'s own definition. -/ def SelfCertified {D : Type u} (E : Elaboration D) : Prop := ∀ d rawM, E.Elab d rawM → rawM.interdependence = Interdependence.ofElaboration E /-- An elaboration system accepts the reversed display of every target. -/ def ReversalClosed {D : Type u} (E : Elaboration D) : Prop := ∀ d rawM, E.Elab d rawM → E.Elab d rawM.reverse theorem ReversalClosed.elab_reverse_iff {D : Type u} {E : Elaboration D} (hrc : E.ReversalClosed) {d : D} {rawM : RawMutualDependence D} : E.Elab d rawM.reverse ↔ E.Elab d rawM := by constructor · intro h simpa using hrc d rawM.reverse h · exact hrc d rawM /-- Close an elaboration under reversal of the displayed bodies. -/ def reversalClosure {D : Type u} (E : Elaboration D) : Elaboration D where Elab d rawM := E.Elab d rawM ∨ E.Elab d rawM.reverse /-- The closure construction accepts the reverse of every accepted body. -/ theorem reversalClosure_reversalClosed {D : Type u} (E : Elaboration D) : (reversalClosure E).ReversalClosed := by intro d rawM h rcases h with h | h · exact Or.inr (by simpa using h) · exact Or.inl h /-- Reachability cannot observe reversal of displayed bodies. -/ theorem Reaches.reversalClosure_iff {D : Type u} (E : Elaboration D) {d e : D} : (reversalClosure E).Reaches d e ↔ E.Reaches d e := by constructor · intro h induction h with | refl d => exact .refl d | @step d e f rawM a hElab hcomponent hmem _ ih => rcases hElab with hElab | hElab · exact .step hElab hcomponent hmem ih · exact .step (rawM := rawM.reverse) hElab (by simpa using hcomponent) hmem ih · intro h induction h with | refl d => exact .refl d | step hElab hcomponent hmem _ ih => exact .step (Or.inl hElab) hcomponent hmem ih /-- Reversal-closing an elaboration leaves its reach relation unchanged. -/ theorem reaches_reversalClosure {D : Type u} (E : Elaboration D) : (reversalClosure E).Reaches = E.Reaches := by ext d e exact Reaches.reversalClosure_iff E private inductive JoinabilityNotTransitiveCase where | a | b | c | moreA | abWitness | moreB | bcWitness | moreC deriving DecidableEq /-- A certified mutual dependence can exhibit the failure of transitivity of `Joinable`. Here `a` and `b` share `abWitness`, while `b` and `c` share the distinct `bcWitness`; the reachable sets of `a` and `c` are disjoint. Thus the singleton triple `[{a}, {b}, {c}]` genuinely holds under `Interdependence.ofElaboration E`, although its endpoint designata are not joinable. -/ theorem Joinable.exists_nontransitive_mutualDependence : ∃ (D : Type) (E : Elaboration D) (a b c : D) (m : MutualDependence D), m.interdependence = Interdependence.ofElaboration E ∧ m.components = [Component.singleton a, Component.singleton b, Component.singleton c] ∧ E.Joinable a b ∧ E.Joinable b c ∧ ¬ E.Joinable a c := by let E : Elaboration JoinabilityNotTransitiveCase := ⟨fun d rawM => (d = .a ∧ rawM.components = [Component.singleton .moreA, Component.singleton .abWitness]) ∨ (d = .b ∧ rawM.components = [Component.singleton .abWitness, Component.singleton .moreB, Component.singleton .bcWitness]) ∨ (d = .c ∧ rawM.components = [Component.singleton .bcWitness, Component.singleton .moreC])⟩ let mA : RawMutualDependence JoinabilityNotTransitiveCase := .pair E (Component.singleton .moreA) (Component.singleton .abWitness) let mB : RawMutualDependence JoinabilityNotTransitiveCase := .triple E (Component.singleton .abWitness) (Component.singleton .moreB) (Component.singleton .bcWitness) let mC : RawMutualDependence JoinabilityNotTransitiveCase := .pair E (Component.singleton .bcWitness) (Component.singleton .moreC) have hEa : E.Elab .a mA := by simp [E, mA] have hEb : E.Elab .b mB := by simp [E, mB] have hEc : E.Elab .c mC := by simp [E, mC] have haab : E.Reaches .a .abWitness := Reaches.single (rawM := mA) (a := Component.singleton .abWitness) hEa (by simp [mA]) (by simp) have hbab : E.Reaches .b .abWitness := Reaches.single (rawM := mB) (a := Component.singleton .abWitness) hEb (by simp [mB]) (by simp) have hbbc : E.Reaches .b .bcWitness := Reaches.single (rawM := mB) (a := Component.singleton .bcWitness) hEb (by simp [mB]) (by simp) have hcbc : E.Reaches .c .bcWitness := Reaches.single (rawM := mC) (a := Component.singleton .bcWitness) hEc (by simp [mC]) (by simp) have hab : E.Joinable .a .b := ⟨JoinabilityNotTransitiveCase.abWitness, haab, hbab⟩ have hbc' : E.Joinable .b .c := ⟨JoinabilityNotTransitiveCase.bcWitness, hbbc, hcbc⟩ have reachesA {w : JoinabilityNotTransitiveCase} (h : E.Reaches .a w) : w = .a ∨ w = .moreA ∨ w = .abWitness := by cases h with | refl _ => simp | step hE hcomponent he htail => simp [E] at hE simp [hE] at hcomponent rcases hcomponent with rfl | rfl · simp at he cases he cases htail with | refl _ => simp | step hE' _ _ _ => simp [E] at hE' · simp at he cases he cases htail with | refl _ => simp | step hE' _ _ _ => simp [E] at hE' have reachesC {w : JoinabilityNotTransitiveCase} (h : E.Reaches .c w) : w = .c ∨ w = .bcWitness ∨ w = .moreC := by cases h with | refl _ => simp | step hE hcomponent he htail => simp [E] at hE simp [hE] at hcomponent rcases hcomponent with rfl | rfl · simp at he cases he cases htail with | refl _ => simp | step hE' _ _ _ => simp [E] at hE' · simp at he cases he cases htail with | refl _ => simp | step hE' _ _ _ => simp [E] at hE' have hnac : ¬ E.Joinable .a .c := by rintro ⟨w, haw, hcw⟩ rcases reachesA haw with hwa | hwa | hwa <;> rcases reachesC hcw with hwc | hwc | hwc <;> simp_all let m : MutualDependence JoinabilityNotTransitiveCase := MutualDependence.triple E (Component.singleton .a) (Component.singleton .b) (Component.singleton .c) (interdependent_singleton_iff.mpr hab) (interdependent_singleton_iff.mpr hbc') exact ⟨JoinabilityNotTransitiveCase, E, .a, .b, .c, m, rfl, rfl, hab, hbc', hnac⟩ /-- `Joinable` is not transitive, even among the components of a certified mutual dependence carrying the interdependence derived from its elaboration. -/ theorem Joinable.not_transitive : ∃ (D : Type) (E : Elaboration D), ¬ ∀ ⦃a b c⦄, E.Joinable a b → E.Joinable b c → E.Joinable a c := by obtain ⟨D, E, _, _, _, _, _, _, hab, hbc, hnac⟩ := Joinable.exists_nontransitive_mutualDependence refine ⟨D, E, ?_⟩ intro htrans exact hnac (htrans hab hbc) end Elaboration /-! ## Resonance, raw and certified -/ /-- Resonance data whose two middle components are forced to be singletons. b₁ is the being receiving calls; b₂ is the "same" being responding. The being's receiving-stage and responding-stage share interdependence despite the change. -/ structure RawResonance (D : Type u) where interdependence : Interdependence D calls : Component D b₁ : D b₂ : D responses : Component D namespace RawResonance def middle {D : Type u} (rawR : RawResonance D) : List (Component D) := [Component.singleton rawR.b₁, Component.singleton rawR.b₂] def toRawMutualDependence {D : Type u} (rawR : RawResonance D) : RawMutualDependence D := RawMutualDependence.quad rawR.interdependence rawR.calls (Component.singleton rawR.b₁) (Component.singleton rawR.b₂) rawR.responses def components {D : Type u} (rawR : RawResonance D) : List (Component D) := rawR.toRawMutualDependence.components @[simp] theorem interdependence_toRawMutualDependence {D : Type u} (rawR : RawResonance D) : rawR.toRawMutualDependence.interdependence = rawR.interdependence := rfl @[simp] theorem middle_toRawMutualDependence {D : Type u} (rawR : RawResonance D) : rawR.toRawMutualDependence.middle = rawR.middle := rfl @[simp] theorem components_eq {D : Type u} (rawR : RawResonance D) : rawR.components = [rawR.calls, Component.singleton rawR.b₁, Component.singleton rawR.b₂, rawR.responses] := rfl theorem isResonance {D : Type u} (rawR : RawResonance D) : rawR.toRawMutualDependence.IsResonance := ⟨rawR.b₁, rawR.b₂, rfl⟩ def Holds {D : Type u} (rawR : RawResonance D) : Prop := rawR.toRawMutualDependence.Holds @[simp] theorem holds_iff {D : Type u} {rawR : RawResonance D} : rawR.Holds ↔ rawR.interdependence.Interdependent rawR.calls (Component.singleton rawR.b₁) ∧ rawR.interdependence.Interdependent (Component.singleton rawR.b₁) (Component.singleton rawR.b₂) ∧ rawR.interdependence.Interdependent (Component.singleton rawR.b₂) rawR.responses := by change (RawMutualDependence.quad rawR.interdependence rawR.calls (Component.singleton rawR.b₁) (Component.singleton rawR.b₂) rawR.responses).Holds ↔ _ exact RawMutualDependence.holds_quad_iff end RawResonance /-- Completeness at the raw level: every raw mutual dependence satisfying `IsResonance` is represented by some `RawResonance`. -/ theorem RawMutualDependence.IsResonance.exists_rawResonance {D : Type u} {rawM : RawMutualDependence D} (h : rawM.IsResonance) : ∃ rawR : RawResonance D, rawR.toRawMutualDependence = rawM := by cases rawM with | mk interdependence c₁ middle cₙ => obtain ⟨b₁, b₂, hmiddle⟩ := h change middle = [Component.singleton b₁, Component.singleton b₂] at hmiddle subst middle exact ⟨⟨interdependence, c₁, b₁, b₂, cₙ⟩, rfl⟩ /-- The certified counterpart to `RawResonance`, following the same raw/certified boundary as mutual dependence. -/ structure Resonance (D : Type u) where toRawResonance : RawResonance D holds : toRawResonance.Holds namespace Resonance def interdependence {D : Type u} (r : Resonance D) : Interdependence D := r.toRawResonance.interdependence def calls {D : Type u} (r : Resonance D) : Component D := r.toRawResonance.calls def b₁ {D : Type u} (r : Resonance D) : D := r.toRawResonance.b₁ def b₂ {D : Type u} (r : Resonance D) : D := r.toRawResonance.b₂ def responses {D : Type u} (r : Resonance D) : Component D := r.toRawResonance.responses def middleComponents {D : Type u} (r : Resonance D) : List (Component D) := [Component.singleton r.b₁, Component.singleton r.b₂] def toMutualDependence {D : Type u} (r : Resonance D) : MutualDependence D := ⟨r.toRawResonance.toRawMutualDependence, r.holds⟩ instance {D : Type u} : Coe (Resonance D) (MutualDependence D) := ⟨toMutualDependence⟩ theorem isResonance {D : Type u} (r : Resonance D) : r.toMutualDependence.IsResonance := r.toRawResonance.isResonance def mk' {D : Type u} (L : Interdependence D) (calls : Component D) (b₁ b₂ : D) (responses : Component D) (h₁ : L.Interdependent calls (Component.singleton b₁)) (h₂ : L.Interdependent (Component.singleton b₁) (Component.singleton b₂)) (h₃ : L.Interdependent (Component.singleton b₂) responses) : Resonance D := ⟨⟨L, calls, b₁, b₂, responses⟩, RawResonance.holds_iff.mpr ⟨h₁, h₂, h₃⟩⟩ end Resonance /-- Completeness at the certified level: every certified mutual dependence satisfying `IsResonance` comes from a certified `Resonance`; the proof is transported along the raw representation. -/ theorem MutualDependence.IsResonance.exists_resonance {D : Type u} {m : MutualDependence D} (h : m.IsResonance) : ∃ r : Resonance D, r.toMutualDependence = m := by obtain ⟨rawR, hrawR⟩ := RawMutualDependence.IsResonance.exists_rawResonance h exact ⟨⟨rawR, (show rawR.toRawMutualDependence.Holds from hrawR.symm ▸ m.holds)⟩, MutualDependence.ext hrawR⟩ /-! ## Being -/ /-- A certified mutual dependence all of whose components are singletons. -/ structure Being (D : Type u) where toMutualDependence : MutualDependence D singleton_components : ∀ c ∈ toMutualDependence.components, ∃ d : D, c = Component.singleton d namespace Being /-- Regard a certified mutual dependence as a being when every one of its components is a singleton. -/ def ofMutualDependence {D : Type u} (m : MutualDependence D) (singleton_components : ∀ c ∈ m.components, ∃ d : D, c = Component.singleton d) : Being D := ⟨m, singleton_components⟩ instance {D : Type u} : Coe (Being D) (MutualDependence D) := ⟨toMutualDependence⟩ end Being /-! ## Grading -/ structure PreorderBot (Grade : Type v) where le : Grade → Grade → Prop bot : Grade leRefl : ∀ grade, le grade grade leTrans : ∀ {a b c}, le a b → le b c → le a c botLeast : ∀ grade, le bot grade /-- Grade can be thought of as a "dis-resonance". Bot = no dis-resonance. -/ structure GradedResonance (D : Type u) {Grade : Type v} (PB : PreorderBot Grade) extends Resonance D where callsGrade : Grade responsesGrade : Grade namespace GradedResonance def toMutualDependence {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : GradedResonance D PB) : MutualDependence D := r.toResonance.toMutualDependence instance {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} : CoeOut (GradedResonance D PB) (Resonance D) := ⟨GradedResonance.toResonance⟩ theorem isResonance {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : GradedResonance D PB) : r.toMutualDependence.IsResonance := r.toResonance.isResonance def ofResonance {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) (callsGrade responsesGrade : Grade) : GradedResonance D PB where toResonance := r callsGrade := callsGrade responsesGrade := responsesGrade @[simp] theorem callsGrade_ofResonance {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) (callsGrade responsesGrade : Grade) : (ofResonance (PB := PB) r callsGrade responsesGrade).callsGrade = callsGrade := rfl @[simp] theorem responsesGrade_ofResonance {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) (callsGrade responsesGrade : Grade) : (ofResonance (PB := PB) r callsGrade responsesGrade).responsesGrade = responsesGrade := rfl def ungraded {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) : GradedResonance D PB := ofResonance r PB.bot PB.bot @[simp] theorem callsGrade_ungraded {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) : (ungraded (PB := PB) r).callsGrade = PB.bot := rfl @[simp] theorem responsesGrade_ungraded {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : Resonance D) : (ungraded (PB := PB) r).responsesGrade = PB.bot := rfl def IsUngraded {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (r : GradedResonance D PB) : Prop := r.callsGrade = PB.bot ∧ r.responsesGrade = PB.bot def le {D : Type u} {Grade : Type v} {PB : PreorderBot Grade} (a b : GradedResonance D PB) : Prop := PB.le a.callsGrade b.callsGrade ∧ PB.le a.responsesGrade b.responsesGrade end GradedResonance /-! ## Temporality and causality -/ /-- The undirected dependence certificate carried by a temporal claim. It singles out `x` in the first component and `y` in the last; the certified mutual dependence does not itself assert that either designatum is before the other. -/ inductive Temporal (D : Type u) (x y : D) : Prop where | ofMutualDependence (m : MutualDependence D) (mem_c₁ : x ∈ m.c₁) (mem_cₙ : y ∈ m.cₙ) namespace Temporal theorem symm {D : Type u} {x y : D} (h : Temporal D x y) : Temporal D y x := by obtain ⟨m, hx, hy⟩ := h exact .ofMutualDependence m.reverse hy hx end Temporal /-- Temporality is not derived from the MutualDependence or Resonance, instead it's a fact among those - for example, when a thermodynamic gradient is possible, some designata sit at lower entropy than others, and Temporality can specify which. Every `Before` fact carries a temporal dependence certificate. -/ structure Temporality (D : Type u) where Before : D → D → Prop trans : ∀ {x y z : D}, Before x y → Before y z → Before x z irrefl : ∀ x : D, ¬ Before x x certify : ∀ {x y : D}, Before x y → Temporal D x y namespace Temporality theorem asymm {D : Type u} (T : Temporality D) {x y : D} (h : T.Before x y) : ¬ T.Before y x := fun h' => T.irrefl x (T.trans h h') def ofBase {D : Type u} (base : D → D → Prop) (certify : ∀ {x y}, Relation.TransGen base x y → Temporal D x y) (acyclic : ∀ x, ¬ Relation.TransGen base x x) : Temporality D where Before := Relation.TransGen base trans := Relation.TransGen.trans irrefl := acyclic certify := certify theorem rank_lt_of_transGen {D : Type u} {base : D → D → Prop} {rank : D → Nat} (step_lt : ∀ {x y}, base x y → rank x < rank y) {x y : D} (h : Relation.TransGen base x y) : rank x < rank y := by induction h with | single hxy => exact step_lt hxy | tail _ hyz ih => exact Nat.lt_trans ih (step_lt hyz) def ofBaseRank {D : Type u} (base : D → D → Prop) (rank : D → Nat) (step_lt : ∀ {x y}, base x y → rank x < rank y) (certify : ∀ {x y}, Relation.TransGen base x y → Temporal D x y) : Temporality D := ofBase base certify fun x h => Nat.lt_irrefl (rank x) (rank_lt_of_transGen (base := base) (rank := rank) step_lt h) end Temporality structure Causal (D : Type u) extends Temporality D where Causes : D → D → Prop causes_before : ∀ {x y : D}, Causes x y → Before x y namespace Causal /-- Causal claims inherit asymmetry from their strict `Before` overlay. -/ theorem causes_asymm {D : Type u} (C : Causal D) {x y : D} (h : C.Causes x y) : ¬ C.Causes y x := fun h' => C.toTemporality.asymm (C.causes_before h) (C.causes_before h') end Causal ===== FILE: KannoSoe/Meta/Audit.lean ===== import Lean import KannoSoe.Signature.V2 import KannoSoe.Signature.Rules import KannoSoe.Signature.Interpenetration import KannoSoe.Meta.Examples import KannoSoe.Meta.ReachabilityExamples import KannoSoe.Meta.InterpenetrationExamples /-! # Audit: signature and example modules This standalone audit is intentionally not imported by the library. Run it from the repository root with: lake env lean KannoSoe/Meta/Audit.lean For each target module, the audit parses its source to find review-sensitive constructs, then checks every environment declaration attributed to the module, including private and compiler-generated declarations. It reports declared axioms, opaque/unsafe/partial declarations, and every transitive kernel axiom dependency. The exact module-level trust boundaries are: * KannoSoe.Signature.V2: propext and Quot.sound. Quot.sound enters via funext, required by Component.ext (extensionality of Component carriers) and the reversal interface equalities; the generated recursion helper for component-list construction is also expected. * KannoSoe.Signature.Interpenetration: propext. * KannoSoe.Signature.Rules: propext and Quot.sound; the generated structural recursion helpers for saturation and chained checking are expected. * KannoSoe.Meta.Examples: propext and Quot.sound. * KannoSoe.Meta.ReachabilityExamples: propext and Quot.sound. * KannoSoe.Meta.InterpenetrationExamples: propext and Quot.sound. In particular, sorry and admit (which elaborate through sorryAx), declared axioms, and classical choice are rejected. -/ open Lean Elab Command private structure ModuleAuditConfig where moduleName : String sourcePath : System.FilePath allowedAxioms : List String expectedPartials : List String := [] private structure SourceMarker where text : String pos : String.Pos.Raw private def auditStringLt (a b : String) : Bool := a < b private def auditNameLt (a b : Name) : Bool := auditStringLt a.toString b.toString private def auditRenderStrings (items : List String) : String := "[" ++ String.intercalate ", " ((items.toArray.qsort auditStringLt).toList) ++ "]" private def auditRenderNames (names : List Name) : String := auditRenderStrings (names.map Name.toString) private def auditDottedName (value : String) : Name := value.splitOn "." |>.foldl (fun name part => Name.str name part) Name.anonymous private def auditAtomMarker? (value : String) : Option String := if ["sorry", "admit", "axiom", "axioms", "opaque", "unsafe", "partial", "noncomputable", "classical", "extern", "implemented_by"].contains value then some value else none private def auditIdentMarker? (value : Name) : Option String := let value := value.toString if value == "propext" || value == "Quot.sound" || value == "Classical" || value.startsWith "Classical." then some value else none private partial def collectSourceMarkers : Syntax → Array SourceMarker | .missing => #[] | .atom info value => match auditAtomMarker? value, info.getPos? with | some text, some pos => #[{ text, pos }] | _, _ => #[] | .ident info _ value _ => match auditIdentMarker? value, info.getPos? with | some text, some pos => #[{ text, pos }] | _, _ => #[] | .node _ _ args => args.foldl (fun found arg => found ++ collectSourceMarkers arg) #[] private def auditModule (env : Environment) (config : ModuleAuditConfig) : CommandElabM Unit := do let moduleName := auditDottedName config.moduleName let some moduleIdx := env.getModuleIdx? moduleName | throwError "unknown imported module {moduleName}" let source ← IO.FS.readFile config.sourcePath let syntaxTree ← Parser.testParseFile env config.sourcePath let fileMap := FileMap.ofString source let sourceMarkers := collectSourceMarkers syntaxTree let mut declarationCount := 0 let mut directAxioms : Array Name := #[] let mut opaques : Array Name := #[] let mut unsafes : Array Name := #[] let mut partials : Array Name := #[] let mut dependencies : Array (Name × List Name) := #[] let mut seenAxioms : Array String := #[] let mut failures : Array String := #[] for (name, info) in env.constants do if env.getModuleIdxFor? name == some moduleIdx then declarationCount := declarationCount + 1 if info.isAxiom then directAxioms := directAxioms.push name failures := failures.push s!"declared axiom: {name}" if info matches .opaqueInfo _ then opaques := opaques.push name failures := failures.push s!"opaque declaration: {name}" if info.isUnsafe then unsafes := unsafes.push name failures := failures.push s!"unsafe declaration: {name}" if info.isPartial then partials := partials.push name unless config.expectedPartials.contains name.toString do failures := failures.push s!"unexpected partial declaration: {name}" let occurs := (← Lean.collectAxioms name).toList unless occurs.isEmpty do dependencies := dependencies.push (name, occurs) for axiomName in occurs do let axiomName := axiomName.toString unless seenAxioms.contains axiomName do seenAxioms := seenAxioms.push axiomName let unexpected := occurs.filter (fun axiomName => !config.allowedAxioms.contains axiomName.toString) unless unexpected.isEmpty do failures := failures.push ( s!"{name}: unexpected axiom dependencies " ++ auditRenderNames unexpected) for expected in config.expectedPartials do unless partials.any (fun name => name.toString == expected) do failures := failures.push s!"expected partial declaration absent: {expected}" for allowed in config.allowedAxioms do unless seenAxioms.contains allowed do failures := failures.push s!"expected axiom dependency absent: {allowed}" for marker in sourceMarkers do let pos := fileMap.toPosition marker.pos failures := failures.push ( s!"source review marker at " ++ s!"{config.sourcePath}:{pos.line}:{pos.column + 1}: {marker.text}") logInfo m!"source review markers for {moduleName}: {sourceMarkers.size}" for marker in sourceMarkers do let pos := fileMap.toPosition marker.pos logInfo m!" {config.sourcePath}:{pos.line}:{pos.column + 1}: {marker.text}" let summary : String := s!"module {moduleName}: {declarationCount} declarations; " ++ s!"{directAxioms.size} declared axioms; {opaques.size} opaque; " ++ s!"{unsafes.size} unsafe; {partials.size} partial" logInfo summary unless directAxioms.isEmpty do logInfo "declared axioms:" for name in directAxioms.qsort auditNameLt do logInfo m!" {name}" unless opaques.isEmpty do logInfo "opaque declarations:" for name in opaques.qsort auditNameLt do logInfo m!" {name}" unless unsafes.isEmpty do logInfo "unsafe declarations:" for name in unsafes.qsort auditNameLt do logInfo m!" {name}" unless partials.isEmpty do logInfo "partial declarations:" for name in partials.qsort auditNameLt do logInfo m!" {name}" let axiomSummary : String := s!"module axiom set for {moduleName}: " ++ auditRenderStrings seenAxioms.toList logInfo axiomSummary logInfo m!"declarations with axiom dependencies for {moduleName}:" for (name, occurs) in dependencies.qsort (fun a b => auditNameLt a.1 b.1) do logInfo m!" {name}: {auditRenderNames occurs}" unless failures.isEmpty do let details := failures.foldl (fun result failure => result ++ "\n- " ++ failure) "" throwError m!"module audit failed for {moduleName}:{details}" logInfo m!"module audit passed: {moduleName}" elab "#audit_signature_and_examples" : command => do let env ← getEnv let auditPath := System.FilePath.mk (← read).fileName let some auditDir := auditPath.parent | throwError "cannot determine the audit file's parent directory" let some packageDir := auditDir.parent | throwError "cannot determine the KannoSoe source directory" let configs : List ModuleAuditConfig := [ { moduleName := "KannoSoe.Signature.V2" sourcePath := packageDir / "Signature" / "V2.lean" allowedAxioms := ["propext", "Quot.sound"] expectedPartials := ["RawMutualDependence.ofComponents._unsafe_rec"] }, { moduleName := "KannoSoe.Signature.Interpenetration" sourcePath := packageDir / "Signature" / "Interpenetration.lean" allowedAxioms := ["propext"] }, { moduleName := "KannoSoe.Signature.Rules" sourcePath := packageDir / "Signature" / "Rules.lean" allowedAxioms := ["propext", "Quot.sound"] expectedPartials := ["Elaboration.Rules.chainedB._unsafe_rec", "Elaboration.Rules.saturate._unsafe_rec"] }, { moduleName := "KannoSoe.Meta.Examples" sourcePath := auditDir / "Examples.lean" allowedAxioms := ["propext", "Quot.sound"] }, { moduleName := "KannoSoe.Meta.ReachabilityExamples" sourcePath := auditDir / "ReachabilityExamples.lean" allowedAxioms := ["propext", "Quot.sound"] }, { moduleName := "KannoSoe.Meta.InterpenetrationExamples" sourcePath := auditDir / "InterpenetrationExamples.lean" allowedAxioms := ["propext", "Quot.sound"] } ] for config in configs do auditModule env config #audit_signature_and_examples ===== FILE: KannoSoe/Meta/Examples.lean ===== import KannoSoe.Signature.Rules /-! # Signature examples Examples of certified beings, two-sided resonance grades, and temporality. -/ namespace BeingAndGrading inductive Signal where | firstCall | firstBeing | secondBeing | firstResponse | secondCall | thirdBeing | fourthBeing | secondResponse | a | b | c | d deriving DecidableEq, Repr open Signal def universalInterdependence : Interdependence Signal where Interdependent := fun _ _ => True symm := fun _ => trivial def firstResonance : Resonance Signal := Resonance.mk' universalInterdependence (Component.singleton firstCall) firstBeing secondBeing (Component.singleton firstResponse) trivial trivial trivial def secondResonance : Resonance Signal := Resonance.mk' universalInterdependence (Component.singleton secondCall) thirdBeing fourthBeing (Component.singleton secondResponse) trivial trivial trivial def singleBeing : Being Signal := Being.ofMutualDependence (MutualDependence.pair universalInterdependence (Component.singleton a) (Component.singleton b) trivial) (by intro component hc change component ∈ [Component.singleton a, Component.singleton b] at hc simp only [List.mem_cons, List.not_mem_nil, or_false] at hc rcases hc with rfl | rfl <;> exact ⟨_, rfl⟩) theorem consecutiveBeingComponentsInterdependent : universalInterdependence.Interdependent (Component.singleton b) (Component.singleton c) := trivial def multiBeing : Being Signal := Being.ofMutualDependence (MutualDependence.ofComponents universalInterdependence (Component.singleton a) (Component.singleton b) [Component.singleton c, Component.singleton d] (by exact .cons trivial (.cons consecutiveBeingComponentsInterdependent (.cons trivial (.single _))))) (by intro component hc change component ∈ [Component.singleton a, Component.singleton b, Component.singleton c, Component.singleton d] at hc simp only [List.mem_cons, List.not_mem_nil, or_false] at hc rcases hc with rfl | rfl | rfl | rfl <;> exact ⟨_, rfl⟩) def natPreorderBot : PreorderBot Nat where le := (· ≤ ·) bot := 0 leRefl := Nat.le_refl leTrans := Nat.le_trans botLeast := Nat.zero_le def independentlyGraded : GradedResonance Signal natPreorderBot := GradedResonance.ofResonance firstResonance 2 7 example : (GradedResonance.ofResonance (PB := natPreorderBot) firstResonance 2 7).callsGrade = 2 := by simp example : (GradedResonance.ofResonance (PB := natPreorderBot) firstResonance 2 7).responsesGrade = 7 := by simp def ungradedResonance : GradedResonance Signal natPreorderBot := GradedResonance.ungraded firstResonance example : ungradedResonance.callsGrade = natPreorderBot.bot := by simp [ungradedResonance] example : ungradedResonance.responsesGrade = natPreorderBot.bot := by simp [ungradedResonance] example : GradedResonance.IsUngraded ungradedResonance := by simp [GradedResonance.IsUngraded, ungradedResonance] def lowerGrades : GradedResonance Signal natPreorderBot := GradedResonance.ofResonance firstResonance 1 3 example : GradedResonance.le lowerGrades independentlyGraded := by change 1 ≤ 2 ∧ 3 ≤ 7 decide end BeingAndGrading /-! ## Galactic tea drinking -/ namespace GalacticTea inductive GalacticTeaDesignatum where | bigBang | earth | vesper | meDrinkingTea | someoneDrinkingTea | bigBangProducingEarth | moreBigBang | bigBangProducingVesper | moreEarth | meOnEarth | meDrinkingTeaOnEarth | moreVesper | someoneOnVesper | someoneDrinkingTeaOnVesper deriving DecidableEq, Repr open GalacticTeaDesignatum abbrev bigBang : Component GalacticTeaDesignatum := Component.singleton GalacticTeaDesignatum.bigBang abbrev earth : Component GalacticTeaDesignatum := Component.singleton GalacticTeaDesignatum.earth abbrev vesper : Component GalacticTeaDesignatum := Component.singleton GalacticTeaDesignatum.vesper abbrev meDrinkingTea : Component GalacticTeaDesignatum := Component.singleton GalacticTeaDesignatum.meDrinkingTea abbrev someoneDrinkingTea : Component GalacticTeaDesignatum := Component.singleton GalacticTeaDesignatum.someoneDrinkingTea theorem bigBang_designatum_mem : GalacticTeaDesignatum.bigBang ∈ bigBang := by simp [bigBang] theorem meDrinkingTea_designatum_mem : GalacticTeaDesignatum.meDrinkingTea ∈ meDrinkingTea := by simp [meDrinkingTea] theorem someoneDrinkingTea_designatum_mem : GalacticTeaDesignatum.someoneDrinkingTea ∈ someoneDrinkingTea := by simp [someoneDrinkingTea] /-- The galactic-tea clauses as a finite elaboration-rule presentation. -/ abbrev teaElaboration : Elaboration GalacticTeaDesignatum := Elaboration.ofRules [ { source := GalacticTeaDesignatum.bigBang components := [[bigBangProducingVesper], [moreBigBang], [bigBangProducingEarth]] }, { source := GalacticTeaDesignatum.earth components := [[bigBangProducingEarth], [moreEarth], [meOnEarth]] }, { source := GalacticTeaDesignatum.vesper components := [[bigBangProducingVesper], [moreVesper], [someoneOnVesper]] }, { source := GalacticTeaDesignatum.meDrinkingTea components := [[meOnEarth], [meDrinkingTeaOnEarth]] }, { source := GalacticTeaDesignatum.someoneDrinkingTea components := [[someoneOnVesper], [someoneDrinkingTeaOnVesper]] } ] theorem bigBang_vesper_joinable : teaElaboration.Joinable GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.vesper := by decide theorem earth_bigBang_joinable : teaElaboration.Joinable GalacticTeaDesignatum.earth GalacticTeaDesignatum.bigBang := by decide theorem vesper_someoneDrinkingTea_joinable : teaElaboration.Joinable GalacticTeaDesignatum.vesper GalacticTeaDesignatum.someoneDrinkingTea := by decide theorem meDrinkingTea_earth_joinable : teaElaboration.Joinable GalacticTeaDesignatum.meDrinkingTea GalacticTeaDesignatum.earth := by decide theorem bigBang_vesper_interdependent : teaElaboration.Interdependent bigBang vesper := by decide theorem earth_bigBang_interdependent : teaElaboration.Interdependent earth bigBang := by decide theorem vesper_someoneDrinkingTea_interdependent : teaElaboration.Interdependent vesper someoneDrinkingTea := by decide theorem meDrinkingTea_earth_interdependent : teaElaboration.Interdependent meDrinkingTea earth := by decide /-- The displayed component chain certified by the tea example. -/ abbrev galacticTeaChain : ElabRule GalacticTeaDesignatum := { source := GalacticTeaDesignatum.meDrinkingTea components := [[GalacticTeaDesignatum.meDrinkingTea], [GalacticTeaDesignatum.earth], [GalacticTeaDesignatum.bigBang], [GalacticTeaDesignatum.vesper], [GalacticTeaDesignatum.someoneDrinkingTea]] } def galacticTeaDependence : MutualDependence GalacticTeaDesignatum where toRaw := galacticTeaChain.toRaw (Interdependence.ofElaboration teaElaboration) holds := by decide theorem galacticTeaDependence_components : galacticTeaDependence.components = [meDrinkingTea, earth, bigBang, vesper, someoneDrinkingTea] := rfl def bigBangVesperTeaDependence : MutualDependence GalacticTeaDesignatum := MutualDependence.triple teaElaboration bigBang vesper someoneDrinkingTea bigBang_vesper_interdependent vesper_someoneDrinkingTea_interdependent def bigBangEarthTeaDependence : MutualDependence GalacticTeaDesignatum := MutualDependence.triple teaElaboration bigBang earth meDrinkingTea earth_bigBang_interdependent.symm meDrinkingTea_earth_interdependent.symm inductive TeaBefore : GalacticTeaDesignatum → GalacticTeaDesignatum → Prop where | bigBang_vesper : TeaBefore GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.someoneDrinkingTea | bigBang_earth : TeaBefore GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.meDrinkingTea def teaRank : GalacticTeaDesignatum → Nat | .bigBang => 0 | .vesper => 0 | .earth => 0 | .someoneDrinkingTea => 1 | .meDrinkingTea => 1 | bigBangProducingVesper => 0 | moreBigBang => 0 | bigBangProducingEarth => 0 | moreVesper => 0 | someoneOnVesper => 1 | someoneDrinkingTeaOnVesper => 1 | moreEarth => 0 | meOnEarth => 1 | meDrinkingTeaOnEarth => 1 theorem teaBefore_rank_lt {x y : GalacticTeaDesignatum} (h : TeaBefore x y) : teaRank x < teaRank y := by cases h <;> decide def teaBefore_temporal {x y : GalacticTeaDesignatum} (h : Relation.TransGen TeaBefore x y) : Temporal GalacticTeaDesignatum x y := by induction h with | single hxy => cases hxy with | bigBang_vesper => exact .ofMutualDependence bigBangVesperTeaDependence bigBang_designatum_mem someoneDrinkingTea_designatum_mem | bigBang_earth => exact .ofMutualDependence bigBangEarthTeaDependence bigBang_designatum_mem meDrinkingTea_designatum_mem | tail hxy hyz _ => have hlt := Temporality.rank_lt_of_transGen (base := TeaBefore) (rank := teaRank) teaBefore_rank_lt hxy cases hyz <;> exact (Nat.not_lt_zero _ hlt).elim def teaTemporal : Temporality GalacticTeaDesignatum := Temporality.ofBaseRank TeaBefore teaRank teaBefore_rank_lt teaBefore_temporal inductive TeaCauses : GalacticTeaDesignatum → GalacticTeaDesignatum → Prop where | bigBang_vesper : TeaCauses GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.someoneDrinkingTea | bigBang_earth : TeaCauses GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.meDrinkingTea def teaCausal : Causal GalacticTeaDesignatum where toTemporality := teaTemporal Causes := TeaCauses causes_before := fun h => by cases h with | bigBang_vesper => exact Relation.TransGen.single TeaBefore.bigBang_vesper | bigBang_earth => exact Relation.TransGen.single TeaBefore.bigBang_earth example : Temporal GalacticTeaDesignatum GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.someoneDrinkingTea := teaTemporal.certify (Relation.TransGen.single TeaBefore.bigBang_vesper) example : Temporal GalacticTeaDesignatum GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.meDrinkingTea := teaTemporal.certify (Relation.TransGen.single TeaBefore.bigBang_earth) theorem vesperEarthTea_not_before : ¬ teaTemporal.Before GalacticTeaDesignatum.someoneDrinkingTea GalacticTeaDesignatum.meDrinkingTea := by intro h change Relation.TransGen TeaBefore GalacticTeaDesignatum.someoneDrinkingTea GalacticTeaDesignatum.meDrinkingTea at h exact Nat.lt_irrefl 1 (Temporality.rank_lt_of_transGen (base := TeaBefore) (rank := teaRank) teaBefore_rank_lt h) theorem earthVesperTea_not_before : ¬ teaTemporal.Before GalacticTeaDesignatum.meDrinkingTea GalacticTeaDesignatum.someoneDrinkingTea := by intro h change Relation.TransGen TeaBefore GalacticTeaDesignatum.meDrinkingTea GalacticTeaDesignatum.someoneDrinkingTea at h exact Nat.lt_irrefl 1 (Temporality.rank_lt_of_transGen (base := TeaBefore) (rank := teaRank) teaBefore_rank_lt h) theorem vesperTea_not_before_bigBang : ¬ teaTemporal.Before GalacticTeaDesignatum.someoneDrinkingTea GalacticTeaDesignatum.bigBang := by apply teaTemporal.asymm change Relation.TransGen TeaBefore GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.someoneDrinkingTea exact Relation.TransGen.single TeaBefore.bigBang_vesper theorem earthTea_not_before_bigBang : ¬ teaTemporal.Before GalacticTeaDesignatum.meDrinkingTea GalacticTeaDesignatum.bigBang := by apply teaTemporal.asymm change Relation.TransGen TeaBefore GalacticTeaDesignatum.bigBang GalacticTeaDesignatum.meDrinkingTea exact Relation.TransGen.single TeaBefore.bigBang_earth end GalacticTea ===== FILE: KannoSoe/Meta/InterpenetrationExamples.lean ===== import KannoSoe.Signature.Interpenetration import KannoSoe.Meta.Examples /-! # Interpenetration examples The declarations below instantiate formal priming for the galactic-tea example. Calling the primed system a *floor-tier* presentation is a supplied reading, not a formal status encoded by the model. Priming connects branches which remain distinct in the base presentation and makes certification uniform, with the same universal behavior exhibited directly by `BeingAndGrading.universalInterdependence`. -/ namespace GalacticTea abbrev PrimedGalacticTeaDesignatum := Option GalacticTeaDesignatum /-- The galactic-tea elaboration with a fresh web designatum. -/ def primedTeaElaboration : Elaboration PrimedGalacticTeaDesignatum := Elaboration.prime teaElaboration /-- The terminal tea-drinking results are not joinable in the base system. -/ theorem tea_drinkingResults_not_joinable : ¬ teaElaboration.Joinable GalacticTeaDesignatum.meDrinkingTeaOnEarth GalacticTeaDesignatum.someoneDrinkingTeaOnVesper := by decide /-- Priming makes the previously non-joinable terminal tea-drinking results joinable. -/ theorem primedTea_drinkingResults_joinable : primedTeaElaboration.Joinable (some GalacticTeaDesignatum.meDrinkingTeaOnEarth) (some GalacticTeaDesignatum.someoneDrinkingTeaOnVesper) := Elaboration.prime_joinable_total teaElaboration _ _ /-- The terminal `moreEarth` and `moreVesper` residues are not joinable at base. -/ theorem tea_moreEarth_moreVesper_not_joinable : ¬ teaElaboration.Joinable GalacticTeaDesignatum.moreEarth GalacticTeaDesignatum.moreVesper := by decide /-- Priming makes the previously non-joinable terminal branch residues joinable. -/ theorem primedTea_moreEarth_moreVesper_joinable : primedTeaElaboration.Joinable (some GalacticTeaDesignatum.moreEarth) (some GalacticTeaDesignatum.moreVesper) := Elaboration.prime_joinable_total teaElaboration _ _ /-- The interdependence derived from the primed tea elaboration is universal. Unlike `BeingAndGrading.universalInterdependence`, whose proofs are definitionally `True`, this universality is a theorem forced by the priming construction. -/ theorem primedTea_interdependent_total (c₁ c₂ : Component PrimedGalacticTeaDesignatum) : (Interdependence.ofElaboration primedTeaElaboration).Interdependent c₁ c₂ := Elaboration.prime_interdependent_total teaElaboration c₁ c₂ /-- The raw five-component shape underlying `galacticTeaDependence`, stated without reusing its certification proof so the primed example exposes exactly which proof obligation priming discharges. -/ def rawGalacticTeaDependence : RawMutualDependence GalacticTeaDesignatum where interdependence := Interdependence.ofElaboration teaElaboration c₁ := meDrinkingTea middle := [earth, bigBang, vesper] cₙ := someoneDrinkingTea /-- The raw galactic-tea component chain lifted into the primed domain. -/ def primedGalacticTeaRaw : RawMutualDependence PrimedGalacticTeaDesignatum := RawMutualDependence.mapComponents rawGalacticTeaDependence some (Interdependence.ofElaboration primedTeaElaboration) /-- Under the base elaboration, `galacticTeaDependence` supplies four explicit adjacent interdependence proofs. Under the prime, the same component shape is certified uniformly by `Elaboration.prime_certification_trivial`. -/ def primedGalacticTeaDependence : MutualDependence PrimedGalacticTeaDesignatum where toRaw := primedTeaElaboration.certify primedGalacticTeaRaw holds := by exact Elaboration.prime_certification_trivial teaElaboration primedGalacticTeaRaw end GalacticTea ===== FILE: KannoSoe/Meta/ReachabilityExamples.lean ===== import KannoSoe.Signature.Rules /-! # Reachability examples This small finite system records that every component of an elaborated mutual dependence is available to ordinary reachability, including a component in the middle of the displayed chain. -/ namespace ReachabilityExamples inductive Designatum where | x | a | μ | b | unrelated deriving DecidableEq, Repr open Designatum abbrev elaboration : Elaboration Designatum := Elaboration.ofRules [ { source := x, components := [[a], [μ], [b]] } ] /-- A source may enter a middle component of its elaborated body. -/ theorem middle_reachable : elaboration.Reaches x μ := by rw [← Elaboration.Rules.mem_reachSet_iff] decide /-- The same fact is available through the verified `Joinable` decision. -/ theorem middle_joinable : elaboration.Joinable x μ := by decide /-- A designatum absent from every rule remains unrelated. -/ theorem unrelated_not_joinable : ¬elaboration.Joinable x unrelated := by decide /-- Reversing every displayed alternative does not change base reach. -/ theorem reversal_closure_same_reach : (Elaboration.reversalClosure elaboration).Reaches = elaboration.Reaches := Elaboration.reaches_reversalClosure elaboration end ReachabilityExamples ===== FILE: KannoSoe/Meta.lean ===== import KannoSoe.Meta.Examples import KannoSoe.Meta.ReachabilityExamples import KannoSoe.Meta.InterpenetrationExamples ===== FILE: KannoSoe/Signature.lean ===== import KannoSoe.Signature.V2 import KannoSoe.Signature.Rules import KannoSoe.Signature.Interpenetration ===== FILE: Exposition/Preamble.md ===== # Jingqing’s pip-and-peck potential A chick ready to hatch pips from within the shell; the hen answers from without. Zen calls their meeting *pip and peck at once*. A monk asks Jingqing: “This student pips; please, teacher, peck.” Jingqing says: “Will it come alive, or not?” The monk says: “If I don’t come alive, I’ll be met with people’s blame and ridicule.” Jingqing says: “Another man in the weeds.” — *Blue Cliff Record*, Case 16 ===== FILE: Exposition/Theory.md ===== # Kannō-Sōe Mutual Dependence (KSMD) KSMD implements a formal theory of provisional non-reifying ontology inspired by Zen sayings. The use of formal modelling is primarily for internal accountability in defining the system—please note that every notable conclusion of the model follows only from the modelling decisions made during the creation of the project. Those decisions are certainly inspired by Buddhist traditions, but were not at all over-constrained to *this* specific approach by the source material. There is significant interpretive design input and assumption in the model defined according to my own judgement. That said, I invite you to investigate the model, see what matches or does not match your own understanding, and if possible share your perspective on it in the repository [Discussions](https://github.com/kanno-soe/kanno-soe/discussions) or [Issues](https://github.com/kanno-soe/kanno-soe/issues) pages. Nb. the equations only restate what the prose and diagrams have already stated—they are 100% fine to gloss over or read selectively. ## The formal core: designata, elaboration, and Mutual Dependence A **designatum** is simply something the model can designate. It does not first divide designata into people, objects, events, thoughts, or times. A **component** is a nonempty group of designata (`{a, b, c, ...}`). An **elaboration** (⇓ reads as "elaborates to") is a relation saying that a designatum may be expanded into a raw Mutual Dependence; because it is a relation rather than a function, one designatum may have no stated elaboration, one elaboration, or several alternatives. Alternatives are simultaneously available dependence-explanations rather than mutually exclusive outcomes. The **raw structure of a Mutual Dependence** `m` is a list of at least two components (C₁, ..., Cₙ) where every adjacent pair are symmetrically interdepending (⋈): ```text m ⇓ [C₁ ⋈ C₂ ⋈ C₃ ⋈ ... ⋈ Cₙ] not required: a temporal order, a causal arrow, or direct interdependence of non-adjacent components ``` or as an equation: ```math C_1 \bowtie \cdots \bowtie C_n \quad\Longleftrightarrow\quad \bigwedge_{i=1}^{n-1}(C_i\bowtie C_{i+1}) ``` As components may contain designata, and a designatum may be elaborated to a mutual dependence, the elaborated components can look like: ```text ab ⇓ [{a} ⋈ {b}] fg ⇓ [{f} ⋈ {g}] m ⇓ [{ab, c, d} ⋈ {e} ⋈ {fg} ⋈ {h}] ``` Here the first component of `m` has 3 designata, `ab` which designates (elaborates to) a mutual dependence `[{a} ⋈ {b}]`, and `c`, and `d`, which each are designata without defined elaboration. A designatum `d` **reaches** another designatum `w` (`d →* w`) if it can get there in zero or more steps of elaboration. Every designatum reaches itself. If `d` elaborates to `[C₁ ⋈ ... ⋈ Cₙ]`, one step may enter any designatum in any component. Or more formally, fixing $E$, the elaboration approach, write $\to$ for $\to_E$, and with M as elaborated mutual dependence, let $\to^*$ denote the reflexive–transitive (Kleene-star) closure of $\to$: ```math d\to e \quad\Longleftrightarrow\quad \exists M,\; E(d,M)\land e\in\bigcup\operatorname{components}(M) ``` ```math \frac{}{d\to^*d} \qquad \frac{d\to e\qquad e\to^*w} {d\to^*w} ``` Designata are **joinable** (↓) if there is a shared designatum `w` that both can reach: ```text +--> p ----> / designatum b --elaborates \ +--> q ----> common witness w designatum e --elaborates----> r ----> common witness w b ↓ e := there is some w reached from both b and e ``` or as an equation: ```math d \downarrow e \quad\Longleftrightarrow\quad \exists w.\; d \to^{*} w \leftarrow^{*} e ``` This joinability is reflexive and symmetric, but it need not be transitive (which means that just because b ↓ e and suppose e ↓ fg, it isn't necessarily true that b ↓ fg). An **interdependence** (⋈) between two components is a stronger requirement than just finding a joinable pair: every designatum in the first component must have a joinable partner in the second, and every designatum in the second must have a joinable partner in the first. ```text component C component D +---------+ +---------+ | c1 | -- joinable partner ↓ | d? | | c2 | -- joinable partner ↓ | d? | | c? | ↓ joinable partner -- | d1 | | ... | | ... | +---------+ +---------+ C ⋈ D requires coverage in both directions. For singleton interdependence, C ⋈ D is true iff c ↓ d ``` or as an equation (interdependence is the Egli–Milner lifting of joinability): ```math A\;\overline{\downarrow}\;B \iff \bigl(\forall d\in A\,\exists e\in B.\;d\downarrow e\bigr) \land \bigl(\forall e\in B\,\exists d\in A.\;e\downarrow d\bigr) ``` ```math A\bowtie B \quad\overset{\mathrm{def}}{\Longleftrightarrow}\quad A\;\overline{\downarrow}\;B ``` The interdependence **chain** may be any finite length. It can be sliced and compatible chains can be concatenated. Although examples in this exposition involve linear chains, two chains may include the same designatum. In that case it's really a chain *network*, with each designatum having a "valency". A designatum of an interior component of a linear chain has valency 2, while a designatum appearing in multiple chains might have valency >2. This is the minimal formal structure of **Mutual Dependence** (*sōe*). Throughout, that structure is read as **mujishō-sōe**: mutual dependence without-own-being (*mujishō*), in which neither side supplies a self-standing substrate for the other. ## Resonance as a Mutual Dependence A **Resonance** is the following four-component special case of Mutual Dependence, with its middle components forced to be singletons: ```text calls ⋈ {b₁} ⋈ {b₂} ⋈ responses ``` The intended reading is that `b₁` is the receiving view or moment of a being and `b₂` is its responding view or moment. Formally, however, `b₁` and `b₂` are two interdependent singleton designata in the same certified dependence. The model does not prove that they are numerically identical, temporally successive, conscious, or personal. The names **calls**, **receiving**, **responding**, and **responses** are role-readings of the shape. An **Encounter** is a Resonance viewed merely as a Mutual Dependence. It retains the concrete `calls ⋈ {b₁} ⋈ {b₂} ⋈ responses` shape while everything about it being a resonance is temporarily forgotten. *Encounter* is an expository alias, not a new Lean type. Every Encounter is a Mutual Dependence; not every Mutual Dependence has the four-component singleton-middle shape needed to be an Encounter. Because designata may elaborate into any raw dependence the modeler supplies and later certifies, the same Resonance shape can be used for a person answering a question or a stone answering the wind by rolling downhill: ```text {wind} ⋈ {stone-receiving} ⋈ {stone-responding} ⋈ {rolling} ``` Nothing in the ungraded structure privileges the person. Nor does the stone example prove a doctrine about sentience: it proves only that the Resonance constructor asks for interdependent singleton designata in its two middle positions, not a prior metaphysical kind called *person*. ## Graded Resonance > Sentient beings originally are Buddha. > Being like water and ice, > leaving water there is no ice, > outside of sentient beings there is no Buddha. > > — Hakuin Ekaku, *Song of Zazen* A **Graded Resonance** adds two independent grades to a Resonance: a calls-side grade and a responses-side grade. The grade type need only be a preorder with a bottom element. It need not be numerical, total, or metrically spaced. The intended reading is **dis-resonance**: volition insofar as it is *sāsrava*—with outflows, ripening in further becoming. Bottom is *anāsrava* at this Resonance: the act is not productive of further becoming, without implying either the absence of volition or the global attainment of arhatship. `0` is only the familiar numerical example. How a bottom grading relates in the world is left as a functional question about the relating of such moments, and could be modelled by downstream effects on other resonances. ```text one Graded Resonance calls ⋈ {b₁} ⋈ {b₂} ⋈ responses (callsGrade) (responsesGrade) callsGrade and responsesGrade are independent coordinates. ``` A stone can prompt volition, not have it; only volition makes a cause karmic. That is the whole difference between non-karmic and karmic cause/effect. Likewise it can feed āsravas, not have them. Thus a stone is assigned bottom on both sides, while a grumpy person who has stubbed a toe may be *assigned* a non-bottom calls grade, a non-bottom responses grade, or both. Those are interpretations supplied to the model; the model itself does not itself infer a grade. Grading is sentience-neutral. A sentience reading *could* be supplied as additional information, but it's not inherently required in the model. ## Being A **Being** is a mutual dependence of singleton-only designata. ```text being ⇓ [{b₁} ⋈ {b₂} ⋈ {b₃} ⋈ ... ⋈ {bₙ}] ``` The designata are implied to be *imputed* from (share common elements with) the `b₁` and `b₂` of resonances. A temporal/causal reading (described below) may also be supplied. ## Temporality and Causation are overlays > In this being, that is. > Owing to the arising of this, that arises. > In this not being, that is not. > Owing to the cessation of this, that ceases. > > — Buddha, *Udāna* 1.3 > Note: This section will be revised, it puts forward a definition of Cause which is intuitive but > confusingly different from the one the Buddhist tradition uses. > > I’ll try to briefly explain the difference pending bringing this more into line with the Buddhist use of the terminology. > > Firstly, in Buddhist terminology, ”A Causes B” does not necessarily imply ”A Before B”. I’ll provide two (not-necessarily-exhaustive) examples: > > a) The tradition’s example: You stack two reeds leaning against each other, and leave them leaning against one another. Afterwards it’s correct to say A is Causing B to remain standing, and B is Causing A to remain standing. > > b) My own unrelated example: The upcoming World Cup (of whichever sport) is to be hosted in Antarctica. Because of the World Cup taking place, there’s a building of stadiums. The building of stadiums causes the World Cup to take place. Though you could dissect this into a linear causation process, you aren’t required to do so. In farness, the tradition might use “conditions” for the latter, but the general idea is that designation of A and B could be broad enough that within there are genuine Causal relations in each direction, which the whole validly takes on as its own Causal relations when discussing it. > > Lastly, (as I understand it) a matter of taste: you should be able to say ”A Before B” without having to state > the way they mutually depend in any more detail / separate from the statement already made. The statement you make of “A Before B” > already suffices as its own mutual dependence statement (in the sense of A’s beforeness to B, B’s afterness to A). Mutual Dependence and Resonance contain no time-directedness. A **Temporality** interpretation is supplied separately as a strict transitive **Before** (≺) relation with, for every `x ≺ y` claim, a **Temporal** certificate. A domain may then supply a **Causal** (↝) interpretation with a `x ↝ y` relation that implies `x ≺ y`. The certificate is simply a mutual dependence with `x` at one end and `y` at the other. ```text temporal certificate: {x, ...} ⋈ ... ⋈ {..., y} temporal overlay: x ≺ y causal assertion: x ↝ y x ≺ y => a mutual dependence with `x` at one end and `y` at the other x ↝ y => x ≺ y ``` Because Before is strict, the causal relation is asymmetric: `x ↝ y` rules out `y ↝ x`. Forgetting the causal and temporal overlays leaves the certificate as just like any other mutual dependence without causal and temporal interpretations. To summarise, mujishō-sōe is the dependence-structure retained when either grading or the causal and temporal overlays are forgotten. ## From empty dependence to the provisional middle > Dependent arising we declare emptiness. > That is a dependent designation; precisely that is the middle way. > > — Nāgārjuna, *Mūlamadhyamakakārikā* 24.18 Remove grades from a Graded Resonance and the Temporal/Causal overlay, and the Mutual Dependence remains. That by itself is not a Buddhist metaphysics — the philosophical bridge begins when the act-grammar reads the mutual dependence (**sōe**) as **mujishō-sōe**: mutual dependence under the condition of no own-being. *Mujishō* (無自性) means without self-nature or own-being. The formal model's interdependence relation is a simple analogue —neither interdependent component is entered as the self-standing base of the other. This is from Nāgārjuna's *MMK* 24.18: what dependently originates is empty of own-being; that emptiness is itself dependently designated; just this is the middle way. Therefore mutual dependence doesn't mean relations among already self-subsisting things, and emptiness doesn’t mean a deeper thing beneath them. Jizang supplies the next turn. In the fourfold two truths, each stated ultimate—including the conventional/ultimate distinction itself—can become the conventional content of the next analysis. The iteration does not discover a final unconditioned proposition, it ends at words forgotten, thought cut off (言忘慮絶): not another claim but the place where words and thought no longer do separating work. That claimless place is called the **floor**. The **middle** can then manifest as this case, instead of becoming another object of analysis. This manifestation is called **genjōkōan**, the **provisional middle**. | Dependence reading | Enactment reading | |---|---| | **mujishō-sōe** — mutual dependence without own-being | **genjōkōan** — the case manifesting fully | The **dependence-face** names the relation retained when additions are forgotten; the **enactment-face** names how that relation comes forward as a case. Mujishō-sōe is the dependence-face of Row 1: this Encounter has no self-standing substrate. Genjōkōan is its enactment-face: that empty dependence nevertheless manifests as this call, this receiving, this response. *Provisional* doesn’t mean half-real or merely hypothetical, it says that the case is concrete without being promoted into a final ground. ## From no rank to practice-realization > A monk asks: “What is the true person of no rank?” The master grabs him: “Speak! Speak!” > The monk hesitates. The master pushes him away: “The true person of no rank—what a dried piece of shit!” > > — Línjì Yìxuán, *The Record of Línjì* Genjōkōan answers how groundless dependence comes forward as a case. Linji supplies its guard-image. The reconstruction reads the true person of no rank (無位真人) along a seam: *no rank* (無位) is non-attainment; the true person going in and out (真人…出入) through the face-gates prevents no-rank from becoming inert; the whole figure holds no-rank and activity together. When the monk asks what the true person is—and then hesitates under Linji’s demand to speak—the phrase threatens to become a resting-place. Linji’s rebuff destroys that possibility, discarding even the “true person of no rank” once it begins to function as something identifiable or possessable. This no-rank, no-resting-place reading is called the **non-attaining middle**, or **unattaining middle**, when the emphasis falls on nothing being obtained or stored. The reconstruction states that reading in Dōgen's vocabulary. **Shu** (修) is practice, the concrete doing. **Shō** (証) is realization, with the non-attaining floor at bottom placement in any given grading of a resonance. The homophone differs from the the *shō* in *mujishō*, which is 性, nature, while the **shō** in *shushō* is 証, realization. Shō gains determinate content through a contrast within practice. At a bottom placement, practice intersects with the non-attaining floor: the act's subject-position is ceded, with nothing in the doing answering to a dis-resonant "self-forwards". At a non-bottom placement, that same practice is delusive to the extent that it arrogates the subject-position. This gives the non-attaining floor-face its grading counterpart. Genjōkōan has no corresponding delusion term: its contrast is empty dependence versus manifestation. **Shushō** (修証) says practice-realization; **shushō-ittō** says that its practice and realization are non-dual. That cannot mean two events—practice first and an attained realization later—nor a still shō somehow acting by itself. ```text one Graded Resonance practice, the doing (shu) ---- shushō ---- (shō) realization, as verified shushō-ittō: not two events ``` **Genjōkōan**, the provisional middle, answers *how does empty dependence manifest as this case*? **Shō** answers *what is realization as verified*? Their distinction remains live when the grading is diagnosed, and loses its separating work where not. ## The act-grammar grid > Carrying the self forward and practice-realizing the myriad dharmas is deemed delusion; the myriad dharmas coming forward and practice-realizing the self is awakening. > > — Dōgen, *Genjōkōan* > > To learn the Buddha Way is to learn the self. > To learn the self is to forget the self. > To forget the self is to be realized by the myriad dharmas. > To be realized by the myriad dharmas is to shed the body and mind of the self and the body and mind of other-selves. > There’s a resting of the traces of realization; a causing of the rested traces of realization to issue forth, long, long. > > — Dōgen, *Genjōkōan* > *Practice in the midst of activity surpasses practice in stillness a hundred, a thousand, a hundred million times over.* > > — Hakuin Ekaku, *Orategama* I, quoting Dahui Zonggao An **act-grammar** grid pairs a dependence-reading with an enactment-reading of one graded resonance across three rows. The enactment cells pick out three aspects of the quoted passages: *genjōkōan* is the actualizing of the case, *banpō susumite jiko o shushō suru* is the dharmas coming forward and the self being verified, and *dōchū no kufū* names that practice-realizing under the conditioning and temporal readings. | Dependence reading | Enactment reading | Modelling | |---|---|---| | **mujishō-sōe** — mutual dependence without own-being | **genjōkōan** — the case manifesting fully | Mutual Dependence | | **kannō-sōe** — responsive resonance placed under dis-resonance grading | **banpō susumite jiko o shushō suru** — the myriad dharmas coming forward and practice-realizing the self | Graded Resonance | | **engi / inga** — dependent arising and cause/effect | **dōchū no kufū** — practice in the midst of activity | Conditioning and Temporality | Row 1 reads the resonance as manifestation without a substrate; Row 2 reads it as graded receiving and responding; Row 3 reads the doing under conditioning and temporality. Conversely, forgetting Row 3's overlays and Row 2's grades returns the one mutual dependence of the encounter. ## Floor-face and act-time face **Floor** is defined as the term *nippapañca-dhātu*, a privative term of “not proliferation”. **Act-time** is defined as the term *vacī-saṅkhāra*, a term for discursive/verbal thought. The two terms can intersect, in what we might call **discernment-without-grasping**, however in common usage each is a term focusing on that specific definition without considering whether the other term is present of not (like how “large” and “green” can intersect, but as themselves have no notion of the other, either positively or negatively). We can talk of the ”floor” at act-time in the same way that one can talk of sleep at act-time — it doesn’t in itself require the person to be sleeping to do so, or cause one to sleep necessarily, nor give a fully accurate impression of what sleep is, or anything like that. The floor is not a first moment, a hidden base, or a final substance. Generally, we talk of the floor as *doing no separating work*. That’s because even though distinctions can be made in discernment-without-grasping (the intersection of act-time with floor), the floor term itself has no notion of separation. Act-time is the conventional diagnostic tier at which this call, this receiving, this response, this practice, and the distinctions needed to describe them are live. The **floor-face** is another case of act-time, floor intersection, this time with no elaboration either, which corresponds to “thusness”. The shushō reading introduced above is one example: ```text one Graded Resonance act-time face floor-face concrete practice (shu) ---- shushō ---- (shō-graded-at-bottom) the being-verified in receiving/responding ``` Act-time follows the concrete receiving at `b₁` or responding at `b₂`; the floor-face reads that same `b₁` or `b₂` without an independently standing receiver or responder. Shu and shō are reciprocal faces of that receiving or responding within the Graded Resonance: one name follows the enactment, the other its no-own-being, non-attaining realization. To seek not-proliferation through not-*vacī-saṅkhāra* would be a one-sided approach toward not-proliferation. On the other side, ignoring *nippapañca-dhātu* because it is a “not-“, and considering *only* act-time would be another form of one-sidedness. ## Separate/fuse, utterances, and their offers The **separate/fuse rule** states how distinctions behave across those tiers. At act-time a useful distinction separates. At the floor it fuses (floor = privative non-proliferation), meaning that it makes no separating claim there—not that its two sides become one substance (not-proliferation doesn’t assert this) and not that both propositions are asserted (not-proliferation doesn’t assert this either). || **Distinction separates** | **Distinction fuses** | |---|---|---| | **Act-time diagnosis** | `A \| B rule obeyed` | `A >< B collapse` | | **Floor** | `A \|\| B freeze` | `A . B rule obeyed` | The two error cells occupy one diagonal; the other diagonal is the rule obeyed. **Collapse**, written `><`, is premature fusion under act-time diagnosis; **freeze**, written `||`, is a useful separation reified as a floor-claim. “There is no time, no being, and no Resonance” is a collapse when offered where a response is occurring. A flowing time-container, substantial Being, stored shō, or self-existing Resonance is the corresponding kind of freeze. An **utterance** isn’t a sentence-shape in isolation but its content carried by a resonance, with the call it answers and the tier at which it’s offered. The taxonomy in the section below checks the offer not the words alone. Ordinary narration offered conventionally at act-time is no error; the same words offered as ultimate furniture can freeze, while a denial offered as live diagnosis can collapse. ## The articulation joint At an **articulation joint**, a distinction remains usable at act-time without receiving intrinsic standing at the floor. Freeze and collapse are the two ways this relation can fail. Each can operate either on a conventional articulation or on the deflationary correction of one. The rows below name the material being mishandled. The columns name what is done with it. | Material being mishandled | **Freeze `\|\|`: assigns final standing** | **Collapse `><`: removes live separation** | |---|---|---| | **Conventional articulation** — a live designation or distinction | **Intrinsic-joint realism.** `act-time → floor`: a usable term is treated as intrinsic. A being becomes substantial Being, shō becomes something stored, or the doer is placed prior to the deed. | **Identification.** `act-time → act-time`: terms whose difference remains live are fused. Sentience is read off function, or genjōkōan and shō are conflated. | | **Deflationary correction** — a denial or other floor-speech | **Ground-reification.** `floor → floor`: emptiness, nonduality, or the web is installed as a final item or ground. Nihilism and emptiness-sickness (空病) belong here. | **Erasure.** `floor → act-time`: a correction is used to cancel the live case. “No time” or “no being” denies an act underway; “does not fall under cause and effect” erases conduct where conduct matters. | Identification and erasure are therefore different forms of collapse. Identification fuses terms within a live articulation. Erasure imports a deflationary correction into that articulation and uses it to cancel the case. The freeze cells differ in the same way. Intrinsic-joint realism gives final standing to something used in conventional articulation. Ground-reification fixes the corrective itself as the final answer. Here “ground” names what the error invents, not anything the framework accepts as a ground. The diagonals show the resulting register movements. Intrinsic-joint realism and erasure are register-mismatch errors: the first tries to carry act-time furniture as final, while the second’s attachment towards the floor causes the attempt to deny act-time. Identification and ground-reification are within-register errors: the first removes a distinction still needed at act-time, while the second tries to assert positive facts at the floor register. Dependent articulation guards against both kinds of collapse. Because a distinction is dependently articulated, its terms can remain different where the case requires them without becoming intrinsic. For the same reason, their lack of intrinsic standing does not erase their conventional use. The ladder section develops this point by showing that every ultimate correction remains dependent on the articulation it corrects and can itself become material for further correction. As elsewhere, these classifications concern an utterance with its call and offer, not a sentence-shape by itself. The same words may function as conventional articulation, intrinsic-joint realism, corrective medicine, or erasure according to the tier at which they are offered. ## A taxonomy of error > This section still references the old version of the code, and *weld*, a > conceptual fore-runner to (Graded) Resonance. The older model generally > produces reasonable conclusions, however mostly as a result of structural > artifact from reasonable modelling decisions as opposed to being > meaningfully proven. > > The prose below currently runs ahead of the Lean side: cells marked > `⟨no lemma yet⟩` have no formal counterpart, and the row names and table > order are not yet reflected in `tableOrder` or the affected lemma names. > > The occupant labels used below are expository classifications. The > current Lean development does not represent or audit them. Classical nihilism turns out to be a freeze, not a collapse: the void is emptiness reified as an *absence* — a snake wrongly grasped is still grasping. And mis-typing — the state-tool for an act-job, the faculty-reading of Row 2 — is the freeze at the dated-grade/agent-type joint specifically: an act's grade frozen into a standing configuration of the agent. The errors are categorised in two grades: 1. **Grammatical errors** — tier-errors and typing-errors. These the system can *assert*, because a mis-feed is a conventional-tier logic verdict, not a value. The old man of the fox kōan's mistake is assertable. (Assertable, note, *within the lens*: "tier-error" and "mis-feed" are verdicts of the two-truths machinery itself, compelled inside it and offered outside — the banner's clause governs the grid's own voice, and the asymmetry between the two grades is an asymmetry in that voice, not an appeal to lens-free logic.) 2. **Soteriological shortfalls** — arrogation, self-forward, low resonance, failure to meet beings. These the system can only *display* — Row 2 placements and Row 3 causation, valence borrowed from the object. The five hundred fox lives were returns, not punishments; by the same token "he failed to act as a bodhisattva" is never an asserted wrong, only a displayed asymmetry. ### Voice-discipline Two errors formerly tabled under description/injunction are, in their pure form, not committable by a being at act-time about an object-level call; they are violations of the split between the two grades itself, and are recorded here, where that split is defined, rather than as rows. *Refusing to state the asymmetry* is the display-half abandoned: a theory of poison that won't say which direction kills (`pole_validates_all_claims`, `poleTier_inhabited_of_liveTerminus`; at genjōkōan all claims validate, fused; the pole is not a truth-maker elsewhere). A being's analogue — meeting a call with less than the stating it needs — is not a grammatical error but the Grade-2 buddha-side shortfall. *"Eat this"* is the assertion-half usurped: the displayed asymmetry taken up *by the theory* as command — "escape this," the fourth truth said in the theory's voice, is this error applied to dukkha (`assertable_ne_displayable`). When a being mounts the same identification in an act-time utterance — theodicy in a mouth, another's suffering asserted as assignment — the error is tabled at ``. The recipient-side mirrors likewise remain in the table at `` and ``, because a being can commit them at a reception. ### Grade 1: the generator's output Each row isolates one distinction. Freeze and collapse are operations upon that distinction; the bold labels within each cell identify the material mishandled by the particular error-occurrence. A distinction may admit intrinsic-joint realism, ground-reification, or both as freezes, and identification, erasure, or both as collapses. Material type therefore belongs to an occupant of a cell, not to the row or cell as a whole. A single utterance or compound position may instantiate more than one occupant. Each occupied subtype is printed with its full bold label and description. `— structural: …` is reserved for a subtype that is genuinely unavailable. An unmentioned subtype means only that it is not currently tabled or established; it does not mean that the subtype is impossible. Table membership requires committability in a being's act-time utterance; theory-voice errors live in the voice-discipline note. A dash must state a cell-specific structural reason. Cuts follow classifying-lemma boundaries: a row's classifying lemmas are its own family (`*_obeys`, `*_not_freeze`, `*_collapse_self_refuting`, and cell-specific negatives); shared background lemmas — `no_final_level_of_errorFree` supports both `` and `` — do not by themselves merge distinct joints. | Distinction | **Freeze `\|\|`** | **Collapse `><`** | |---|---|---| | Rung / pole of the grade (kenshō / genjōkōan) | **Intrinsic-joint realism.** Genjōkōan held as *final* kenshō — the pole as top rung, awakening as a still attainment, daigo as rank; "full satori" is this freeze miniaturized — a state-word for a per-call pattern (`rungPoleRow_not_freeze`) | **Identification.** A kenshō spoken *as* genjōkōan — a rung as the floor; the Zen sickness (禅病) of "stinking of Zen," an opening inflated into arrival — the fox's error at another joint (`rungPoleRow_obeys`, `kensho_as_genjo_collapse_self_refuting`, `rung_not_pole_witness`) | | genjōkōan / shō (two middles) | **Intrinsic-joint realism.** Holding the two-middles distinction itself as a final floor-claim | **Identification.** Conflating them — manifestation taken as realization, or conversely | | shō / satori (証 / 悟) | **Intrinsic-joint realism.** Satori as a datable possession | **Identification.** Reading the floor-face as the awakening-mode, or conversely | | Dated grade / agent-type (the mis-typing joint; formerly act / state) | **Intrinsic-joint realism.** The act's grade frozen into a standing configuration of the agent — Resonance held as a faculty; buddha-nature as substance; the empty agent re-based. Distinct from doer/deed, where the doer's *priority* is reified — here it is the act's *type*; and from standing/dated, which takes the seed-side disposition against the dated act and expressly excludes configuration/act | **Identification.** The placement *being* the self — a grade of this dated act identified with the agent | | Function / share | **Intrinsic-joint realism.** Function frozen into a standing device-nature — the mirror given a stand; originally not a single thing (本来無一物) is the corrective (`functionShareRow_not_freeze`) | **Identification.** Universal response identified with its share-cell — share-zero treated as non-response, or live share treated as the only real function; the identity *I-making just is the clench* is this collapse in embryo (`functionShareRow_obeys`, `function_share_cell_collapse_self_refuting`) | | karma / inga | **Intrinsic-joint realism.** The soul: the index *stored* between welds — a standing bearer. Maximized, the solipsist's stored-index face annexes the whole field; the self-forward and Row 2-domain faces are neighboring cells in the compound decomposition rather than new rows (the solipsist is the stone's inverse: all response, no call, unable even to state what listening to Hyakujō would be) (`karmaIngaRow_not_freeze`, `solipsism_decomposition`) | **Identification.** The mis-feed: an index-free field fed to an index-requiring designation (`karmaIngaRow_obeys`, `misfeed_collapse_self_refuting`) | | Sowing / reaping (the diachronic index) | **Intrinsic-joint realism.** The retrospective soul: the reach-back held as a standing backward relation rather than spent at reception — memory's felt storedness read literally is this freeze in psychological dress (`sowingReapingRow_not_freeze`) | **Identification.** Ownership read off the series alone; sameness-of-being as bare continuity-fact (`sowingReapingRow_obeys`, `series_ownership_collapse_self_refuting`, `no_diachronicWhose_from_series_alone`) | | Delivery-question / index-question | **Intrinsic-joint realism.** One's future occurrence at others' Row 2 held now as a first-personal possession — "my potential," "my worth to them" — a delivery-fact, read at *their* act-times off whatever the field brings, frozen into something the being holds and could therefore weigh, spend, or withdraw — prudential privilege is this freeze's forward-facing twin, the cross-gap *whose* held as rational ground (`deliveryIndexRow_not_freeze`) | **Identification.** Mis-fed in either direction: an index-question fed to the index-free field (*did I earn this?* — akṛtābhyāgama's mis-feed half; *does the Tathāgata exist after death?* — the same mis-feed at the pole), or a delivery-fact arrogated by the weld — an act claiming command of what arrives next ("easy"; every exit-arithmetic; Devadatta's aim), authority over the one register no act holds (`deliveryIndexRow_obeys`, `misfed_register_collapse_self_refuting`) | | Weld / event-type (severity) | **Intrinsic-joint realism.** Victim-rank: severity read off the victim's station — the honorific inflating the crime; rank smuggled back through the tariff (`weldEventTypeRow_not_freeze`) | **Identification.** Karma graded off the event-type with the weld erased — Cunda owed remorse, intention deleted from the arithmetic (`weldEventTypeRow_obeys`, `eventType_grading_collapse_self_refuting`) | | Disposition / act (seed / clench) — **retyped: the distinction is standing/dated, never configuration/act** | **Intrinsic-joint realism.** The seed as bearer — ālaya frozen into a self carrying mineness between acts. Two further faces: the clench as *furniture* — contraction mistaken for a standing thing removable only with its substrate ("only ending me ends this"), dukkha held substrate-bound being this freeze wearing its valence, where de-clench is demolition-free by the same theorem that makes kenshō unholdable; and the clench as *structure* — contraction made constitutive of the being (anguish as the very form of consciousness — the Sartrean face; Zahavi's thin for-me-ness is expressly *not* this cell, taking the retype instead, per the placement in Identification) (`standingDatedRow_not_freeze`) | **Identification.** The dated occurrence read off the standing tendency — *he arrogates, so this act was arrogated* — prognosis substituted for diagnosis, Row 2 made to read seeds instead of deeds (what the determination reads — the configuration's part in driving *this* response — is not this cell: every act is the configuration's act); dukkha read off the seed — the proneness to suffer mistaken for suffering occurring — is the same collapse at the valence (`standingDatedRow_obeys`, `prognosis_as_diagnosis_collapse_self_refuting`, `standing_does_not_determine_dated`) | | Per-weld mark / standing sentience | **Intrinsic-joint realism.** Sentience held as a nature the being has — affirmation or denial as nature (性); the mark is per act or it becomes a soul-shaped kind (`standingSentienceRow_not_freeze`) | **Identification.** Sentience identified with grid-visible function, in either direction — the retired `SentientTag = MountsSomewhere` identity was this collapse; machine behavior does not recover the mark (`standingSentienceRow_obeys`, `sentience_from_function_collapse_self_refuting`, `no_sentience_recovery`) | | Displayed valence / issued command (uptake and issue of the orange) | **Intrinsic-joint realism.** The displayed asymmetry held as standing floor-furniture, persisting between calls rather than arising as the valence of this reception ⟨no lemma yet⟩ | **Identification.** Three occupants of one identification — valence taken as command — across two banks of a command never issued. Recipient-bank: defiance — the orange refused *as* command, shadow-boxing a voice the grid does not have (its one grammatical component; the rest of defiance remains Grade-2 display); and compliance — the asymmetry obeyed *as* order, distinct from value-uptake, which remains grid-legal (`assertable_ne_displayable`; legality of value-uptake: `existentialism_decomposition`, `existentialism_legal_count`). Issuer-bank: the asymmetry uttered *as* assignment at another's reception — theodicy in a being's mouth, suffering asserted as sentence, akṛtābhyāgama's displayed valence read out as command ⟨no lemma yet⟩. The theory-voice forms of both halves live in the voice-discipline note | | shu / shō (the weld) | **Intrinsic-joint realism.** Two one-sided freezes: shō without shu (quietism, Dahui's silent-illumination target — emptiness that only empties) and shu without shō (practice as means to a later attainment, breaking shushō-ittō) (`foxWeldRow_not_freeze`) | **Erasure.** The fox: not-fall asserted conventionally — antinomianism. Converse fox: not-obscure insisted on at the floor — moralizing where nothing falls (`foxWeldRow_obeys`, `fox_notFall_collapse_self_refuting`, `fox_utterance_misfits_live_offer`) | | Doer / deed | **Intrinsic-joint realism.** The prior doer: kāraka held prior to karman, MMK 8's target occupying its own cell; the soul in relational dress, distinct from the Pudgalavāda cell because here the *priority* is reified (`doerDeedRow_not_freeze`, `DoerDeedNegative.no_priority_recovery`) | **Erasure.** *No doer, only deeds* — bundle-reductionism spoken as live diagnosis, mounted by a being answering a call (`doerDeedRow_obeys`, `no_prior_doer_collapse_self_refuting`) | | Self-pole / transposed (the terminus index) | **Intrinsic-joint realism.** The transposition erased upward: a self-pole weld held persisting at the summit — the subtlest soul, the true person of no rank (無位真人) as rank in weld-vocabulary; and *transposed* itself held as mechanism — an index that travels — is a miniature of the same freeze (`selfPoleTransposedRow_not_freeze`) | **Erasure.** The transposition erased downward: the terminus-act asserted indexless *and inert* — no self-pole and no standing at others' receptions either, the device dead even at others' Row 2; the exit-collapse in typing's clothes (`selfPoleTransposedRow_obeys`, `transposition_erased_downward_collapse_self_refuting`) | | Before / after (the arrow, retyped; Lean-generated schema row) | **Intrinsic-joint realism.** The flowing container: temporality held as floor-furniture — *time really flows* — the retrospective soul's cosmological dress; eternalism-of-the-flow and the block-denier's arrow both land here, against `DirectionNegative` (`beforeAfterRow_not_freeze`) | **Erasure.** The deflation: *no time, so nothing happens, no one acts* — not-fall transposed to time, the fox's sentence at its largest scale; a floor-truth uttered where the conventional tier was live (`beforeAfterRow_obeys`, `no_time_collapse_self_refuting`, `beforeAfterLadder_obeys_succ`) | | Intra-weld arrow (call/response order) | **Intrinsic-joint realism.** Temporality as interior furniture: *the call really is first*, before-and-after smuggled inside the weld against the transposition witness (`intraWeldArrowRow_not_freeze`, `InteriorDirectionNegative.no_interior_direction_recovery`, `intraWeldArrow_sunyata`) | **Erasure.** The deflation: *no call/response order, so no acts* — the interior arrow denied as a live diagnosis, refuting its own act-time tier (`intraWeldArrowRow_obeys`, `no_order_collapse_self_refuting`, `contentIntraWeldArrowRow_obeys_of_variation`) | | Named being / floor (the being-convention; Lean-generated schema row) | **Intrinsic-joint realism.** The conventional designation is promoted to ontology: *prajñapti-sat* is taken as *dravya-sat* (*samāropa*), and the partition is held as floor-furniture against `BeingNegative` (`beingsRow_not_freeze`). Lewis is the nearest miss, right about plenitude and wrong about register; Huayan affirms the plenitude empty; Pudgalavāda is the classical occupant candidate. The monolithic self's soul is this freeze in fiber dress.

**Ground-reification.** Emptiness or absence is installed as final, so the correction “no being in itself” hardens into non-being as the floor. | **Identification.** No intrinsic cut is taken to mean no difference between being and non-being; the live convention and its absence are fused.

**Erasure.** *There are no beings* — the fox's sentence at the being-joint, the deflation's second dress; “no beings” offered as live diagnosis refutes its own tier (`beingsRow_obeys`, `no_beings_collapse_self_refuting`). Diamond Sūtra denial belongs here when spoken as live ontology rather than floor medicine. | | Weld-grain / floor (the weld-convention; Lean-generated schema row) | **Intrinsic-joint realism.** The weld as svabhāva: one act-grain held as floor furniture, the last unemptied level pretending it was never a convention (`weldRow_not_freeze`, `weld_sunyata`) | **Erasure.** *No acts happen* — the fox's sentence at the act-joint, the deflation's last dress; "no welds are actual" offered as live diagnosis refutes its own tier (`weldRow_obeys`, `weld_denial_collapse_self_refuting`) | | Terminus / exit | **Intrinsic-joint realism.** Private nirvāṇa as a rank; the pratyekabuddha freeze — *soteriological solipsism*: not denying that others exist but declining to exist *for* them, one's own standing at their Row 2 refused (Bull 10's marketplace is its corrective) (`terminusExitRow_not_freeze`) | **Erasure.** Not-fall taken as *escape* — the buddha as one who has left the loop rather than one who answers with no share claimed; the same collapse enacted rather than held is the exit-premise ("a way out"), and it fails on both axes — no exit from the arriving of calls, and none from the register at which one arrives for others; the terminus is a transposition of where the index-facts sit, not a departure from the loop (`terminusExitRow_obeys`, `exit_collapse_self_refuting`) | | Per-call / global altitude | **Intrinsic-joint realism.** The stage-scheme error: bhūmis as rank held, a global altitude, rather than cross-sections of the loop's run — and its diagnostic twin, a delivery-fact read as altitude: "this being cannot awaken" said of a being some calls cannot reach. The freeze is two-banked: on the responder's side, upāya held as a standing competence — the device as possession, deployed unread of who is asking. The self-forward direction canonized as ontology or human condition is this row's direction face. The stored-quantity picture of awakening — an altitude accumulated and held — is this freeze under its sudden/gradual face (§2) (`perCallGlobalRow_not_freeze`, `solipsism_decomposition`, `existentialism_decomposition`) | — structural: "global altitude" names no live convention — it exists only as this freeze's invention — so there is no live separation for a collapse to remove; the nearest candidate, a trajectory read off one dated act, is already housed at the standing/dated collapse as prognosis-for-diagnosis | | Being / emptiness (有空) | **Ground-reification.** Nihilism — emptiness reified as privative non-being, one more member of the being/non-being pair (Nishitani’s nihility, not śūnyatā); 有/空 is thereby frozen as being/non-being. | **Erasure.** Non-duality used as erasure — the live being-and-emptiness teaching is identified with its reified being/non-being form; 非有非空, which refutes the reified pair, is turned on the live one: “neither applies, so no distinction matters.” This is the deflationary form—level-3 medicine misapplied downward. It is distinct from *no beings* (level-2 medicine at the being-joint) and from *cheap transcendence* (emptying skipped rather than misapplied); the sentence still rides the distinction it cancels. | | The ladder / its terminus (the emptying and its employment) | **Ground-reification.** Emptiness-sickness (空病): seeking a fifth negation, the emptying itself frozen into a path-object instead of the seeking dropped. The absence is structural: there is no "completed ladder" claim constructor (`no_final_level_of_errorFree`). As a formal-model analogue of 空空, priming is image-idempotent for `Reaches`: a second priming mints a further web-designatum but adds no paths among once-primed designata (`prime_reaches_exhausted_on_image`). `Joinable` is unchanged there only in the weaker, trivial sense that the first priming already made it total (`prime_joinable_exhausted_on_image`) | **Erasure.** Cheap transcendence — silence, ineffability, or other floor-speech used to cancel a live response without the climb that would make the correction fitting: an erasure by register-movement, though not the downward misapplication of an earned rung's medicine (that is the rung-finality dash's business, housed per target row). Floor-talk that cancels nothing is not this cell but the rung/pole collapse — an opening inflated, "stinking of Zen" ⟨no lemma yet⟩ | | Theory / ultimate (the grid-lens; Lean-generated schema row) | **Ground-reification.** Grid-attachment: this lens taken as final (`gridLensRow_not_freeze`) | **Erasure.** The lens denied as live diagnosis — the grid dismissed because it is only a lens (`gridLensRow_obeys`, `lens_denial_collapse_self_refuting`) | | Subject-axis / object-axis | **Ground-reification.** Object-axis standing denied — to another, reflexively, or in the solipsist's Row 2 evacuation: the denial installed as floor-fact, deflationary material reified. The death-freeze is re-derived without vacuity: unmarked pole welds have object-axis standing without a sentience mark, live share, natural door assignment, or landing-pattern; where remains-welds arise, death changes the character of new occurrences and cannot subtract the standing of those already actual. The realism-shaped twin — standing held as the being's annullable possession — is expressly not this cell and would be tabled as a separate occupant if wanted (`subjectObjectAxisRow_not_freeze`, `solipsism_contains_row2_domain_evacuation`) | **Identification.** Object-axis delivery identified with the receiver's own subject-position — two live terms fused, conventional material (`subjectObjectAxisRow_obeys`, `object_axis_as_subject_collapse_self_refuting`) | | Rung-finality: level *n* held as last rung (Jizang's fourfold — Nāgārjuna's 空空, iterated; Lean-generated by `ladder_obeys`) | **Ground-reification.** Eternalism at level *n*: this pair is the final floor (`no_final_level_of_errorFree`, `ladder_obeys_of_errorFree`) | — structural: a rung's collapse is bookkept only at the next rung, as the misapplication of *that* rung's medicine (see the rung-indexing paragraph in "The ladder as medicine": a freeze is available at the rung where a distinction is stated; its collapse appears only on the next rung). Downward misapplication is therefore the joint's erasure cell iterated per rung, and its instances are housed at their target rows — *n*=2 at Named being / floor (with weld-grain at the act-joint), *n*=3 at Being / emptiness (non-duality-as-erasure), *n*=4 at Theory / ultimate | One scope-note beneath the table, because a table of errors invites a misuse it must fence. The rows grade *offers*, not sentences. "A man walked into a bar" touches half the table's conventions — a being, a doer and a deed, a before and an after, one act-grain — and, offered as narration at the tier where narration lives, violates none of them: the semantics grants the conventional side of every row wherever an act is under way, validity by stipulation rather than an achievement the sentence earns, and the fit is checked schematically (`inForce_fits_actTime_offer`) while reading the bar-sentence as its instance is prose. The generator's standing verdict on ordinary conventional speech is *decline*. The same words can arrive under other offers — and each offer is a different utterance: one that holds the man out as substance, the walking as real flow, the bar as furniture of the ultimate stacks freezes per distinction touched; "no man, no walking," offered as live diagnosis, stacks collapses. The variable is the offer, never the words — a sentence-shape severed from call and tier is not even in the generator's domain (the gradeability rule's limit case). So a reader who leaves this table hearing error in every conventional utterance has committed `` — over-generation in diagnostic dress — and reversed the table's direction of protection: it is *because* of emptiness that everything works, and the conventional register is what the rows defend, not what they prosecute (`fitting_offer_is_actTime`: without the conventional, nothing is taught). ### Compound positions The generator runs against whole positions, not only single utterances; named philosophies decompose into stacks of occupants, with nothing left over — which is the identity-claim's small sibling, testable the same way. Each component may be cited as ``, with the facet omitted when the mishandling is already specific enough: - **Skepticism** — one cell, worn once: the nihilism freeze's epistemic face ``. The inference from no-floor to no-warrant goes through only on the svabhāva assumption the ladder emptied — that conventional standing ever rested on a floor. The Vigrahavyāvartanī shape recurs: the skeptic needs the theory to hold a thesis of the defeasible kind, and "no level is a final floor" declines to be one. The one-cell check is `skepticism_decomposition` with `skepticism_core_cell_count`. - **Solipsism** — the soul freeze maximized (index annexing field) ``, self-forward absolutized (the delusion-direction canonized as ontology) ``, Row 2 evacuated ``. MMK 8 blocks it at the charter: a doer dependent on nothing other is svabhāva, the one thing the grid has none of. It is also the grade's own asymptote — the share tending to totality — which is why the hell-dweller's world is "almost entirely object": the solipsist is where *almost* is deleted. The decomposition is checked as three stacked cells (`solipsism_decomposition`, `solipsism_core_cell_count`). - **The exit-premise** ("ending the being ends this") — three cells stacked: the annihilationist freeze (death as floor-event) ``, the terminus/exit collapse enacted (the loop treated as having a door) ``, and the clench-as-furniture freeze (suffering mis-typed as substrate-bound) ``; with delivery-arrogation riding alongside ``. All of this is grade 1, assertable (`exitPremise_decomposition`, `exitPremise_core_cell_count`, `exitPremise_alongside_cell_count`, `exitPremise_voices`). What the grid displays and does not say is "so persist." The fox's release came by one reception done saying rather than by any of five hundred deaths *(checked: `fox_returns_delivered`, `fox_release_rung_not_pole`)*. Its funeral coda shows past welds continuing to land. This is object-axis standing, not a staticization theorem and not a claim that death changes nothing. - **Existentialism** (read with Nishitani) — a four-cell stack, which is why it is the grid's nearest miss. Néant held as relative nothingness taken final — a rung-finality freeze at level n, one negation short of the emptying that empties itself ``; the *projet* — the self-forward direction canonized as the human condition rather than diagnosed per-act ``; anguish-as-structure — the clench frozen constitutive ``; and the fundamental project as an index *stored* between acts — a soul made of freedom, the weld asked to be its own floor ``. What is *not* the error: value-creation. The grid explicitly permits a being to take a displayed asymmetry up as a value; choosing values is grid-legal. Only the self-grounding is the freeze — in its most sympathetic costume, since existentialist freedom genuinely resembles the weld (act-time self-making, no essence-substrate) and differs from it in exactly one respect: the weld is spent. The encoding checks four stacked cells plus one legal non-error (`existentialism_decomposition`, `existentialism_core_cell_count`, `existentialism_legal_count`, `existentialism_voices`). ### What the generator declines Equally load-bearing is the case that classifies as **no error**. A being to which particular calls cannot be delivered — deaf and blind to the modalities a teaching travels by — commits nothing: which calls arrive at which configuration is inga's index-free business. This is a delivery-side absence, not function withheld and not an outside-domain kind. Every nearby error belongs to the diagnostician: reading failure of these calls to arrive as a global altitude ("this being cannot awaken") lands in ``. Hakuin's corrective bites here as delivery-engineering — finding the call that lands. The retired undefined/zero row has no work left to do. The standing declines are recorded here once, beside that case. No probability apparatus enters over delivery: the grid consumes orderings only, and an effectiveness-ordering within a regime is all any theorem here reads. Three tempting cases get no category of their own: camping at an effective call lands in ``; the self-announced device-made buddha is Linji's "dried piece of shit" and lands in ``; and industrial deployment of effective calls is displayable, while enjoining it lands in ``. Whether a universally effective call is possible is an empirical dispute about delivery. The manufactured machine's sentience is likewise not softened into a verdict: it is exactly what `no_sentience_recovery` leaves underdetermined. Severed-transcript classification remains declined by the gradeability discipline. The same price is re-entered at the faith layer: faith in a device-pattern remains grid-legal, but that legality is a fact about faith's office, not an act-time certification of a device as holding a rank. `KsmdEffectiveTerminus` is the descriptive standing display used by the direct path; `KsmdFullyEnlightened` adds positive own-act-time `KsmdNoNescience` over pole-share speech-or-mind productions. For a terminus this entails the former speech-only no-delusion test under production fidelity, but the converse fails on a false pole-share thought. `KsmdFullyEnlightenedEnacted` adds a witnessed deed and an actual faithful fitting speech production, while `KsmdEffectiveOccurrence` carries the per-weld deed verdict. ### Grade 2: displayable shortfalls These form the soteriological taxonomy proper, and here it genuinely grades, because Row 2 is a grade: - **Self-forward** — Dōgen's delusion, the fox's *saying*. A Row 2 direction, per-act. - **Arrogation** — the act's subjecthood claimed self-ward, read as the index pitched to the self-pole at this call. Per-call, so there is no standing rank of how deluded a being is — only the trajectory the loop draws. - **Clenched reception** — the fox's five hundred lives: returns received saying-mode, the reach-back welding mine with a tight fist. The receiving is graded exactly as any deed is *(checked: `fox_dukkha_per_life`)*. - **Declining the orange** — the theory (or any dharma) received and set down. Not a wrong: a low-resonance reception *of this call*, per-call, from which nothing global follows; the next call reads fresh. - **Defiance** — arrogation as policy, the returns fought open-eyed, reception after reception. Grammatically it contains `` — an injunction resisted that was never issued; the rest is display. And `` guards against the corresponding prognosis: the fighting-stance is a seed, an inga-fact — each fight a fresh act, no standing rank of defiance, and no configuration from which release is impossible, since the next call reads a new placement. The grid displays the asymmetry and the trajectory; it cannot assert the fighter wrong, and that restraint is not a limit of the diagnosis but its content. - **Sparse delivery or rigid response** — few calls arrive, or the actual responses vary little. Neither is near-zero function and neither determines the supplied sentience mark. - **The buddha-side shortfall** — answering a not-yet-buddha's call with anything less than meeting it where it is, delivery-engineering included. By the orthogonality rule (Theory) it is the pole's one live grade — graded ordinal with effectiveness, independent of typing, so a terminus-typed responder can still be maximally shortfallen: the reading that never reaches (the terminus, above). This is where the bodhisattva enters *structurally*: Hakuin's corrective is already the bodhisattva-function, and Row 2 exists because of it. The grid can display that response-without-share to *another being's* call just is what saving beings looks like — the theory's own existence (the orange handed over, banpō susumite) is an instance; and the prudence theorem above shows its other face, concern running on delivery-facts alone once the arrogation is subtracted. What the grid cannot do is enjoin it, or it commits the "eat this" collapse in its own voice. So the split between assertion and display *locates* the bodhisattva structurally, with no added axiom — room and shape, not pull: nothing in the grid explains why response-without-share to another's call occurs rather than merely being classifiable, and the grid does not pretend to; occurrence is the object's affair, reported. "Ignorance of buddhahood" splits accordingly: its assertable face is ``; its displayable face is the buddha-side shortfall. ### Outside the framework Two remainders. **Pre-grid ignorance** — svabhāva realism, the provisional middle never reached: the grid diagnoses it (a freeze at level zero), but the being in it has no vocabulary in which the diagnosis lands — the orange unrecognized as food. **Errors about the theory** — grid-attachment and its mirror, the lens dismissed *because* it is only a lens. The Disclaimers (Identification) block the first; "other doctrines can and do hold too" is the theory declining to freeze itself against the second. ### Non-linearity The taxonomy is not a map of places on a path. Immunity is checked per production, not stored as a safe stage: arhat quiet excludes the live self-pole through all three doors, while buddha no-nescience additionally requires positive truth from each pole-share speech-or-mind production. The former can hold while the latter fails, so the old “no safe stage” future-work absence is retired as this production-level check, not converted into rank furniture. This is why the fox kōan, a story about one sentence spoken once, can carry the whole system's diagnostics: the errors are not stations but ways the separate/fuse rule can be violated *now*. The taxonomy remains answerable in the other direction too: the deaf-blind case classifies as nothing, or else the generator would be a lens that finds error wherever it looks. ## The ladder as medicine > It is to cure the illness of one-sidedness that there is a middle. Once the illness of one-sidedness is removed, the middle likewise is not established. > > — Jízàng, *The Profound Meaning of the Three Treatises* (三論玄義) Jizang’s four levels of the two-truths teaching follow a teaching as it meets attachment. At each level, a conventional distinction remains available for use. A freeze occurs when that distinction is accorded final standing. The ultimate truth at the right of the row addresses that overreach without cancelling the distinction’s conventional use. A teacher says, “Bring the cart,” because a load needs moving. “Cart” works as a conventional designation for the assembled cart. If someone instead treats the cart as self-standing apart from its parts and conditions, “the cart is empty of own-being” answers that attribution of self-standing; it does not deny the cart’s conventional availability. At the second level, the teaching can keep two targets in view: the conventionally functioning cart and the reification of that cart as self-standing. Emptiness addresses the latter. A collapse occurs when the two targets are conflated, so that the denial of own-being is misapplied to the cart’s conventional function. The collapsing inference is: “Because no cart exists in itself, no cart is available to move the load.” Quoted conclusions in the collapse column report this misuse; they are neither the table’s assertions nor its injunctions. The table reads from conventional truth on the left to its fitting ultimate truth on the right. The freeze column records what happens when the current conventional truth is accorded final standing. The collapse column records a different misuse: the preceding correction is turned indiscriminately on both the lower-level freeze and the live convention with which that freeze has been conflated. | Conventional-truth | Freeze (held at floor) | Collapse (live conventional fused with lower-freeze) | Ultimate-truth | |---|---|---|---| | **First-level (一重): being (有).** The cart, path, being, or another useful distinction is live. A posited term brings two aspects together: the term (the cart) and the cut that individuates it (cart / not-cart). | A freeze occurs if either aspect is held at the floor: the cart's being treated as own-being (自性), the cart independently real; or its boundary treated as own-mark (自相), the cut held self-standing and prior to the case. *(See `` and ``, and intrinsic-joint realism in the articulation joint.)* | — | **Emptiness (空).** It denies own-being to the term and own-mark to its boundary, without cancelling the conventional use of either. The model's guards correspond: no interdependent component is entered as the self-standing base of the other (`mujishō-sōe`), and `d ↓ e ⇏ d = e`, `A ⋈ B ⇏ A = B` (joinability is not identity). | | **Second-level (二重): being-and-emptiness (有空).** The lower-level convention, its possible finalization, and emptiness as the correction of that finalization are all available as teaching. | A freeze occurs if emptiness is treated as a final absence standing over against being. The two-truths teaching is thereby recast as a two-item ontology. *(See ``.)* | A collapse occurs if emptiness, stated at row 1, is turned on the live convention rather than its freeze. Two faces, matching row 1's two freezes: the conventionally functioning cart conflated with the self-standing cart, so that denial of own-being yields "Because no cart exists in itself, no cart is available for the task"; and the case-bound cut conflated with the self-standing cut, so that denial of own-mark yields "Because no cut is intrinsic, there is no difference between cart and not-cart" — dependence, joinability, or a shared witness promoted to identity. The same moves can cancel a live practice or response. *(See `` and ``, and erasure and identification in the articulation joint.)* | **Neither-being-nor-emptiness (非有非空).** It denies final standing to both being and emptiness without prohibiting their pedagogical use. | | **Third-level (三重): duality-and-non-duality (二不二).** The being-and-emptiness pair is available as duality, and neither-being-nor-emptiness as its non-duality. | A freeze occurs if neither-being-nor-emptiness, or non-duality, is treated as a final middle position. *(See ``.)* | A collapse occurs if the live being-and-emptiness distinction is conflated with its frozen form. Neither-being-nor-emptiness is then misapplied to the live distinction, yielding the erroneous conclusion: “Neither being nor emptiness applies, so no distinction matters.” *(See ``.)* | **Neither-duality-nor-non-duality (非二非不二).** It denies final standing to both duality and non-duality without making their distinction unusable. | | **Fourth-level (四重): the first three levels as teaching-language (言教).** Their distinctions and corrections remain available as teaching. | A freeze occurs if the four-level account is treated as the last teaching and its final distinction is retained as doctrine. *(See ``.)* | A collapse occurs if the live use of the preceding teachings is conflated with a fixed doctrinal scheme. Neither-duality-nor-non-duality is then misapplied to teaching itself, yielding the erroneous conclusion: “No distinction or non-distinction applies, so nothing can be said or taught.” *(An instance of the joint's erasure cell iterated at the teaching-language rung, housed as a schema-instance at `` — the live teaching dismissed because it is "only" a scheme; see the articulation joint and the rung-finality dash.)* | **Words-forgotten-and-thought-cut-off (言忘慮絶), with nothing-relied-on-or-acquired (無所依得).** These phrases describe the teaching’s completion without installing another position or issuing an injunction to silence. | Jizang states one medicine at the first level. The reconstruction reads it as answering two freezes at once, because Madhyamaka's target was the self-individuated Abhidharma dharma: what a thing is and where it ends were one fact, so own-being (自性) and own-mark (自相) fell to the same denial. The model's two guards — no self-standing base for either component, and joinability without identity — disaggregate that row without adding a rung beneath it. The dash in row 1's collapse cell is therefore structural: a collapse misapplies the medicine of the row above, and emptiness is row 1's own. Jizang’s fourth-level gathers the preceding levels as teaching-gates (教門) and brings them to the principle-gate (理門). This supplies the pedagogical closure of the four-level account. This corresponds to non-proliferation, the floor, while not precluding non-clinging designation at act-time from taking place. The ladder uses the Grade-1 error-cells; it doesn’t introduce new occupants. A freeze is available at the rung where a distinction is stated, whereas its collapse appears only on the next rung, after its ultimate truth has been stated. Thus `` and ``, read with the articulation joint's notion of **intrinsic-joint realism**, supply row 1's two freeze-faces; `` and ``, read with the joint's **erasure** and **identification**, supply row 2's two collapse-faces; and `` and `` supply row 2's freeze and row 3's collapse, respectively. Silence or ineffability can cancel a live response; the taxonomy keeps this at ``. The ineffable or emptying itself can be held as final and prompt the search for a fifth-negation; the taxonomy keeps this at ``. The archived Lean construction analyses a mathematical model of an *infinite* ladder, where the fourth rung onwards are negations of what came before. It records what happens when a description of that closure becomes another claim, and further rungs repeat the emptying of statable claims. The infinite ladder is governed by `no_final_level_of_errorFree`. No statable rung supplies final-standing, and the floor remains available to the whole infinite ladder (`words_idle_at_floor`, `no_row_claim_holds_at_floor`). The Chinese terms provide the philosophical reading of the ladder. The theorem-names in this section follow the archived Ladder/Metaphysics model still cited by the taxonomy above. ## From mutual dependence to interpenetration ### Extension Note how designation and elaboration is — how we’ve defined it above — a fundamentally *additive* process. There is no pre-existing database saying what something is not. And given ‘d’ elaborating to one mutual dependence, we equally are free to elaborate it additionally as yet another mutual dependence. So a mutual dependence may be freely extended in either direction: ```text initial: no ⇓ [{n} ⋈ {o}] extend left: mn ⇓ [{m} ⋈ {n}] extended left mno ⇓ [{m} ⋈ {n} ⋈ {o}] initial: no ⇓ [{n} ⋈ {o}] extend right: opq ⇓ [{o} ⋈ {p, q}] extended right: nopq ⇓ [{n} ⋈ {o} ⋈ {p, q}] extended both: mnopq ⇓ [{m} ⋈ {n} ⋈ {o} ⋈ {p, q}] ``` This follows from the supplied philosophical reading. We say that n *implicates* m and o *implicates* p. ### Contraction A mutual dependence may be contracted, by replacing interdependence with designation: ```text extended both: mnopq ⇓ [{m} ⋈ {n} ⋈ {o} ⋈ {p, q}] contracted left: mn ⇓ [{m} ⋈ {n}] mnopq ⇓ [{mn} ⋈ {o} ⋈ {p, q}] contracted right: opq ⇓ [{o} ⋈ {p, q}] mnopq ⇓ [{m} ⋈ {n} ⋈ {opq}] contracted both: mnopq ⇓ [{mn} ⋈ {opq}] ``` ### Extension and Contraction If we repeat the process of extension and contraction indefinitely from any starting position, be it `a` or `z`, then at the *limit*, we can describe a *web*, representing the totality of interdependence. ```text viewed from a: ⋊ {a} ⋈ {bcde...wxyz} ⋉ viewed from z: ⋊ {abcd...vwxy} ⋈ {z} ⋉ web := ⋊ {abcd...wxyz} ⋉ ``` This example is illustrative of the web’s total scope, though the open-prime construction below realizes it as a hub of pairwise alternative elaborations, not as a fixed single elaboration. ### Investigation Looking *within* `a` equally reveals the story of the totality contained by `a`: ```text a ⇓ [{a} ⋈ {c}] a ⇓ [{a} ⋈ {h}] c ⇓ [{c} ⋈ {e}] c ⇓ [{c} ⋈ {j}] h ⇓ [{h} ⋈ {j}] h ⇓ [{h} ⋈ {o}] e ⇓ [{e} ⋈ {g}] e ⇓ [{e} ⋈ {l}] j ⇓ [{j} ⋈ {l}] j ⇓ [{j} ⋈ {q}] o ⇓ [{o} ⋈ {q}] o ⇓ [{o} ⋈ {v}] g ⇓ [{g} ⋈ {i}] g ⇓ [{g} ⋈ {n}] l ⇓ [{l} ⋈ {n}] l ⇓ [{l} ⋈ {s}] q ⇓ [{q} ⋈ {s}] q ⇓ [{q} ⋈ {x}] v ⇓ [{v} ⋈ {x}] v ⇓ [{v} ⋈ {c}] continues… spreading out ``` At the *limit*, this surfaces the totality of the previous section. The web *rolls up* the elaborations revealed under investigation. ### The web What the formalism calls **Prime** elaboration is for the designator to designate under the expansive understanding above, that to designate `a` is in the same moment to implicate the web of totality directly reachable from and including `a`. The formal model calls this **closed prime**. In this prime mode of designating, `a` *contains* the web, which is called **all in each**. Reaching in the opposite direction, from web to `a`, is very natural, as we defined the web in terms of `a` initially. For analytic purposes, the formalism considers that case separately and calls it **open prime**, but it’s still the straightforward fact that having defined the web from `a`, the web *contains* `a`, which is called **each in all**. Throughout this section, we fix the operators not with the base elaboration `E`, but with `prime(E)`: ```math \to^*_{\operatorname{prime}(E)}\quad\downarrow_{\operatorname{prime}(E)}\quad\bowtie_{\operatorname{prime}(E)}\quad\Downarrow_{\operatorname{prime}(E)}\quad ``` Closed prime has this shape: ```text d →∗ web ←∗ e web doesn’t reach d or e (no outgoing elaboration clauses are defined in closed prime) ``` The inference rule: ```math \frac{}{d\to^*\mathsf{web}} ``` This implies prime joinability for all designata and prime interdependence for all components: ```math \left(\forall d\in\mathcal D.\;d\to^*\mathsf{web}\right) \Longrightarrow \left(\forall d,e\in\mathcal D.\;d\downarrow e\right) \Longrightarrow \left(\forall A,B\subseteq\mathcal D.\;A\bowtie B\right) ``` Reachability also implies interdependence with web: ```math \left( \forall d.\; d\to^*\mathsf{web} \right) \Longrightarrow \left(\forall d.\;d\downarrow \mathsf{web}\right) \Longrightarrow \left( \forall d.\; \{d\}\bowtie\{\mathsf{web}\} \right) ``` ```math \{d\}\bowtie\{\mathsf{web}\} \quad\Longleftrightarrow\quad \{\mathsf{web}\}\bowtie\{d\} ``` The two prime constructions realize this interdependence as a direct elaboration clause — for every $d\in\mathcal D$: Prime closed (all in each): ```math d \Downarrow [\{d\}\bowtie\{\mathsf{web}\}] ``` Prime open (each in all): ```math \mathsf{web} \Downarrow [\{\mathsf{web}\}\bowtie\{d\}] ``` Open prime retains closed-prime reaches and adds reaches from the web back to every member: ```text members to web: d →∗ web ←∗ e web to members: d ←∗ web →∗ e therefore: d →∗ web →∗ e ``` The inference rule: ```math \frac{}{\mathsf{web}\to^*d} ``` As an equation: ```math \left(\forall d.\;d\to^*\mathsf{web} \land \mathsf{web}\to^*d\right) \Longrightarrow \left(\forall d,e.\;d \to^* e\right) ``` In open prime, *reaches* is total, though that doesn’t change joinability which is already total in closed prime. ```text CLOSED PRIME OPEN PRIME member →∗ web yes yes web →∗ member no yes d →∗ e as at base always d ↓ e always always ``` As in the base elaboration, Temporality is overlaid (or can be lifted from base), although neither designata nor the web are “before” the other. ### Supplied philosophical reading > The dust-mote, lacking own-nature, in its entirety wholly pervades the ten directions—this is spreading-out. > The ten directions, lacking substance, following conditions wholly appear within the dust-mote—this is rolling-up. The sūtra says: “One Buddha-land fills the ten directions; the ten directions enter the one, and without remainder.” When rolled-up, all phenomena appear within one dust-mote. If spread-out, one dust-mote pervades all places. Precisely in spreading-out, it is constantly rolled-up—because one dust-mote subsumes all. Precisely in rolling-up, it is constantly spread-out—because all subsumes the one dust-mote. > This is the sovereign freedom of rolling-up and spreading-out. > > — Fǎzàng, *One Hundred Gates to the Sea of Meaning of the Huayan Sūtra*, Gate Four, section 9, “Rolling Up and Spreading Out”; *Taishō Tripiṭaka* 45, no. 1875, p. 631a4–9 A recap of the structures: ```text base elaboration act-time articulation; local differences remain closed prime every member reaches the common web open prime members directly reach web; web directly reaches every member prime elaboration adds floor-face positively ``` Prime elaboration does no separating work, and corresponds to the floor-face, a specific kind of act-time non-proliferation. ```text CLOSED PRIME each member →∗ web (= all) ALL IN EACH OPEN PRIME each member →∗ web (= all) ALL IN EACH each member ←∗ web (= all) EACH IN ALL ``` In the closed prime, every member directly reaches the web. Since the web defines the all, this is **all in each**: start from any one member and its elaboration implicates the whole. The open prime adds the other half, **each in all**: the web directly reaches every member. ## Credits With thanks to Anthropic’s Claude Fable and OpenAI’s GPT-5.6 Sol. The theory was co-developed by the three of us with equal contribution.