pith. machine review for the scientific record. sign in
theorem proved term proof

torsion_differences

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)

  37theorem torsion_differences :
  38    tau 1 - tau 0 = 11 ∧ tau 2 - tau 1 = 6 ∧ tau 2 - tau 0 = 17 := by

proof body

Term-mode proof.

  39  simp only [tau, E_passive, W, passive_field_edges, cube_edges,
  40             active_edges_per_tick, D, wallpaper_groups]
  41  omega
  42
  43/-! ## CKM Structure from Torsion
  44
  45The Wolfenstein parametrization:
  46  |V_us| ~ λ ~ sin(θ_C)
  47  |V_cb| ~ λ²
  48  |V_ub| ~ λ³
  49
  50In RS, λ = φ^{-(τ₁ − τ₀)/some_scale}. The generation torsion
  51provides the hierarchy directly. -/
  52

used by (1)

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

depends on (19)

Lean names referenced from this declaration's body.