6 Continuous Approximation and Representation Space

In this chapter, we bridge the discrete combinatory logic of the ISAR substrate with continuous analysis and matrix spaces. We formalize dimensional physical quantities, matrix representations, expressive completeness, the tensor semantics, and named analytic axioms for universal approximation. Unique addresses in a completion of KernelAddress remain axiomatic: there is no metric on KernelAddress.

6.1 Physical Quantities and Matrix Representations

We define dimensional quantities and 4x4 matrix algebra.

Definition 33 Quantities and Uncertainty

A quantity represents a physical parameter with:

A value (rational scalar).
A physical dimension (exponent exponents).
An epistemic uncertainty expression Uncertainty and Correlation.

Covariance propagation propagates exact metric-epistemic covariance equations under addition and multiplication.

Definition 34 Matrix4 Carriers

The concrete integer 4x4 matrix representation used for basis combinator signatures. The primitive matrices are:

\begin{gather*} I_1 = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 0 \end{pmatrix}, \quad R_1 = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \end{pmatrix}, \\ A_1 = \begin{pmatrix} 0 & 0 & 0 & 0 \\ 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 0 \end{pmatrix}, \quad S_1 = \begin{pmatrix} 1 & 1 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 1 \end{pmatrix}\end{gather*}

Theorem 15 Idempotency and Nilpotency

The identity matrix \(I_1\) is idempotent:

\[ I_1^2 = I_1 \]

The core rewrite operator \(K_1 = I_1 \cdot R_1 \cdot A_1 \cdot S_1\) is nilpotent:

\[ K_1^2 = \mathbf{0} \]

Theorem 16 Gauge Similarity

The two alternative matrix representations \(K_1\) and \(K_2\) are conjugate (similar) via the lower-triangular gauge transformation matrix \(P\):

\[ P \cdot K_1 \cdot P^{-1} = K_2 \]

proving that representation details are gauge shadows, while the terminal quotient state is invariant.

Definition 35 Matrix View Map

The structural homomorphism mapping each ISAR term to its concrete 4x4 integer matrix signature:

\[ \text{term\_ signature\_ val} : \text{ITerm} \to \text{Matrix4} \]

Theorem 17 Expressive Completeness

Every matrix generated by the basis combinator algebra is the image of some term:

\[ \forall M \in \text{ISKAlgebra}, \quad \exists t \in \text{ISKSubtype}, \quad \text{term\_ signature\_ val } t = M \]

6.2 The Categorical Matrix Bridge

We package the matrix representations as an admissible semantic kernel.

Definition 36 Matrix Kernel

The semantic kernel MatrixKernel whose carrier is Matrix4 and whose view map is term_signature_val.

Theorem 18 Nilpotent Collapse

Applying konst to itself maps to the zero matrix, showing the nilpotent collapse of the basis algebra:

\[ \text{kernelMatrixView}(\mathbf{K}\ \mathbf{K}) = \mathbf{0} \]

Theorem 19 Matrix Terminality

Every structure-preserving morphism from MatrixKernel to ISAR_Kernel is observationally equivalent to the canonical decoding morphism.

Theorem 20 Unreachability of R and A

The structural homomorphism kernelMatrixView never produces the rotation matrix \(R_1\) or adjacency matrix \(A_1\) from a pure ISK term.

6.3 Tensor Denotation Semantics

We bridge the discrete combinatory logic of the ISAR substrate with continuous analysis and matrix spaces by formalizing the denotational mapping of symbolic ISAR terms into an abstract rank-4 tensor space, where reductions map to extensional equality.

Definition 37 Tensor Space Primitives

The abstract tensor space \(\mathcal{T}\) is characterized by five primitive operators:

Identity: t_norm
Constant: t_konst
Duplicator: t_dup
Swapper: t_swap
Composition: t_comp

Definition 38 Derived S in Tensor Space

The distributive combinator \(\mathbf{S}\) in the tensor space is constructively derived using swapper, composition, and duplicator operators:

\begin{align*} \text{t\_ s}_{\text{s}} & \triangleq \text{t\_ app}\Big(\text{t\_ app}\big(\text{t\_ comp}, \text{t\_ app}(\text{t\_ comp}, \text{t\_ dup})\big), \\ & \quad \text{t\_ app}\big(\text{t\_ app}(\text{t\_ swap}, P), \text{t\_ norm}\big)\Big) \end{align*}

where:

\[ P \triangleq \text{t\_ app}\big(\text{t\_ app}(\text{t\_ comp}, \text{t\_ comp}), \text{t\_ app}(\text{t\_ app}(\text{t\_ comp}, \text{t\_ comp}), \text{t\_ swap})\big) \]

Definition 39 Denotational Mapping

The structural denotational homomorphism mapping symbolic terms to the tensor space:

\[ \text{denot} : \text{ITerm} \to \text{TensorSpace} \]

Theorem 21 Denotational Soundness

One-step reduction in the symbolic calculus maps to extensional equivalence of denotations:

\[ \forall t, u, \quad t \to _I u \implies \text{denot } t \approx _{\text{ext}} \text{denot } u \]

Thus, the denotational mapping factors uniquely through the Invariant Layer quotient:

\[ \text{InvariantLayer.toExtTensor} : \text{InvariantLayer} \to \text{ExtTensor} \]

6.3.1 Sparse Matrix Operator Composition

In the concrete implementation of the axiomatic kernel (scratch/isar_ski_kernel.py), the emergent operator combinators are represented as products of the basic sparse matrices \(I, R, A, S\):

\begin{align*} \text{NORM} & \triangleq S \cdot I \\ \text{APP} & \triangleq A \cdot R \\ \text{DUP} & \triangleq S \cdot S \\ \text{COMP} & \triangleq R \cdot A \cdot S \\ \text{SWAP} & \triangleq R \cdot S \\ \text{CONST} & \triangleq I \cdot S \end{align*}

6.3.2 Plex-Agent Tensor Primitives and Special Forms

Alternatively, the runtime environment and compiler stack defined in tensor_primitives.py specify four basic tensor primitives and four special forms derived from them:

\begin{align*} \text{ATOM (0)} & \triangleq I \\ \text{PAIR (1)} & \triangleq S \\ \text{JOIN (2)} & \triangleq R \cdot A \\ \text{NORM (3)} & \triangleq I \cdot R \cdot A \cdot S \end{align*}

The special forms are defined as compositions of these primitives:

\begin{align*} \text{LAMBDA} & \triangleq \text{JOIN} \cdot \text{PAIR} \cdot \text{NORM} \\ \text{QUOTE} & \triangleq \text{ATOM} \cdot \text{NORM} \end{align*}

along with conditional branching (IF) and variable bindings (DEF).

6.4 Continuous Universal Approximation

We formalize the continuous parameter space of the ISAR update.

Definition 40 Non-Polynomial Activation

An activation function \(\sigma \in C(\mathbb {R}, \mathbb {R})\) is non-polynomial:

\[ \forall P \in \text{Polynomial } \mathbb {R}, \quad \sigma \neq P \]

Definition 41 Raw Address Space

The raw parameter configuration space \(\text{RawAddress } d\ k\) representing a neural network configuration:

\begin{align*} \text{RawAddress } d\ k & \triangleq \Sigma (N, T : \mathbb {N}), \quad (\text{Fin } T \to \text{Fin } 4 \to \mathbb {R}) \times C(\mathbb {R}^d, \text{GridState } N) \\ & \quad \times C(\text{GridState } N, \mathbb {R}^k) \end{align*}

Definition 42 Realization Map

The continuous function realized by a raw address configuration:

\[ \text{realizeRaw } d\ k\ \sigma : \text{RawAddress } d\ k \to C(\mathbb {R}^d, \mathbb {R}^k) \]

Definition 43 Address Equivalence

Two raw parameter configurations are equivalent if they realize the same continuous function.

Definition 44 Kernel Address Space

The quotient parameter space of raw addresses modulo observational equivalence:

\[ \text{KernelAddress } d\ k\ \sigma := \text{Quotient } (\text{addressSetoid } d\ k\ \sigma ) \]

We state the Universal Approximation Theorem as a named axiom (Leshno-style; not a theorem in this repository).

Axiom 5 ISAR Universal Approximation

Let \(K \subset \mathbb {R}^d\) be compact, \(f \in C(\mathbb {R}^d, \mathbb {R}^k)\) a target continuous function, \(\sigma \) a non-polynomial activation, and \(\varepsilon {\gt} 0\). Then there exists a raw address \(\theta \in \text{RawAddress } d\ k\) such that:

\[ \forall x \in K, \quad \| \text{realizeRaw } d\ k\ \sigma \ \theta \ x - f(x) \| {\lt} \varepsilon \]

6.5 Quotient Completion and Unique Representation

We complete the parameter space only as a named interface.

Axiom 6 Quotient Completion Space

The named placeholder type for a completion of KernelAddress. KernelAddress has no metric or uniform structure in Lean; this is not Mathlib Metric.Completion.

Axiom 7 Continuous Realization Limit

The named realization map on KernelAddressLimit (not a constructed Mathlib extension).

Axiom 8 Completion Embedding

Named embedding \(i : \text{KernelAddress} \to \text{KernelAddressLimit}\) (not a metric-completion inclusion).

Theorem 22 Embedding Injectivity

The named embedding is injective (from continuousRealization injectivity and the commuting axiom).

Theorem 23 Embedding Density

Compact-open density relative to the named axiom ISAR_UAT, not a metric-space density theorem.

Axiom 9 Topological Extension Bijection

Named extension axiom. Would follow from a metric on KernelAddress plus density; that metric does not exist in the formalization.

Theorem 24 ISAR Representation Theorem

Relative to the named axioms ISAR_UAT and topological_extension_bijection: every continuous \(f \in C(\mathbb {R}^d, \mathbb {R}^k)\) has a unique address \(\theta _{\text{limit}} \in \text{KernelAddressLimit}\) such that:

\[ \text{continuousRealizationLimit } d\ k\ \sigma \ \theta _{\text{limit}} = f \]

This does not prove UAT or construct a metric completion.

Theorem 25 Physical System Address

Wrapper: ISAR_representation applied to an arbitrary continuous map. Adds no physical content and no extra axiom.