Encyclopedia Delta Delta Kernel Semantics Subst At Cons

ARTICLE 3 claims 3 theorems

Delta Kernel Semantics Subst At Cons

A small formal lemma about bookkeeping with variable names, and why it matters for a machine-checked proof of soundness.

Verify this page

Substitution under a binder

In formal logic, a binder is a construct that introduces a new name, like the x in "for all x" or the n in "there exists n". When a proof manipulates formulas, it often needs to replace one name with another, and it must do so without accidentally capturing a name that was supposed to stay free. The declaration substAt_cons in the framework's machine-checked library of formal theorems is a bookkeeping lemma that states a precise fact about this replacement process: substituting at a shifted position in an environment that has a new entry at the front is the same as first adding the new entry and then substituting at the original position.

To see what this means, think of an environment as a list of values, one for each variable in scope. The operation substAt k v ρ replaces the value at position k with v, and shifts the values above k down by one to close the gap. The lemma says that if you have already added a new value w at the front of the list, then substituting at position k+1 in that longer list gives the same result as substituting at position k in the original list and then adding w at the front. In symbols: substAt (k+1) v (cons w ρ) n = cons w (substAt k v ρ) n for every position n.

This fact is not deep mathematics, but it is exactly the kind of detail that a machine-checked proof of soundness must get right. The lemma is proved constructively, meaning it does not rely on classical logic. That matters because the framework's soundness theorem, which states that the formal system's rules are consistent with its semantics, is itself axiom-audited as choice-free. The lemma is one of several commutation facts that the soundness proof needs when it handles the rules for introducing and eliminating quantifiers.

In Recognition Science, this lemma is part of the kernel's own self-examination. The framework models recognition events as a ledger, a discrete record of distinctions, and the kernel is the part of the framework that checks its own reasoning. The lemma does not claim anything about the physical world. It does not derive a constant, force a dimension, or predict a measurement. It is a purely syntactic and semantic fact about the framework's internal language, a small but necessary step in showing that the framework's logic is sound.

What the lemma does not claim is also clear. It does not say that substitution is always safe in every context; it only covers the specific case of a binder at the front of an environment. It does not prove that the framework's logic is complete, only that it is sound. And it does not establish any connection between the framework's formal system and any physical theory; that connection is made by other parts of the framework, not by this lemma.

THEOREM substAt_cons · IndisputableMonolith/DeltaKernel/Semantics.lean
substAt_cons · IndisputableMonolith/DeltaKernel/Semantics.lean:59 
/-- `substAt` commutes with `cons` at a shifted index, pointwise. This is
the binder case of the substitution lemma. -/
theorem substAt_cons (k v w : Nat) (ρ : Env) :
    ∀ n, substAt (k + 1) v (cons w ρ) n = cons w (substAt k v ρ) n := by
  intro n
  cases n with
  | zero =>
      show (if 0 = k + 1 then v
            else if k + 1 < 0 then cons w ρ (0 - 1) else cons w ρ 0) = w
      have h1 : ¬ (0 = k + 1) := by omega
      have h2 : ¬ (k + 1 < 0) := by omega
      rw [if_neg h1, if_neg h2]
      rfl
  | succ m =>
      show (if m + 1 = k + 1 then v
            else if k + 1 < m + 1 then cons w ρ (m + 1 - 1) else cons w ρ (m + 1))
          = (if m = k then v else if k < m then ρ (m - 1) else ρ m)
      cases Nat.decEq m k with
      | isTrue h =>
          have h1 : m + 1 = k + 1 := by omega
          rw [if_pos h1, if_pos h]
      | isFalse h =>
          have h1 : ¬ (m + 1 = k + 1) := by omega
          rw [if_neg h1, if_neg h]
          cases Nat.decLt k m with
          | isTrue h2 =>
              have h3 : k + 1 < m + 1 := by omega
              rw [if_pos h3, if_pos h2]
              obtain ⟨j, rfl⟩ : ∃ j, m = j + 1 := ⟨m - 1, by omega⟩
              rfl
          | isFalse h2 =>
              have h3 : ¬ (k + 1 < m + 1) := by omega
              rw [if_neg h3, if_neg h2]
              rfl
