Second-Magnus Swap Curvature

Abstract

An alternating Fourier slot kernel modulates finite holonomy into a bounded second-Magnus energy.

Definition 1.1 (Second-Magnus Fourier slot kernel).

Lean statement: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.secondMagnusSwapKernel

Formalization. D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.secondMagnusSwapKernel (✓ std3).

Source. Repository-derived.

Commentary.

The kernel is the determinant obtained by assigning two frequency characters to two fixed time slots and subtracting the swapped assignment.

Definition 1.2 (Finite second-Magnus energy).

Lean statement: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.finiteSecondMagnusEnergy

Formalization. D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.finiteSecondMagnusEnergy (✓ std3).

Source. Repository-derived.

Commentary.

Each ordered-pair curvature is multiplied by its two-slot Fourier kernel, squared in norm, and summed over the finite carrier.

Definition 1.3 (Stable residual second-Magnus energy).

Lean statement: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.stableResidualSecondMagnusEnergy

Formalization. D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.stableResidualSecondMagnusEnergy (✓ std3).

Source. Repository-derived.

Commentary.

The finite second-Magnus construction is specialized to the existing stable residual swap-curvature field.

Theorem 1.4 (Frequency-exchange antisymmetry).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f_q,f_p,t_1,t_2)=-\mathrm{secondMagnusSwapKernel}(f_p,f_q,t_1,t_2).$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_swap_frequency (✓ std3). ∎

Source. Repository-derived.

Commentary.

Exchanging the two frequency labels reverses the orientation and negates the slot kernel.

Theorem 1.5 (Time-slot antisymmetry).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f_p,f_q,t_2,t_1)=-\mathrm{secondMagnusSwapKernel}(f_p,f_q,t_1,t_2).$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_swap_time (✓ std3). ∎

Source. Repository-derived.

Commentary.

Exchanging the two time slots reverses the orientation and negates the slot kernel.

Theorem 1.6 (Equal-time vanishing).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f_p,f_q,t,t)=0.$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_equal_times (✓ std3). ∎

Source. Repository-derived.

Commentary.

The alternating determinant vanishes when both evaluations use the same time slot.

Theorem 1.7 (Equal-frequency vanishing).

$$\forall f:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f,f,t_1,t_2)=0.$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_equal_frequencies (✓ std3). ∎

Source. Repository-derived.

Commentary.

The alternating determinant vanishes when both channels carry the same frequency.

Theorem 1.8 (Uniform kernel norm bound).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\Vert \mathrm{secondMagnusSwapKernel}(f_p,f_q,t_1,t_2)\Vert \le 2.$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_norm_le_two (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both phase products have unit norm, so their difference has norm at most two.

Theorem 1.9 (Center and relative decomposition).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f_p,f_q,t_1,t_2)=\mathrm{fourierPhase}(\frac{f_p+f_q}{2},t_1+t_2)\cdot (\mathrm{fourierPhase}(\frac{f_p-f_q}{2},t_1-t_2)-\mathrm{fourierPhase}(-\frac{f_p-f_q}{2},t_1-t_2)).$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_center_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mean time and mean frequency form a common unitary phase. The remaining bracket depends only on the time difference and half the frequency difference.

Theorem 1.10 (Odd sine form).

$$\forall f_p:\mathbb{R},f_q:\mathbb{R},t_1:\mathbb{R},t_2:\mathbb{R},\mathrm{secondMagnusSwapKernel}(f_p,f_q,t_1,t_2)=(-2i)\cdot \exp (-i\cdot (t_1+t_2)\cdot \frac{f_p+f_q}{2})\cdot \sin ((t_1-t_2)\cdot \frac{f_p-f_q}{2}).$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_sine_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

The relative bracket is exactly minus two times the imaginary unit times the sine of half the time-frequency area, multiplied by the common mean phase.

Theorem 1.11 (Finite energy domination).

$$\forall f,c,t_1:\mathbb{R},t_2:\mathbb{R},0\le \mathrm{finiteSecondMagnusEnergy}(f,c,t_1,t_2)\wedge \mathrm{finiteSecondMagnusEnergy}(f,c,t_1,t_2)\le 4\cdot \mathrm{finiteHolonomyEnergy}(c).$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.finite_second_magnus_energy_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite second-Magnus energy is nonnegative and bounded above by four times the underlying finite holonomy energy.

Theorem 1.12 (Residual envelope to second-Magnus decay).

$$\begin{array}{c}\forall s,r,v,f,t_1:\mathbb{R},t_2:\mathbb{R},e:\mathbb{R}:\\ (0\le e\wedge (\forall p,\Vert v_p\Vert \le 1)\wedge (\forall p,\Vert r_p\Vert \le e))\Rightarrow \\ 0\le \mathrm{stableResidualSecondMagnusEnergy}(s,r,v,f,t_1,t_2)\wedge \mathrm{stableResidualSecondMagnusEnergy}(s,r,v,f,t_1,t_2)\le 4\cdot (\mathrm{card}(\iota {)}^2\cdot (2\cdot \Vert s-1\Vert \cdot e+2\cdot e^2{)}^2)\wedge \\ (e=0\Rightarrow \mathrm{stableResidualSecondMagnusEnergy}(s,r,v,f,t_1,t_2)=0).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.stable_residual_second_magnus_energy_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Composing finite energy domination with the stable residual holonomy bound makes a vanishing residual envelope sufficient for vanishing finite second-Magnus energy.

References

• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.finiteSecondMagnusEnergy
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.finite_second_magnus_energy_bound
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.secondMagnusSwapKernel
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_center_decomposition
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_equal_frequencies
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_equal_times
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_norm_le_two
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_sine_form
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_swap_frequency
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.second_magnus_swap_kernel_swap_time
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.stableResidualSecondMagnusEnergy
• Truth anchor: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature.stable_residual_second_magnus_energy_bound
• Dependency: D5/S3/Observer/AgencyHolonomy/FiniteHolonomyEnergy
• Dependency: D5/S3/Observer/AgencyHolonomy/TimeOrderedPrimeMemoryCocycle