Golden Second-Magnus Sampling

Abstract

Golden Mellin sample times make second-Magnus curvature descend through whole golden shell shifts.

Definition 1.1 (Golden Mellin sample time).

Lean statement: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenSampleTime

Formalization. D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenSampleTime (✓ std3).

Source. Repository-derived.

Commentary.

An integral golden Fourier mode is sent to its vertical Mellin time by multiplying it by the fundamental golden angular frequency.

Definition 1.2 (Visible golden scale-circle point).

Lean statement: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleCirclePoint

Formalization. D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleCirclePoint (✓ std3).

Source. Repository-derived.

Commentary.

The unwrapped logarithmic golden coordinate is projected to the unit additive circle.

Definition 1.3 (Golden scale Fourier character).

Lean statement: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleFourierPhase

Formalization. D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleFourierPhase (✓ std3).

Source. Repository-derived.

Commentary.

The integral mode character evaluates the visible golden scale coordinate as a unit complex phase.

Theorem 1.4 (Positive multiplication becomes circle addition).

$$\forall x,y,0<x\wedge 0<y\Rightarrow \mathrm{goldenScaleCirclePoint}(x\cdot y)=\mathrm{goldenScaleCirclePoint}(x)+\mathrm{goldenScaleCirclePoint}(y).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_circle_point_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplication of positive scales adds their unwrapped logarithmic coordinates and therefore adds their visible circle points.

Theorem 1.5 (Whole golden shells have one visible circle point).

$$\forall k,x,0<x\Rightarrow \mathrm{goldenScaleCirclePoint}((ph{i}^2{)}^k\cdot x)=\mathrm{goldenScaleCirclePoint}(x).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_circle_point_phi_even_pow_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplication by any natural power of phi squared changes the unwrapped coordinate by an integer and is invisible on the unit additive circle.

Theorem 1.6 (Golden circle phase equals sampled log-frequency phase).

$$\forall x,m,\mathrm{goldenScaleFourierPhase}(x,m)=\mathrm{fourierPhase}(\log (x),\mathrm{goldenSampleTime}(m)).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_eq_log_frequency (✓ std3). ∎

Source. Repository-derived.

Commentary.

The golden circle character is exactly the existing Fourier character of log scale evaluated at the corresponding golden Mellin sample time.

Theorem 1.7 (Golden scale characters have unit norm).

$$\forall x,m,\Vert \mathrm{goldenScaleFourierPhase}(x,m)\Vert =1.$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_norm (✓ std3). ∎

Source. Repository-derived.

Commentary.

The sampled phase lies on the complex unit circle for every real scale and integral mode.

Theorem 1.8 (Golden scale characters are multiplicative).

$$\forall x,y,m,0<x\wedge 0<y\Rightarrow \mathrm{goldenScaleFourierPhase}(x\cdot y,m)=\mathrm{goldenScaleFourierPhase}(x,m)\cdot \mathrm{goldenScaleFourierPhase}(y,m).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

At one integral mode, the phase of a positive product is the product of the two phases.

Theorem 1.9 (Integral modes ignore whole golden shell shifts).

$$\forall k,x,m,0<x\Rightarrow \mathrm{goldenScaleFourierPhase}((ph{i}^2{)}^k\cdot x,m)=\mathrm{goldenScaleFourierPhase}(x,m).$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_phi_even_pow_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every natural whole-shell shift contributes an integral multiple of a full circle turn, so the complex phase is unchanged.

Theorem 1.10 (Golden sampling realizes the second-Magnus alternant).

$$\begin{array}{c}\forall x,y,m_1,m_2:\\ \mathrm{secondMagnusSwapKernel}(\log (x),\log (y),\mathrm{goldenSampleTime}(m_1),\mathrm{goldenSampleTime}(m_2))=\mathrm{goldenScaleFourierPhase}(x,m_1)\cdot \mathrm{goldenScaleFourierPhase}(y,m_2)-\mathrm{goldenScaleFourierPhase}(y,m_1)\cdot \mathrm{goldenScaleFourierPhase}(x,m_2).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.second_magnus_kernel_at_golden_samples (✓ std3). ∎

Source. Repository-derived.

Commentary.

At two golden Mellin sample times, the existing second-Magnus kernel is the alternating determinant of four golden scale character values.

Theorem 1.11 (The sampled kernel descends through shell orbits).

$$\begin{array}{c}\forall k_x,k_y,x,y,m_1,m_2,0<x\wedge 0<y\Rightarrow \\ \mathrm{secondMagnusSwapKernel}(\log ((ph{i}^2{)}^{k_x}\cdot x),\log ((ph{i}^2{)}^{k_y}\cdot y),\mathrm{goldenSampleTime}(m_1),\mathrm{goldenSampleTime}(m_2))=\mathrm{secondMagnusSwapKernel}(\log (x),\log (y),\mathrm{goldenSampleTime}(m_1),\mathrm{goldenSampleTime}(m_2)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_second_magnus_shell_orbit_invariance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Independent whole-shell shifts of the two positive scale inputs leave the sampled second-Magnus kernel unchanged.

Theorem 1.12 (Finite sampled energy descends through channelwise shell orbits).

$$\begin{array}{c}\forall s,k,c,m_1,m_2,(\forall p,0<s_p)\Rightarrow \\ \mathrm{finiteSecondMagnusEnergy}(p\mapsto \log ((ph{i}^2{)}^{k_p}\cdot s_p),c,\mathrm{goldenSampleTime}(m_1),\mathrm{goldenSampleTime}(m_2))\\ =\mathrm{finiteSecondMagnusEnergy}(p\mapsto \log (s_p),c,\mathrm{goldenSampleTime}(m_1),\mathrm{goldenSampleTime}(m_2)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.finite_second_magnus_energy_golden_shell_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Applying an independent natural whole-shell shift to every positive scale channel preserves the complete finite second-Magnus energy.

References

• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.finite_second_magnus_energy_golden_shell_invariant
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenSampleTime
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleCirclePoint
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.goldenScaleFourierPhase
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_circle_point_mul
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_circle_point_phi_even_pow_mul
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_eq_log_frequency
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_mul
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_norm
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_scale_fourier_phase_phi_even_pow_mul
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.golden_second_magnus_shell_orbit_invariance
• Truth anchor: D5/S3/Observer/GoldenPrimeCircle/GoldenSecondMagnusSampling.second_magnus_kernel_at_golden_samples
• Dependency: D5/S3/Observer/AgencyHolonomy/SecondMagnusSwapCurvature
• Dependency: D5/S3/Observer/GoldenPrimeCircle/GoldenVerticalSampling