ISAR Universal Approximation

What this file establishes

The ISAR kernel has two kinds of universality:

Logical universality (proved elsewhere in this codebase):

• morphism_uniqueness (KernelCategory): ISAR_Kernel is the terminal object — every admissible rewriting system embeds into it via a unique canonical morphism.
• K1_nilpotent / K2_nilpotent (ISARMatrices): the core rewrite operator K = IRAS satisfies K² = 0.
• isk_expressive_completeness (BasisCompleteness): every ISKAlgebra matrix is the image of some ISK term under the structural homomorphism term_signature_val.

Statistical and Topological universality (this file):

• Defines RMat := Matrix (Fin 4) (Fin 4) ℝ using Mathlib, which carries a full CommRing, Module ℝ, NormedAddCommGroup, and InnerProductSpace ℝ for free.
• Proves rigorously that RMat inherits the nilpotency of K from the integer proof, sorry-free, using Matrix.mul_apply and Mathlib cast lemmas.
• Defines the ISAR update kernel as an ℝ-linear combination of basis matrices, parametrised by (αI, αR, αA, αS) ∈ ℝ⁴. No ℚ→ℝ gap.
• Proves constructively that the continuous-limit update map activatedUpdate is well-defined and continuous, reducing the axiom space.
• States named axioms ISAR_UAT (analytic, not proved) and a named completion interface (KernelAddressLimit, …). KernelAddress has no metric.

Why K² = 0 is the key structural property

Nilpotency means the ISAR update is a pure first-order generator:

exp(εK) = I + εK (the exponential series terminates at degree 1)

Composing T such steps interleaved with a nonlinear activation σ: σ(I + ε_T K) ∘ ⋯ ∘ σ(I + ε_1 K)

implements a depth-T polynomial approximation of the target function, parametrised continuously in (ε_1, ..., ε_T) ∈ ℝᵀ. By the Weierstrass approximation theorem, polynomials are dense in C(X, ℝ) for compact X, so T → ∞ gives universal approximation.

Scalar type: ℤ → ℝ directly, no ℚ layer

The algebra is proved over ℤ in ISARMatrices, lifted to ℝ via Int.cast. Unlike the earlier QMat/Rat version, ISARUpdateR lives in ℝ⁴ from the start — the ℚ→ℝ density gap no longer applies.

Axiom inventory (all intentional — see ADR-003)

ISAR_UAT, KernelAddressLimit, continuousRealizationLimit, kernelAddressEmbedding, continuousRealizationLimit_coe, topological_extension_bijection.

All other structures (Activation, nonPolynomial, RawAddress, KernelAddress, activatedUpdate, ISAR_representation, kernelAddressEmbedding_injective, kernelAddressEmbedding_dense) are defined or proved concretely.

Freeze (2026-08-16): the freeze is the decision, not a placeholder. KernelAddress has no MetricSpace/UniformSpace instance, so KernelAddressLimit is not Mathlib Metric.Completion. Do not invent a compact-K or BoundedContinuousFunction metric this cycle (that would be a different theorem). ISAR_UAT remains a named analytic axiom (not a theorem). Next wiring is Metric.Completion only, after a metric exists. Do not add physical-system axioms.

1. Real 4×4 matrices via Mathlib

@[reducible, inline]

abbrev ISAR.RMat : Type

RMat: Mathlib's Matrix (Fin 4) (Fin 4) ℝ. Carries CommRing, Module ℝ, NormedAddCommGroup, InnerProductSpace ℝ for free. Replaces the hand-rolled QMat and its 4 @[simp] app lemmas — Mathlib already has Matrix.mul_apply, Matrix.add_apply, Matrix.zero_apply, Matrix.smul_apply.

Equations

• ISAR.RMat = Matrix (Fin 4) (Fin 4) ℝ

2. Lifting Matrix4 (Int) to RMat (ℝ)

def ISAR.toRMat (M : Matrix4) : RMat

The canonical ring homomorphism from Matrix4 (over Int) to RMat (over ℝ), using Lean's built-in Int → ℝ coercion (Int.cast / algebraMap ℤ ℝ).

