Shifted Xi Observation Layers

Abstract

Opposite shifted-xi observations are sharp reflections linked by the frozen scattering quotient.

Definition 1.1 (Positive shifted-xi observation).

Lean statement: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservation

Formalization. D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservation (✓ std3).

Source. Repository-derived.

Commentary.

The positive layer evaluates the frozen xi reading at one half plus the real observation depth minus i times the spectral coordinate.

Definition 1.2 (Sharp shifted-xi observation).

Lean statement: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservationSharp

Formalization. D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservationSharp (✓ std3).

Source. Repository-derived.

Commentary.

Sharp reflection conjugates the value of the positive observation at the conjugate spectral coordinate.

Theorem 1.3 (The two shifted-xi observation layers).

$$\begin{gathered} \forall \omega \in \mathbb{R},\forall z\in \mathbb{C}, \\ (\omega >0\wedge \mathrm{shiftedXiObservation}(\omega ,z)\ne 0)\Rightarrow \\ \mathrm{shiftedXiObservationSharp}(\omega ,z)=\mathrm{xiReading}(\frac{1}{2}-\omega -i\cdot z)\wedge \\ \mathrm{shiftedXiScattering}(\omega ,z)=\frac{\mathrm{shiftedXiObservationSharp}(\omega ,z)}{\mathrm{shiftedXiObservation}(\omega ,z)}\wedge \\ \mathrm{shiftedXiScattering}(\omega ,z)\cdot \mathrm{shiftedXiObservation}(\omega ,z)=\mathrm{shiftedXiObservationSharp}(\omega ,z). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shifted_xi_observation_layers (✓ std3). ∎

Source. Repository-derived.

Commentary.

At positive real depth, xi reflection identifies the sharp positive observation with the negative shifted layer. The existing shifted-xi scattering reading is exactly the quotient of these two layers.

The positive layer is assumed nonzero before quotient multiplication is cancelled. This excludes Lean’s totalized division-by-zero value.

This is the self-contained algebraic observation-layer closure of the source. The Suzuki meromorphic-inner criterion and the associated de Branges claims require external analytic definitions and results and are not asserted here.

Theorem 1.4 (A regular observation at depth one half).

$$\begin{gathered} 0<\frac{1}{2}\wedge \\ \mathrm{shiftedXiObservation}(\frac{1}{2},0)\ne 0\wedge \\ \mathrm{shiftedXiObservationSharp}(\frac{1}{2},0)=\mathrm{xiReading}(\frac{1}{2}-\frac{1}{2}-i\cdot 0)\wedge \\ \mathrm{shiftedXiScattering}(\frac{1}{2},0)=\frac{\mathrm{shiftedXiObservationSharp}(\frac{1}{2},0)}{\mathrm{shiftedXiObservation}(\frac{1}{2},0)}\wedge \\ \mathrm{shiftedXiScattering}(\frac{1}{2},0)\cdot \mathrm{shiftedXiObservation}(\frac{1}{2},0)=\mathrm{shiftedXiObservationSharp}(\frac{1}{2},0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Scattering/ShiftedXiObservationLayers.positive_depth_observation_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

Depth one half and spectral coordinate zero give a concrete positive-depth instance whose positive layer is nonzero and satisfies all three laws.

Theorem 1.5 (A zero denominator breaks transition recovery).

$$\begin{gathered} numerator:=1,denominator:=0, \\ denominator=0\wedge \frac{numerator}{denominator}\cdot denominator\ne numerator. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Scattering/ShiftedXiObservationLayers.zero_denominator_breaks_transition_recovery (✓ std3). ∎

Source. Repository-derived.

Commentary.

The concrete numerator one and denominator zero show that quotient multiplication cannot recover a nonzero numerator without the regularity premise.

References

• Truth anchor: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.positive_depth_observation_witness
• Truth anchor: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservation
• Truth anchor: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shiftedXiObservationSharp
• Truth anchor: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.shifted_xi_observation_layers
• Truth anchor: D5/S3/Weil/Scattering/ShiftedXiObservationLayers.zero_denominator_breaks_transition_recovery
• Dependency: D5/S3/Weil/Scattering/FiniteScatteringCascade
• Dependency: D5/S3/Zeros/Symmetry/ZetaConjugationCovariance