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

1 topic

15 results

Clear filters
Project-declaredLean 4.32.0

Map lift Charge

FTheory.SU5.TenQuanta.map_liftCharge

Project documentation

Given a finite set of charges c the TenQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. This is defined to be as efficient as possible. -/ def liftCharge (c : Finset 𝓩) : Multiset (TenQuanta 𝓩) := /- The {(1, 0), (1, 0), (1, 0)} case. -/ /- The multisets of cardinality 3 containing 3 elements of c. -/ let...

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.TenQuanta.mem_liftCharge_of_mem_noExotics_hasNoZero

Project documentation

Given a finite set of charges c the TenQuanta which do not have exotics, duplicate charges or zero fluxes, which map down to c. This is defined to be as efficient as possible. -/ def liftCharge (c : Finset 𝓩) : Multiset (TenQuanta 𝓩) := /- The {(1, 0), (1, 0), (1, 0)} case. -/ /- The multisets of cardinality 3 containing 3 elements of c. -/ let...

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 Ten

FTheory.SU5.TenQuanta.mem_powerset_sum_of_mem_reduce_toFluxesTen

Project documentation

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

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.TenQuanta.reduce_eq_self_of_ofCharges_nodup

Project documentation

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

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Reduce num Chiral E of mem elems No Exotics

FTheory.SU5.TenQuanta.reduce_numChiralE_of_mem_elemsNoExotics

Project documentation

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

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Reduce num Chiral Q of mem elems No Exotics

FTheory.SU5.TenQuanta.reduce_numChiralQ_of_mem_elemsNoExotics

Project documentation

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

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record