therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 16 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

16 results

Clear filters
Project-declaredLean 4.32.0

Reduce num Chiral D of mem elems No Exotics

FTheory.SU5.FiveQuanta.reduce_numChiralD_of_mem_elemsNoExotics

Project documentation

The reduce of FiveQuanta is a new FiveQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.toCharges.dedup.map fun q5 => (q5, ((x.filter (fun f => f.1 = q5)).map (fun y => y.2)).sum) /-! ### B.1. The reduced FiveQuanta has no duplicate elements -/ l...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Reduce num Chiral L of mem elems No Exotics

FTheory.SU5.FiveQuanta.reduce_numChiralL_of_mem_elemsNoExotics

Project documentation

The reduce of FiveQuanta is a new FiveQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.toCharges.dedup.map fun q5 => (q5, ((x.filter (fun f => f.1 = q5)).map (fun y => y.2)).sum) /-! ### B.1. The reduced FiveQuanta has no duplicate elements -/ l...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Reduce sum eq sum to Charges

FTheory.SU5.FiveQuanta.reduce_sum_eq_sum_toCharges

Project documentation

The reduce of FiveQuanta is a new FiveQuanta with all the fluxes corresponding to the same charge (i.e. representation) added together. -/ def reduce (x : FiveQuanta 𝓩) : FiveQuanta 𝓩 := x.toCharges.dedup.map fun q5 => (q5, ((x.filter (fun f => f.1 = q5)).map (fun y => y.2)).sum) /-! ### B.1. The reduced FiveQuanta has no duplicate elements -/ l...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

To Charges to Finset of mem lift Charge

FTheory.SU5.FiveQuanta.toCharges_toFinset_of_mem_liftCharge

Project documentation

Given a finite set of charges c the FiveQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. -/ def liftCharge (c : Finset 𝓩) : Multiset (FiveQuanta 𝓩) := /- The multisets of cardinality 3 containing 3 elements of c. -/ let S53 : Multiset (Multiset 𝓩) := toMultisetsThree c /- Pairs of multisets (s1, s2) such...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record