Equations

• ISAR.toRMat M i j = ↑(ISAR.fromMatrix4 M i j)

theorem ISAR.toRMat_zero : toRMat zero = 0

toRMat sends the zero matrix to zero.

theorem ISAR.toRMat_mul (M N : Matrix4) : toRMat (M * N) = toRMat M * toRMat N

toRMat is a ring homomorphism: it respects matrix multiplication.

3. ISAR Basis Matrices over ℝ

@[reducible, inline]

abbrev ISAR.I1R : RMat

The invariant-projection matrix I, lifted to ℝ.

Equations

• ISAR.I1R = ISAR.toRMat ISAR.I1

@[reducible, inline]

abbrev ISAR.R1R : RMat

The rotation matrix R, lifted to ℝ.

Equations

• ISAR.R1R = ISAR.toRMat ISAR.R1

@[reducible, inline]

abbrev ISAR.A1R : RMat

The adjacency matrix A, lifted to ℝ.

Equations

• ISAR.A1R = ISAR.toRMat ISAR.A1

@[reducible, inline]

abbrev ISAR.S1R : RMat

The selection matrix S, lifted to ℝ.

Equations

• ISAR.S1R = ISAR.toRMat ISAR.S1

@[reducible, inline]

abbrev ISAR.K1R : RMat

The nilpotent core kernel K = I·R·A·S, lifted to ℝ.

Equations

• ISAR.K1R = ISAR.toRMat (ISAR.I1 * ISAR.R1 * ISAR.A1 * ISAR.S1)

4. Nilpotency (ℝ world)

theorem ISAR.K1R_nilpotent : K1R * K1R = 0

K1 is nilpotent of order 2 in the ℝ representation. Transferred from K1_nilpotent (proved over Int by decide) via toRMat_mul.

theorem ISAR.K2R_nilpotent : toRMat (I2 * R2 * A2 * S2) * toRMat (I2 * R2 * A2 * S2) = 0

K2 is also nilpotent of order 2.

5. The Differentiable ISAR Update Kernel over ℝ

def ISAR.ISARUpdateR (αI αR αA αS : ℝ) : RMat

The differentiable ISAR update matrix: an ℝ-linear combination of the four basis matrices, parametrised by (αI, αR, αA, αS) ∈ ℝ⁴.

ISARUpdateR αI αR αA αS = αI·I + αR·R + αA·A + αS·S

Scalar multiplication • is Mathlib's SMul ℝ (Matrix ...) from the module structure. Unlike the former QMat version over ℚ, parameters live in ℝ from the start.

Equations

• ISAR.ISARUpdateR αI αR αA αS = αI • ISAR.I1R + αR • ISAR.R1R + αA • ISAR.A1R + αS • ISAR.S1R

theorem ISAR.ISARUpdateR_zero_params : ISARUpdateR 0 0 0 0 = 0

The zero parameter choice gives the zero matrix.

6. Iterated Update Rule

def ISAR.linearIterateR (U : RMat) : ℕ → RMat

Iterate the update matrix U, T times.

Equations

• ISAR.linearIterateR U 0 = 1
• ISAR.linearIterateR U n.succ = U * ISAR.linearIterateR U n

theorem ISAR.linearIterateR_zero (U : RMat) : linearIterateR U 0 = 1

theorem ISAR.linearIterateR_succ (U : RMat) (n : ℕ) : linearIterateR U (n + 1) = U * linearIterateR U n

theorem ISAR.nilpotent_kills_higher_order : K1R * K1R = 0

First-order flow property (consequence of K² = 0).

7. Universal Approximation (Continuous Morphism and Address Space)

@[reducible, inline]

abbrev ISAR.Activation : Type

A nonlinear activation function: continuous real functions ℝ → ℝ.

Equations

• ISAR.Activation = C(ℝ, ℝ)

def ISAR.evalPoly (coeffs : List ℝ) (x : ℝ) : ℝ

Horner's method to evaluate a polynomial represented as a list of real coefficients.

Equations

• ISAR.evalPoly coeffs x = List.foldr (fun (coef acc : ℝ) => coef + x * acc) 0 coeffs

def ISAR.Activation.nonPolynomial (σ : Activation) : Prop

Predicate: σ is non-polynomial (necessary condition for representation).

Equations

• σ.nonPolynomial = ∀ (coeffs : List ℝ), ⇑σ ≠ ISAR.evalPoly coeffs

@[reducible, inline]

abbrev ISAR.GridState (N : ℕ) : Type

Grid state: N cells, each with a 4-dimensional real state vector. We represent the grid index space as Fin N × Fin 4. This is mathematically isomorphic to Fin (4 * N) but allows direct, type-safe block-diagonal indexing without division or modulo operations.

Equations

• ISAR.GridState N = EuclideanSpace ℝ (Fin N × Fin 4)

def ISAR.middleMap (N : ℕ) (U : RMat) (v : Fin N × Fin 4 → ℝ) : Fin N × Fin 4 → ℝ

The middle linear map representing the block-diagonal matrix multiplication by U.

Equations

• ISAR.middleMap N U v p = ∑ j' : Fin 4, U p.2 j' * v (p.1, j')

theorem ISAR.continuous_middleMap (N : ℕ) (U : RMat) : Continuous (middleMap N U)

Proof of continuity of the middle linear map.

noncomputable def ISAR.blockDiagonalAction (N : ℕ) (U : RMat) (x : GridState N) : GridState N

The block-diagonal action of U on GridState N.

Mathematical Motivation: Implements the linear transformation step of the neural network update (a block-diagonal matrix multiplication action on the grid coordinates). Why Noncomputable: Relies on real numbers (ℝ) via WithLp.equiv, which is defined as a topological completion of ℚ and does not have a constructive computational representation in Lean.

Equations

• ISAR.blockDiagonalAction N U x = (WithLp.equiv 2 (Fin N × Fin 4 → ℝ)).symm (ISAR.middleMap N U ((WithLp.equiv 2 (Fin N × Fin 4 → ℝ)) x))

theorem ISAR.continuous_blockDiagonalAction (N : ℕ) (U : RMat) : Continuous (blockDiagonalAction N U)

Proof of continuity of the block-diagonal update action.

noncomputable def ISAR.continuousBlockDiagonalAction (N : ℕ) (U : RMat) : C(GridState N, GridState N)

The bundled continuous block-diagonal linear map.

Mathematical Motivation: Lifts blockDiagonalAction to a bundled continuous map C(GridState N, GridState N). Why Noncomputable: Bundling a function into a ContinuousMap requires proving continuity, and evaluates on topological spaces using noncomputable real numbers (ℝ).

Equations

• ISAR.continuousBlockDiagonalAction N U = { toFun := ISAR.blockDiagonalAction N U, continuous_toFun := ⋯ }

noncomputable def ISAR.applyActivation (σ : Activation) (N : ℕ) (x : GridState N) : GridState N

The elementwise activation function applied to a GridState.

Mathematical Motivation: Implements the element-wise nonlinear activation function application on the grid state. Why Noncomputable: Performs function application over ℝ using WithLp.equiv and continuous activation functions, neither of which have constructive computational representations.

Equations

• ISAR.applyActivation σ N x = (WithLp.equiv 2 (Fin N × Fin 4 → ℝ)).symm fun (p : Fin N × Fin 4) => σ ((WithLp.equiv 2 (Fin N × Fin 4 → ℝ)) x p)

theorem ISAR.continuous_applyActivation (σ : Activation) (N : ℕ) : Continuous fun (v : Fin N × Fin 4 → ℝ) (p : Fin N × Fin 4) => σ (v p)

Proof of continuity of the elementwise function application.

theorem ISAR.continuous_applyActivation_state (σ : Activation) (N : ℕ) : Continuous (applyActivation σ N)

Proof of continuity of applyActivation.

noncomputable def ISAR.continuousApplyActivation (σ : Activation) (N : ℕ) : C(GridState N, GridState N)

The bundled continuous elementwise activation map.

Mathematical Motivation: Lifts applyActivation to a bundled continuous map C(GridState N, GridState N). Why Noncomputable: Evaluates real functions and relies on the noncomputable real topology.

Equations

• ISAR.continuousApplyActivation σ N = { toFun := ISAR.applyActivation σ N, continuous_toFun := ⋯ }

noncomputable def ISAR.activatedUpdate (σ : Activation) (N T : ℕ) : (Fin T → Fin 4 → ℝ) → C(GridState N, GridState N)

activatedUpdate: The concrete, recursive definition of the T-step ISAR update with alternating activation. Defined constructively via composing the continuous block-diagonal updates and elementwise activations.

Mathematical Motivation: Computes the multi-layer neural network update $F_{\theta} = \sigma \circ U_T \circ \dots \circ \sigma \circ U_1$. Why Noncomputable: Combines continuous maps via composition (ContinuousMap.comp) over continuous spaces, which relies on noncomputable real numbers (ℝ).

Equations

• One or more equations did not get rendered due to their size.
• ISAR.activatedUpdate σ N 0 x_2 = ContinuousMap.id (ISAR.GridState N)

def ISAR.RawAddress (d k : ℕ) : Type

RawAddress: the concrete configuration space representing all finite-grid, finite-time neural representations of the ISAR update. Contains the grid size N, time steps T, parameter sequence θ, and the bundled continuous encoder and readout maps.

Equations

• ISAR.RawAddress d k = ((N : ℕ) × (T : ℕ) × (Fin T → Fin 4 → ℝ) × C(EuclideanSpace ℝ (Fin d), ISAR.GridState N) × C(ISAR.GridState N, EuclideanSpace ℝ (Fin k)))

noncomputable def ISAR.realizeRaw (d k : ℕ) (σ : Activation) (θ : RawAddress d k) : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))

The realization map mapping a raw parameter trajectory to a continuous function. Computes the composition: readout ∘ activatedUpdate ∘ encode.

Mathematical Motivation: Realizes the full neural network representation from the parameters (encoder, readout, updates). Why Noncomputable: Computes composition of continuous maps over continuous Euclidean spaces, which is noncomputable in Lean.

Equations

• ISAR.realizeRaw d k σ θ = θ.snd.snd.2.2.comp ((ISAR.activatedUpdate σ θ.fst θ.snd.fst θ.snd.snd.1).comp θ.snd.snd.2.1)

def ISAR.AddressEq (d k : ℕ) (σ : Activation) (θ₁ θ₂ : RawAddress d k) : Prop

Two raw addresses are observationally/functionally equivalent if they realize the same continuous function.

Equations

• ISAR.AddressEq d k σ θ₁ θ₂ = (ISAR.realizeRaw d k σ θ₁ = ISAR.realizeRaw d k σ θ₂)

noncomputable def ISAR.addressSetoid (d k : ℕ) (σ : Activation) : Setoid (RawAddress d k)

The setoid defining the functional equivalence relation on RawAddress.

Mathematical Motivation: Equates two addresses if they yield the exact same continuous realization function. Why Noncomputable: The equality relation realizeRaw d k σ θ₁ = realizeRaw d k σ θ₂ is an equality of continuous functions over ℝᵈ, which is mathematically undecidable/noncomputable.

Equations

• ISAR.addressSetoid d k σ = { r := ISAR.AddressEq d k σ, iseqv := ⋯ }

def ISAR.KernelAddress (d k : ℕ) (σ : Activation) : Type

KernelAddress: the address space defined as the quotient of RawAddress modulo observational/functional equivalence. This is the exact continuous counterpart to the discrete InvariantLayer.

Equations

• ISAR.KernelAddress d k σ = Quotient (ISAR.addressSetoid d k σ)

noncomputable def ISAR.continuousRealization (d k : ℕ) (σ : Activation) (q : KernelAddress d k σ) : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))

The well-defined continuous realization of a quotiented KernelAddress. Derived via Quotient.lift from realizeRaw.

Mathematical Motivation: The canonical projection/realization map from the quotient space KernelAddress to the space of continuous functions. Why Noncomputable: Relies on Quotient.lift over a noncomputable equivalence relation, and returns a continuous function over ℝ.

Equations

• ISAR.continuousRealization d k σ q = Quotient.lift (fun (θ : ISAR.RawAddress d k) => ISAR.realizeRaw d k σ θ) ⋯ q

theorem ISAR.continuousRealization_injective (d k : ℕ) (σ : Activation) (q₁ q₂ : KernelAddress d k σ) : continuousRealization d k σ q₁ = continuousRealization d k σ q₂ → q₁ = q₂

Injectivity of the Continuous Realization.

By construction, two equivalence classes in the quotient address space KernelAddress are equal if and only if they realize the exact same continuous function. This guarantees that the representation is unique (injectivity holds constructively).

def ISAR.InvariantLayerContinuousBridge : InvariantLayer ≃ Quotient operEqSetoid

Conceptual Bridge to the Invariant Layer.

This equivalence formally states that the topological quotient KernelAddress uses the exact same mathematical construction as the discrete symbolic InvariantLayer. Both are quotients of a raw representation space modulo operational/observational equivalence.

Equations

• ISAR.InvariantLayerContinuousBridge = Equiv.refl ISAR.InvariantLayer

axiom ISAR.ISAR_UAT (d k : ℕ) (K : Set (EuclideanSpace ℝ (Fin d))) : IsCompact K → ∀ (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) (σ : Activation), σ.nonPolynomial → ∀ (ε : ℝ), 0 < ε → ∃ (θ : RawAddress d k), ∀ x ∈ K, ‖(realizeRaw d k σ θ) x - f x‖ < ε

Named axiom ISAR_UAT (not a theorem).

For any continuous function f : ℝᵈ → ℝᵏ, a non-polynomial activation σ, and a compact domain K ⊆ ℝᵈ, the finite-grid iterated ISAR update can approximate f uniformly on K to arbitrary precision ε > 0.

Why named: Leshno, Lin, Pinkus, and Schocken (1993) is the cited analytic fact (non-polynomial continuous σ iff universal on compact sets; generalizing Cybenko 1989 / Hornik 1991, which require boundedness). Not proved in this repository.

axiom ISAR.KernelAddressLimit (d k : ℕ) (σ : Activation) : Type

Named placeholder for a completion of KernelAddress.

Not constructed: KernelAddress has no MetricSpace/UniformSpace instance (C(ℝᵈ, ℝᵏ) on unbounded Euclidean domains is compact-open, not a global supremum metric). This is not Mathlib Metric.Completion. Next wiring is Metric.Completion only, after a metric exists.

axiom ISAR.continuousRealizationLimit (d k : ℕ) (σ : Activation) : KernelAddressLimit d k σ → C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))

Named realization map on KernelAddressLimit.

Not constructed: would be the unique continuous extension of continuousRealization after a metric/uniform structure exists.

axiom ISAR.kernelAddressEmbedding (d k : ℕ) (σ : Activation) : KernelAddress d k σ → KernelAddressLimit d k σ

Named embedding KernelAddress → KernelAddressLimit.

Not constructed: would be the inclusion into a metric completion.

axiom ISAR.continuousRealizationLimit_coe (d k : ℕ) (σ : Activation) (q : KernelAddress d k σ) : continuousRealizationLimit d k σ (kernelAddressEmbedding d k σ q) = continuousRealization d k σ q

Named commuting law: realization on the limit agrees with continuousRealization after embedding. Relies on the named completion axioms, not on a Mathlib extension.

theorem ISAR.kernelAddressEmbedding_injective (d k : ℕ) (σ : Activation) : Function.Injective (kernelAddressEmbedding d k σ)

Injectivity of the named embedding.

Follows from injectivity of continuousRealization plus the named commuting axiom continuousRealizationLimit_coe. Not a metric-completion theorem.

