Large Signal Model · Plate 12 of 17

A curved domain can have a finite witness

A matrix embedding changes the certificate language.

Question to keep in view. How can a curved domain have a finite matrix certificate?

The Lorentz cone and its normalized disk admit the representation

\[ C=\{(m,x,y):m\geq\sqrt{x^2+y^2}\},\qquad J(m,x,y)=\frac12\begin{pmatrix}m+x&y\\y&m-x\end{pmatrix}. \]

A finite orbit in a normalized disk, with the corresponding positive-semidefinite matrix certificate.

Since the eigenvalues of \(J\) are \((m\pm\sqrt{x^2+y^2})/2\), membership in \(C\) is equivalent to \(J\succeq0\). Also \(\operatorname{tr}J=m\).

For the exact spatial rotation \(R=\bigl(\begin{smallmatrix}3/5&-4/5\\4/5&3/5\end{smallmatrix}\bigr)\) and \(T={\operatorname{diag}}(1,R)\),

\[ J(Tz)=\frac15WJ(z)W^{\mathsf T},\qquad W=\begin{pmatrix}2&-1\\1&2\end{pmatrix}. \]

Permalink · Source line 284

The mathematical point

A rational congruence identity certifies the unchanged rotation on the curved cone. In the full P46 model, the canonical domain has no finite normalized positive-generator certificate.

Permalink · Source line 291

Scope

The drawn orbit is finite. Density and the finite-generator obstruction are proved in the volume, not established by its plotted points. The full instrument also needs its observation, mass and initial-state identities. No quantum implementation is asserted.

Permalink · Source line 292

Formal route

RotationP46.lean; MatrixEmbedding.lean; MatrixRotation.lean.

Permalink · Source line 293

Follow the proofs

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