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	9 math math: linearParametersQENeqZero.grav_of_cubic, 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	3 math math: grav_of_cubic, 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	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	—	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