pith. machine review for the scientific record. sign in
structure definition def or abbrev

TwoBranchRotation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  22structure TwoBranchRotation where
  23  θ_s : ℝ  -- starting angle (determines initial amplitude)
  24  θ_s_bounds : 0 < θ_s ∧ θ_s < π/2
  25  T : ℝ    -- duration of rotation
  26  T_pos : 0 < T
  27
  28/-- Residual action S = π/2 - θ_s (geodesic length on Bloch sphere) -/

used by (16)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.