THEOREM substAt_cons · IndisputableMonolith/DeltaKernel/Semantics.lean
substAt_cons · IndisputableMonolith/DeltaKernel/Semantics.lean:59 
/-- `substAt` commutes with `cons` at a shifted index, pointwise. This is
the binder case of the substitution lemma. -/
theorem substAt_cons (k v w : Nat) (ρ : Env) :
    ∀ n, substAt (k + 1) v (cons w ρ) n = cons w (substAt k v ρ) n := by
  intro n
  cases n with
  | zero =>
      show (if 0 = k + 1 then v
            else if k + 1 < 0 then cons w ρ (0 - 1) else cons w ρ 0) = w
      have h1 : ¬ (0 = k + 1) := by omega
      have h2 : ¬ (k + 1 < 0) := by omega
      rw [if_neg h1, if_neg h2]
      rfl
  | succ m =>
      show (if m + 1 = k + 1 then v
            else if k + 1 < m + 1 then cons w ρ (m + 1 - 1) else cons w ρ (m + 1))
          = (if m = k then v else if k < m then ρ (m - 1) else ρ m)
      cases Nat.decEq m k with
      | isTrue h =>
          have h1 : m + 1 = k + 1 := by omega
          rw [if_pos h1, if_pos h]
      | isFalse h =>
          have h1 : ¬ (m + 1 = k + 1) := by omega
          rw [if_neg h1, if_neg h]
          cases Nat.decLt k m with
          | isTrue h2 =>
              have h3 : k + 1 < m + 1 := by omega
              rw [if_pos h3, if_pos h2]
              obtain ⟨j, rfl⟩ : ∃ j, m = j + 1 := ⟨m - 1, by omega⟩
              rfl
          | isFalse h2 =>
              have h3 : ¬ (k + 1 < m + 1) := by omega
              rw [if_neg h3, if_neg h2]
              rfl
THEOREM sat_subst · IndisputableMonolith/DeltaKernel/Semantics.lean
sat_subst · IndisputableMonolith/DeltaKernel/Semantics.lean:248 
/-- Substitution commutes with satisfaction through `substAt`. -/
theorem sat_subst (φ : DFormula) : ∀ (k : Nat) (s : DTerm) (ρ : Env),
    sat ρ (φ.subst k s) ↔ sat (Env.substAt k (s.eval ρ) ρ) φ := by
  induction φ with
  | eq t u =>
      intro k s ρ
      simp [subst, sat, DTerm.eval_subst]
  | fls => intro k s ρ; exact Iff.rfl
  | conj a b iha ihb =>
      intro k s ρ
      simp only [subst, sat]
      exact and_congr (iha k s ρ) (ihb k s ρ)
  | disj a b iha ihb =>
      intro k s ρ
      simp only [subst, sat]
      exact or_congr (iha k s ρ) (ihb k s ρ)
  | impl a b iha ihb =>
      intro k s ρ
      simp only [subst, sat]
      exact imp_congr (iha k s ρ) (ihb k s ρ)
  | all a ih =>
      intro k s ρ
      simp only [subst, sat]
      have key : ∀ n : Nat,
          sat (Env.cons n ρ) (a.subst (k + 1) (s.lift 1 0)) ↔
          sat (Env.cons n (Env.substAt k (s.eval ρ) ρ)) a := by
        intro n
        have e1 : (s.lift 1 0).eval (Env.cons n ρ) = s.eval ρ := by
          rw [DTerm.eval_lift]
          exact DTerm.eval_ext (fun m => by simp) s
        rw [ih (k + 1) (s.lift 1 0) (Env.cons n ρ), e1]
        exact sat_ext a (Env.substAt_cons k (s.eval ρ) n ρ)
      constructor
      · intro h n; exact (key n).mp (h n)
      · intro h n; exact (key n).mpr (h n)
  | ex a ih =>
      intro k s ρ
      simp only [subst, sat]
      have key : ∀ n : Nat,
          sat (Env.cons n ρ) (a.subst (k + 1) (s.lift 1 0)) ↔
          sat (Env.cons n (Env.substAt k (s.eval ρ) ρ)) a := by
        intro n
        have e1 : (s.lift 1 0).eval (Env.cons n ρ) = s.eval ρ := by
          rw [DTerm.eval_lift]
          exact DTerm.eval_ext (fun m => by simp) s
        rw [ih (k + 1) (s.lift 1 0) (Env.cons n ρ), e1]
        exact sat_ext a (Env.substAt_cons k (s.eval ρ) n ρ)
      constructor
      · rintro ⟨n, hn⟩; exact ⟨n, (key n).mp hn⟩
      · rintro ⟨n, hn⟩; exact ⟨n, (key n).mpr hn⟩

What this page does not claim

The lemma does not claim that substitution is always safe in every context. The lemma does not prove that the framework's logic is complete. The lemma does not establish any connection between the framework's formal system and any physical theory.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/DeltaKernel/Semantics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND