Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 5 research declarations. Search 10,000 more complete Mathlib declarations.
5 results
Clear filtersFTheory.SU5.FluxesFive.chiralIndicesOfD_noneg_of_noExotics
Plain-language statement
The chiral indices of the representations D = (bar 3,1)_{1/3} are all non-negative if there are no chiral exotics in the spectrum.
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesFive.chiralIndicesOfD_subset_sum_le_three_of_noExotics
Project documentation
The chiral indices of the representation E = (1,1)_{1} are less then or equal to 3. -/ lemma FluxesTen.chiralIndicesOfE_le_three_of_noExotics (F : FluxesTen) (hF : NoExotics F) (ci : ℤ) (hci : ci ∈ F.chiralIndicesOfE) : ci ≤ 3 := by have hle := Multiset.single_le_sum (fun x hx => chiralIndicesOfE_noneg_of_noExotics F hF x hx) ci hci rwa [F.chiralIndic...
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesFive.chiralIndicesOfL_noneg_of_noExotics
Plain-language statement
The chiral indices of the representations L = (1,2)_{-1/2} are all non-negative if there are no chiral exotics in the spectrum.
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesTen.chiralIndicesOfQ_noneg_of_noExotics
Plain-language statement
The chiral indices of the representations Q = (3,2)_{1/6} are all non-negative if there are no chiral exotics in the spectrum.
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesTen.chiralIndicesOfU_noneg_of_noExotics
Plain-language statement
The chiral indices of the representations U = (bar 3,1)_{-2/3} are all non-negative if there are no chiral exotics in the spectrum.
Source project: Physlib
Person-level attribution pending.