Upper-branch frequency on a -dimensional lattice, and reversal along axis 0
DefinitionPinnedAsymmetryQ_omegaFix , real numbers (stiffness), (neighbour coupling), (gyroscopic strength), and a wavevector . The upper-branch frequency is
with the gauge term acting along axis 0 and the sum over all axes. The reversal along axis 0 is .
Formalization Note The square root is Real.sqrt, which returns on negative inputs; flip0 is Function.update at index .
import Mathlib
open Real BigOperators
namespace PinnedAsymmetryQ
/-- Upper-branch frequency on a uniform lattice with q axes; the gauge term acts
along axis 0. Wavevector k, stiffness K, neighbour coupling c, strength β. -/
noncomputable def omega (q : ℕ) [NeZero q] (K c β : ℝ) (k : Fin q → ℝ) : ℝ :=
β * c * sin (k 0) +
Real.sqrt ((β * c * sin (k 0)) ^ 2 + K + 2 * c * ∑ a : Fin q, (1 - cos (k a)))
/-- Reverse the wavevector along axis 0 only. -/
def flip0 (q : ℕ) [NeZero q] (k : Fin q → ℝ) : Fin q → ℝ :=
Function.update k 0 (-(k 0))
end PinnedAsymmetryQ
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Definition 1: (omega). The inputs are:
- a natural number , with the standing assumption , so ;
- three arbitrary real numbers , with no sign or other constraints (any of them may be negative or zero);
- a function , written , which is an arbitrary real vector of length .
The index is the first element of . It exists because . The value is defined as
Here and are the real sine and cosine, with arguments in radians. The sum runs over all indices, including . For it is just . Each summand lies in , but can still be negative when or .
The square root is Mathlib's total real square root:
- if , is the usual nonnegative square root;
- if , is defined to be . No error or complex value is produced.
So when , and when . At the boundary both formulas give the same value. is defined for every choice of inputs, and nothing in the definition requires .
Definition 2: (flip0). The inputs are:
- a natural number with ;
- a vector , indexed as above.
is the vector in obtained from by replacing only the entry at index with its negative and leaving every other entry unchanged:
For this is the single vector . The negated entry is the original value . does not use , and does not use . These two definitions only introduce the functions and assert nothing about them.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.