LinearParameterization

📁 Source: PhysLean/Particles/StandardModel/AnomalyCancellation/NoGrav/One/LinearParameterization.lean

Statistics

Metric	Count
Definitions linearParameters, E', Q', Y, asCharges, asLinear, bijection, bijectionQEZero, linearParametersQENeqZero, bijection, bijectionLinearParameters, toLinearParameters, tolinearParametersQNeqZero, v, w, x	16
Theorems asLinear_val, cubic, cubic_zero_E'_zero, cubic_zero_Q'_zero, ext, ext_iff, grav, speciesVal, bijectionLinearParameters_apply_coe_E', bijectionLinearParameters_apply_coe_Q', bijectionLinearParameters_apply_coe_Y, bijectionLinearParameters_symm_apply_v, bijectionLinearParameters_symm_apply_w, bijectionLinearParameters_symm_apply_x, cube_w_v, cube_w_zero, cubic, cubic_v_or_w_zero, cubic_v_zero, ext, ext_iff, grav, grav_of_cubic, hvw, hx, toLinearParameters_coe_E', toLinearParameters_coe_Q', toLinearParameters_coe_Y, tolinearParametersQNeqZero_v, tolinearParametersQNeqZero_w, tolinearParametersQNeqZero_x	31
Total	47

SM.SMNoGrav.One

Definitions

Name	Category	Theorems
linearParameters 📖	CompData	12 math math: linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w, linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y, linearParametersQENeqZero.toLinearParameters_coe_E', linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v, linearParametersQENeqZero.toLinearParameters_coe_Y, linearParametersQENeqZero.bijectionLinearParameters_symm_apply_x, linearParametersQENeqZero.tolinearParametersQNeqZero_v, linearParametersQENeqZero.toLinearParameters_coe_Q', linearParametersQENeqZero.bijectionLinearParameters_apply_coe_E', linearParametersQENeqZero.tolinearParametersQNeqZero_x, linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Q', linearParametersQENeqZero.tolinearParametersQNeqZero_w
linearParametersQENeqZero 📖	CompData	8 math math: linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w, linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y, linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v, linearParametersQENeqZero.bijectionLinearParameters_symm_apply_x, linearParametersQENeqZero.bijectionLinearParameters_apply_coe_E', linearParametersQENeqZero.cubic, linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Q', linearParametersQENeqZero.grav

SM.SMNoGrav.One.linearParameters

Definitions

Name	Category	Theorems
E' 📖	CompOp	16 math math: SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_E', SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_x, grav, SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_v, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Q', SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_E', cubic_zero_Q'_zero, SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_x, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Q', SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_w, ext_iff, cubic
Q' 📖	CompOp	16 math math: SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_E', cubic_zero_E'_zero, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_x, grav, SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_v, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Q', SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_E', SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_x, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Q', SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_w, ext_iff, cubic
Y 📖	CompOp	8 math math: SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v, SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Y, SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_v, SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_w, ext_iff, cubic
asCharges 📖	CompOp	4 math math: grav, speciesVal, asLinear_val, cubic
asLinear 📖	CompOp	1 math math: asLinear_val
bijection 📖	CompOp	—
bijectionQEZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asLinear_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav asLinear asCharges	—	—
cubic 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube asCharges Q' Y E'	—	speciesVal
cubic_zero_E'_zero 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube asCharges E'	Q'	—	cubic
cubic_zero_Q'_zero 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube asCharges Q'	E'	—	cubic
ext 📖	—	Q' Y E'	—	—	—
ext_iff 📖	mathematical	—	Q' Y E'	—	ext
grav 📖	mathematical	—	ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMACCs.accGrav asCharges E' Q'	—	SMACCs.accGrav.eq_1 speciesVal
speciesVal 📖	mathematical	—	ACCSystemCharges.Charges SMCharges SMSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMCharges.toSpecies asCharges	—	—

SM.SMNoGrav.One.linearParametersQENeqZero

Definitions

