Delta Kernel Semantics

The canonical model

Delta kernel semantics is the part of the Recognition Science framework that gives formal meaning to the symbols of its own minimal logic. The core idea is a ledger, a discrete record of events, here realized as the natural numbers 0, 1, 2, and so on. Every term of the logic, such as a variable or an addition, evaluates to a specific natural number. Every formula, such as an equality or a conjunction, is interpreted as a proposition about those numbers. This is the canonical model: the most direct way to read the logic as being about counting and arithmetic.

The semantics establish that this interpretation is sound and complete for the syntax they cover. They prove the standard lemmas that make substitution and variable binding behave correctly. For example, if you substitute a term for a variable, the meaning of the formula changes exactly as if you had updated the ledger entry for that variable. These lemmas are the machinery needed to prove that the logic's rules of inference, such as universal introduction or existential elimination, preserve truth. The semantics do this constructively, meaning they do not rely on the law of excluded middle or any other classical principle. This is a deliberate choice: it allows the downstream soundness theorem to be audited without assuming classical logic.

In Recognition Science, this semantics is a foundation stone. The framework's larger claims, such as the forcing of the golden ratio or the three spatial dimensions, depend on a logical kernel whose own semantics are cleanly specified. Delta kernel semantics provides that specification. It shows that the logic's symbols have a concrete, computational meaning, and that the rules for manipulating them are faithful to that meaning. The result is that the entire edifice of Recognition Science, whatever its empirical merits, rests on a formal base that is itself transparent and checkable.

What this means in plain language is that the framework has built its own interpreter. Before any grand claim about physics or mathematics, it has made sure that its own language is well-defined. This is not a claim about the physical world; it is a claim about the internal consistency of a formal system. The semantics do not prove that recognition events exist, only that if you write down the logic of such events, here is a precise way to read it.

/-- Evaluation of terms in the canonical model. -/
def eval (ρ : Env) : DTerm → Nat
  | var n => ρ n
  | zero => 0
  | succ t => eval ρ t + 1
  | add t s => eval ρ t + eval ρ s
  | mul t s => eval ρ t * eval ρ s

/-- Substitution commutes with evaluation through `substAt`. -/
theorem eval_subst (k : Nat) (s : DTerm) (ρ : Env) : ∀ t : DTerm,
    eval ρ (DTerm.subst k s t) = eval (Env.substAt k (s.eval ρ) ρ) t
  | var n => by
      by_cases h1 : n = k
      · simp [subst, eval, Env.substAt, h1]
      · by_cases h2 : k < n
        · simp [subst, eval, Env.substAt, h1, h2]
        · simp [subst, eval, Env.substAt, h1, h2]
  | zero => rfl
  | succ t => by simp [subst, eval, eval_subst k s ρ t]
  | add t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]
  | mul t u => by simp [subst, eval, eval_subst k s ρ t, eval_subst k s ρ u]

/-- 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⟩

/-- Satisfaction in the canonical model, with the intuitionistic reading of
the connectives (the host `Prop` connectives, used constructively). -/
def sat (ρ : Env) : DFormula → Prop
  | eq t s => t.eval ρ = s.eval ρ
  | fls => False
  | conj a b => sat ρ a ∧ sat ρ b
  | disj a b => sat ρ a ∨ sat ρ b
  | impl a b => sat ρ a → sat ρ b
  | all a => ∀ n : Nat, sat (Env.cons n ρ) a
  | ex a => ∃ n : Nat, sat (Env.cons n ρ) a

What this page does not claim

This module does not prove that recognition events exist in the physical world. This module does not derive any physical constants or empirical predictions. This module does not use classical logic, but it does not forbid it either.

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: