Large Signal Model · Plate 1 of 17

Realizable coefficients form a subspace

Exact storage includes a consistency condition.

Question to keep in view. Can every stored coefficient vector represent an observation?

For linear analysis and synthesis maps \(A:X\to C\) and \(S:C\to X\), the left-inverse law \(SA=I_X\) gives injectivity of \(A\). The coefficient projector is \(\Pi=AS\), with

\[ \Pi^2=\Pi,\qquad {\operatorname{im}}\Pi={\operatorname{im}} A,\qquad c\text{ is realizable}\iff \Pi c=c. \]

Permalink · Source line 72

A plane of realizable coefficients inside a redundant three-dimensional archive.

Permalink · Source line 76

A redundant archive. Take \(X={\mathbb R}^2\), \(C={\mathbb R}^3\) and

\[ A(x_1,x_2)=(x_1,x_2,x_1+x_2),\qquad S(c_1,c_2,c_3)=(c_1,c_2). \]

Then \(\Pi(c_1,c_2,c_3)=(c_1,c_2,c_1+c_2)\). The shaded plane is the set of realizable coefficients. The red segment shows synthesis followed by reanalysis of an inconsistent vector.

Permalink · Source line 77

The mathematical point

A left inverse determines an idempotent consistency map. Here it is oblique: \(\Pi\) is not self-adjoint. Orthogonality requires an additional hypothesis.

Permalink · Source line 82

Scope

For bounded linear maps on normed spaces, \(\|S\|\) controls amplification of coefficient errors. Exact invertibility by itself gives no conditioning guarantee.

Permalink · Source line 83

Formal route

Realization.lean; norm estimates in Normed.lean.

Permalink · Source line 84

Follow the proofs

Proposition 1: Exact realization and consistencyWritten proof · Recorded Lean scope

Inspect the mapped Lean modules

Source and reading aids

The atlas text, mathematics, plate order, and original diagrams are retained. Questions, diagram descriptions, navigation, and the bounded comparison explorer are web reading aids. No original TeX build or Lean execution is added.

Source identities and conversion checks