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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,171 to 1,176 of 2,569 results.
FTheory.SU5.FluxesTen.chiralIndicesOfQ_noneg_of_noExotics
Mathematical 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
Mathematical 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.
FTheory.SU5.FluxesTen.mem_elemsNoExotics_of_noExotics
Project documentation
The allowed subsets of a FluxesTen which has no exotics or zeros. -/ def noExoticsSubsets : (n : ℕ) → Finset (Multiset Fluxes) | 0 => {{}} | 1 => {{⟨1, -1⟩}, {⟨1, 0⟩}, {⟨1, 1⟩}, {⟨2, -1⟩}, {⟨2, 0⟩}, {⟨2, 1⟩}, {⟨3, 0⟩}} | 2 => {{⟨1, -1⟩, ⟨1, 0⟩}, {⟨1, -1⟩, ⟨1, 1⟩}, {⟨1, -1⟩, ⟨2, 1⟩}, {⟨1, 0⟩, ⟨1, 0⟩}, {⟨1, 0⟩, ⟨1, 1⟩}, {⟨1, 0⟩, ⟨2, 0⟩}, {⟨1, 1⟩, ⟨2, -1⟩}...
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesTen.mem_mem_finset_of_noExotics
Project documentation
Completeness of elemsNoExotics, that is, every element of FluxesFive which obeys NoExotics is an element of elemsNoExotics, and every element of elemsNoExotics obeys NoExotics. -/ lemma noExotics_iff_mem_elemsNoExotics (F : FluxesFive) : F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics := by constructor · exact fun ⟨h1, h2⟩ => mem_elemsNoExotics...
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.FluxesTen.subset_le_mem_of_card_eq_succ
Project documentation
Completeness of elemsNoExotics, that is, every element of FluxesFive which obeys NoExotics is an element of elemsNoExotics, and every element of elemsNoExotics obeys NoExotics. -/ lemma noExotics_iff_mem_elemsNoExotics (F : FluxesFive) : F.NoExotics ∧ F.HasNoZero ↔ F ∈ elemsNoExotics := by constructor · exact fun ⟨h1, h2⟩ => mem_elemsNoExotics...
Source project: Physlib
Person-level attribution pending.
FTheory.SU5.Quanta.isViable_iff_charges_mem_viableCharges_mem_liftCharges
Project documentation
The quanta satisfy the linear anomaly cancellation conditions. -/ linear_anomalies : x.LinearAnomalyCancellation lemma isViable_iff_def (x : Quanta) : IsViable x ↔ x.toCharges.IsComplete ∧ ¬ x.toCharges.IsPhenoConstrained ∧ ¬ x.toCharges.YukawaGeneratesDangerousAtLevel 1 ∧ (∃ I : CodimensionOneConfig, x.toCharges ∈ ofFinset I.allowedBarFiveCharges I.allow...
Source project: Physlib
Person-level attribution pending.