Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Consumed finite algebra

Abstract

The finite atom supplier for the literal-V obstruction.

Definition 1.1 (literalNuNodes).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNuNodes

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNuNodes (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.2 (literalNuCoeffs).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNuCoeffs

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNuCoeffs (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.3 (literalStep).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalStep

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalStep (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.4 (literalNodes).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNodes

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNodes (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.5 (literalCoeffs).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalCoeffs

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalCoeffs (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.6 (literal_step_bounds).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_step_bounds

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_step_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.7 (literal_support).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_support

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.8 (literal_S_tail).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_S_tail

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_S_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.9 (literalNu_W_lower).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNu_W_lower

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalNu_W_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.10 (literal_moments).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_moments

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_moments (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.11 (literal_moment_residual).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_moment_residual

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_moment_residual (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.12 (literal_exp_null).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_exp_null

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_exp_null (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.13 (literal_exp_residual).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_exp_residual

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_exp_residual (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.14 (literalPair).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalPair

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalPair (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.15 (literal_S_pair).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_S_pair

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_S_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.16 (literalEtaNodes).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalEtaNodes

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalEtaNodes (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.17 (literalEtaCoeffs).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalEtaCoeffs

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalEtaCoeffs (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Definition 1.18 (literalN).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalN

Formalization. D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literalN (✓ std3).

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.19 (literal_eta_mass).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_mass

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_mass (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.20 (literal_eta_exp).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_exp

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_exp (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.21 (literal_eta_support).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_support

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.22 (literal_N_pos).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_N_pos

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_N_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.23 (literal_eta_W).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_W

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_eta_W (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.24 (literal_support_D).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_support_D

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_support_D (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.25 (literal_two_S).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_two_S

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_two_S (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

Theorem 1.26 (literal_energy_double).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_energy_double

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualKernelMomentFiniteAtom.literal_energy_double (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite atom supplier declaration consumed by the literal-V endpoint.

References