Name	Category	Theorems
bijection 📖	CompOp	2 math math: cubic, grav
bijectionLinearParameters 📖	CompOp	6 math math: bijectionLinearParameters_symm_apply_w, bijectionLinearParameters_apply_coe_Y, bijectionLinearParameters_symm_apply_v, bijectionLinearParameters_symm_apply_x, bijectionLinearParameters_apply_coe_E', bijectionLinearParameters_apply_coe_Q'
toLinearParameters 📖	CompOp	3 math math: toLinearParameters_coe_E', toLinearParameters_coe_Y, toLinearParameters_coe_Q'
tolinearParametersQNeqZero 📖	CompOp	3 math math: tolinearParametersQNeqZero_v, tolinearParametersQNeqZero_x, tolinearParametersQNeqZero_w
v 📖	CompOp	12 math math: bijectionLinearParameters_apply_coe_Y, toLinearParameters_coe_E', bijectionLinearParameters_symm_apply_v, toLinearParameters_coe_Y, tolinearParametersQNeqZero_v, cubic_v_or_w_zero, bijectionLinearParameters_apply_coe_E', cube_w_zero, cube_w_v, ext_iff, cubic, grav
w 📖	CompOp	12 math math: bijectionLinearParameters_symm_apply_w, bijectionLinearParameters_apply_coe_Y, toLinearParameters_coe_E', toLinearParameters_coe_Y, cubic_v_or_w_zero, bijectionLinearParameters_apply_coe_E', cube_w_v, cubic_v_zero, ext_iff, cubic, grav, tolinearParametersQNeqZero_w
x 📖	CompOp	9 math math: bijectionLinearParameters_apply_coe_Y, toLinearParameters_coe_E', toLinearParameters_coe_Y, bijectionLinearParameters_symm_apply_x, toLinearParameters_coe_Q', bijectionLinearParameters_apply_coe_E', ext_iff, tolinearParametersQNeqZero_x, bijectionLinearParameters_apply_coe_Q'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijectionLinearParameters_apply_coe_E' 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters x v w	—	—
bijectionLinearParameters_apply_coe_Q' 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters x	—	—
bijectionLinearParameters_apply_coe_Y 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.Y SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters x v w	—	—
bijectionLinearParameters_symm_apply_v 📖	mathematical	—	v SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters SM.SMNoGrav.One.linearParameters.Y	—	—
bijectionLinearParameters_symm_apply_w 📖	mathematical	—	w SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters SM.SMNoGrav.One.linearParameters.Y	—	—
bijectionLinearParameters_symm_apply_x 📖	mathematical	—	x SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParametersQENeqZero bijectionLinearParameters	—	—
cube_w_v 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection	v w	—	cubic_v_or_w_zero cubic_v_zero cube_w_zero
cube_w_zero 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection w	v	—	cubic
cubic 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection v w	—	SM.SMNoGrav.One.linearParameters.cubic bijectionLinearParameters_apply_coe_E' hvw hx
cubic_v_or_w_zero 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection	v w	—	cubic
cubic_v_zero 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection v	w	—	cubic
ext 📖	—	x v w	—	—	—
ext_iff 📖	mathematical	—	x v w	—	ext
grav 📖	mathematical	—	ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMACCs.accGrav ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection v w	—	SM.SMNoGrav.One.linearParameters.grav hvw hx bijectionLinearParameters_apply_coe_E'
grav_of_cubic 📖	mathematical	HomogeneousCubic ACCSystemCharges.Charges SMCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun SMACCs.accCube ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad SM.SMNoGrav ACCSystemLinear.LinSols SMSpecies SMCharges.Q SMCharges.E SM.SMNoGrav.One.linearParametersQENeqZero bijection	SMACCs.accGrav	—	grav cube_w_v
hvw 📖	—	—	—	—	—
hx 📖	—	—	—	—	—
toLinearParameters_coe_E' 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.E' SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' toLinearParameters x v w	—	—
toLinearParameters_coe_Q' 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.E' toLinearParameters x	—	—
toLinearParameters_coe_Y 📖	mathematical	—	SM.SMNoGrav.One.linearParameters.Y SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E' toLinearParameters x v w	—	—
tolinearParametersQNeqZero_v 📖	mathematical	—	v tolinearParametersQNeqZero SM.SMNoGrav.One.linearParameters.Y SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E'	—	—
tolinearParametersQNeqZero_w 📖	mathematical	—	w tolinearParametersQNeqZero SM.SMNoGrav.One.linearParameters.Y SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters.E'	—	—
tolinearParametersQNeqZero_x 📖	mathematical	—	x tolinearParametersQNeqZero SM.SMNoGrav.One.linearParameters.Q' SM.SMNoGrav.One.linearParameters SM.SMNoGrav.One.linearParameters.E'	—	—

---

← Back to Index