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

1 topic

2 results

Clear filters
Project-declaredLean 4.32.0

Is Pheno Constrained insert Q10 iff is Pheno Constrained Q10

SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrained_insertQ10_iff_isPhenoConstrainedQ10

Project documentation

The proposition which is true if the addition of a charge q10 to a set of charges x leads x to being phenomenologically constrained. -/ def IsPhenoConstrainedQ10 [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q10 : 𝓩) : Prop := x.AllowsTermQ10 q10 μ ∨ x.AllowsTermQ10 q10 β ∨ x.AllowsTermQ10 q10 Λ ∨ x.AllowsTermQ10 q10 W2 ∨ x.AllowsTermQ10 q10 W4 ∨ x.All...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Is Pheno Constrained insert Q5 iff is Pheno Constrained Q5

SuperSymmetry.SU5.ChargeSpectrum.isPhenoConstrained_insertQ5_iff_isPhenoConstrainedQ5

Project documentation

The proposition which is true if the addition of a charge q5 to a set of charge x leads x to being phenomenologically constrained. -/ def IsPhenoConstrainedQ5 [DecidableEq 𝓩] (x : ChargeSpectrum 𝓩) (q5 : 𝓩) : Prop := x.AllowsTermQ5 q5 μ ∨ x.AllowsTermQ5 q5 β ∨ x.AllowsTermQ5 q5 Λ ∨ x.AllowsTermQ5 q5 W2 ∨ x.AllowsTermQ5 q5 W4 ∨ x.AllowsTermQ5 q5 K...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record