recognition / Flight / Flight.Medium / HelicityProxy

structure

`HelicityProxy`

definition

show as: view math explainer →

module: IndisputableMonolith.Flight.Medium
domain: Flight
line: 66 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Flight.Medium on GitHub at line 66.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

depends on

value IndisputableMonolith.QFT.SpinStatistics

used by

MediumStateH IndisputableMonolith.Flight.Medium

formal source

  63current domain file does not expose it directly, so we provide a stubbed
  64field for downstream refinement.
  65-/
  66structure HelicityProxy where
  67  value : ℝ
  68
  69/-- Attach a helicity proxy to a medium state (display-level wrapper). -/
  70structure MediumStateH where
  71  S : MediumState
  72  H : HelicityProxy
  73
  74end Medium
  75end Flight
  76end IndisputableMonolith
  77

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.