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

Map lift Charge

FTheory.SU5.FiveQuanta.map_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
Project-declaredLean 4.32.0

Mem lift Charge of mem no Exotics has No Zero

FTheory.SU5.FiveQuanta.mem_liftCharge_of_mem_noExotics_hasNoZero

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
Project-declaredLean 4.32.0

Mem powerset sum of mem reduce to Fluxes Five

FTheory.SU5.FiveQuanta.mem_powerset_sum_of_mem_reduce_toFluxesFive

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 eq self of of Charges nodup

FTheory.SU5.FiveQuanta.reduce_eq_self_of_ofCharges_nodup

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 Anti Chiral D of mem elems No Exotics

FTheory.SU5.FiveQuanta.reduce_numAntiChiralD_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 Anti Chiral L of mem elems No Exotics

FTheory.SU5.FiveQuanta.reduce_numAntiChiralL_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