theorem ISAR.kernelAddressEmbedding_dense (d k : ℕ) (σ : Activation) (h_np : σ.nonPolynomial) (K : Set (EuclideanSpace ℝ (Fin d))) (hK : IsCompact K) (θ_limit : KernelAddressLimit d k σ) (ε : ℝ) (hε : 0 < ε) : ∃ (q : KernelAddress d k σ), ∀ x ∈ K, ‖(continuousRealization d k σ q) x - (continuousRealizationLimit d k σ θ_limit) x‖ < ε

Compact-open density relative to ISAR_UAT.

Any KernelAddressLimit realization can be approximated uniformly on a compact set by a KernelAddress, using the named axiom ISAR_UAT. This is not a metric-space density theorem (there is no metric on KernelAddress).

axiom ISAR.topological_extension_bijection (d k : ℕ) (σ : Activation) (h_inj : ∀ (q₁ q₂ : KernelAddress d k σ), continuousRealization d k σ q₁ = continuousRealization d k σ q₂ → q₁ = q₂) (h_dense : ∀ (K : Set (EuclideanSpace ℝ (Fin d))), IsCompact K → ∀ (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) (ε : ℝ), 0 < ε → ∃ (q : KernelAddress d k σ), ∀ x ∈ K, ‖(continuousRealization d k σ q) x - f x‖ < ε) (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) : ∃! θ_limit : KernelAddressLimit d k σ, continuousRealizationLimit d k σ θ_limit = f

Named extension/bijection axiom (not Mathlib UniformSpace.Completion.extension).

Would follow from a metric on KernelAddress (pullback of a metric on C(ℝᵈ, ℝᵏ) via continuousRealization) plus isometric embedding and density. That metric does not exist in this file. The axiom stays named until Metric.Completion can be wired.

theorem ISAR.ISAR_representation (d k : ℕ) (σ : Activation) (h_np : σ.nonPolynomial) (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) : ∃! θ_limit : KernelAddressLimit d k σ, continuousRealizationLimit d k σ θ_limit = f

Representation relative to named completion axioms.

Every continuous f has a unique KernelAddressLimit address if one assumes topological_extension_bijection and ISAR_UAT. Not a constructed completion theorem; ISAR_UAT remains a named analytic axiom.

theorem ISAR.ISAR_logical_and_statistical_universality : (∀ (K : Kernel) (f : KernelHom K ISAR_Kernel) (c : K.Carrier), OperEq (f.hom c) (K.decode c)) ∧ (∀ (d k : ℕ) (K : Set (EuclideanSpace ℝ (Fin d))), IsCompact K → ∀ (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) (σ : Activation), σ.nonPolynomial → ∀ (ε : ℝ), 0 < ε → ∃ (θ : RawAddress d k), ∀ x ∈ K, ‖(realizeRaw d k σ θ) x - f x‖ < ε) ∧ ∀ (d k : ℕ) (σ : Activation), σ.nonPolynomial → ∀ (f : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))), ∃! θ_limit : KernelAddressLimit d k σ, continuousRealizationLimit d k σ θ_limit = f

Corollary: logical universality plus named analytic/completion axioms.

1. Logical universality (morphism_uniqueness, propext): unique morphisms into ISAR_Kernel relative to the Kernel interface.
2. Statistical approximation (named axiom ISAR_UAT, not proved): every continuous f is approximable on compact K by a RawAddress.
3. Representation (ISAR_representation): unique KernelAddressLimit address, relative to ISAR_UAT and the named completion axioms — not a theorem that UAT or metric completion has been constructed.

theorem ISAR.physical_system_has_address (d k : ℕ) (σ : Activation) (h_np : σ.nonPolynomial) (f_sys : C(EuclideanSpace ℝ (Fin d), EuclideanSpace ℝ (Fin k))) : ∃! θ : KernelAddressLimit d k σ, continuousRealizationLimit d k σ θ = f_sys

Wrapper: ISAR_representation applied to an arbitrary continuous map. Adds no physical content and no extra axiom. Relies on the same named ISAR_UAT / completion axioms as ISAR_representation.