BasisLinear

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/Odd/BasisLinear.lean

Statistics

Metric	Count
Definitions P, P!, P!', P', Pa, Pa', basis, basis!, basis!AsCharges, basisAsCharges, basisa, basisaAsBasis, oddFst, oddMid, oddShiftFst, oddShiftShiftFst, oddShiftShiftMid, oddShiftShiftSnd, oddShiftShiftZero, oddShiftSnd, oddShiftZero, oddSnd	22
Theorems P!'_val, P!_accCube, P!_linearACC, P!_oddShiftFst, P!_oddShiftSnd, P!_oddShiftZero, P!_zero, P'_val, P_P_P!_accCube, P_accCube, P_linearACC, P_oddFst, P_oddMid, P_oddSnd, P_zero, Pa'_P'_P!', Pa'_elim_eq_iff, Pa'_eq, Pa_eq, Pa_oddShiftShiftFst, Pa_oddShiftShiftMid, Pa_oddShiftShiftSnd, Pa_oddShiftShiftZero, Pa_zero, Pa_zero!, basis!_linearACC, basis!_linear_independent, basis!_oddShiftSnd_eq_minus_oddShiftFst, basis!_on_oddShiftFst_other, basis!_on_oddShiftFst_self, basis!_on_oddShiftSnd_other, basis!_on_oddShiftSnd_self, basis!_on_oddShiftZero, basis!_on_other, basis!_val, basis_linearACC, basis_linear_independent, basis_oddSnd_eq_minus_oddFst, basis_on_oddFst_other, basis_on_oddFst_self, basis_on_oddMid, basis_on_oddSnd_other, basis_on_oddSnd_self, basis_on_other, basis_val, basisa_card, basisa_linear_independent, oddShiftShiftFst_eq_oddFst_succ, oddShiftShiftFst_eq_oddShiftFst_castSucc, oddShiftShiftMid_eq_oddMid, oddShiftShiftMid_eq_oddShiftFst_last, oddShiftShiftSnd_eq_oddShiftSnd, oddShiftShiftSnd_eq_oddSnd, oddShiftShiftZero_eq_oddFst_zero, oddShiftShiftZero_eq_oddShiftZero, oddSnd_eq_oddShiftSnd, odd_shift_eq, odd_shift_shift_eq, span_basis, span_basis_swap!, sum_odd, sum_oddShift, swap!_as_add	63
Total	85

PureU1.VectorLikeOddPlane

Definitions

Name	Category	Theorems
P 📖	CompOp	11 math math: PureU1.Odd.parameterizationAsLinear_val, PureU1.Odd.P_P_P!_accCube', P_accCube, span_basis, P_P_P!_accCube, P_oddSnd, P_oddFst, P_linearACC, PureU1.Odd.lineInCubicPerm_swap, P'_val, P_oddMid
P! 📖	CompOp	8 math math: PureU1.Odd.parameterizationAsLinear_val, P!_linearACC, span_basis, P!_oddShiftZero, P!_oddShiftSnd, P!_oddShiftFst, P!'_val, P!_accCube
P!' 📖	CompOp	2 math math: Pa'_P'_P!', P!'_val
P' 📖	CompOp	2 math math: Pa'_P'_P!', P'_val
Pa 📖	CompOp	6 math math: Pa_oddShiftShiftSnd, Pa_eq, Pa_oddShiftShiftFst, Pa_oddShiftShiftMid, Pa_oddShiftShiftZero, Pa'_elim_eq_iff
Pa' 📖	CompOp	3 math math: Pa'_P'_P!', Pa'_eq, Pa'_elim_eq_iff
basis 📖	CompOp	2 math math: basis_val, basis_linear_independent
basis! 📖	CompOp	2 math math: basis!_val, basis!_linear_independent
basis!AsCharges 📖	CompOp	14 math math: basis!_val, PureU1.Odd.P_P_P!_accCube', basis!_on_oddShiftFst_self, basis!_on_oddShiftSnd_self, P_P_P!_accCube, basis!_on_oddShiftFst_other, swap!_as_add, basis!_on_other, basis!_on_oddShiftSnd_other, PureU1.Odd.lineInCubicPerm_swap, basis!_oddShiftSnd_eq_minus_oddShiftFst, span_basis_swap!, basis!_on_oddShiftZero, basis!_linearACC
basisAsCharges 📖	CompOp	9 math math: basis_val, basis_oddSnd_eq_minus_oddFst, basis_linearACC, basis_on_oddMid, basis_on_oddSnd_other, basis_on_oddFst_other, basis_on_oddSnd_self, basis_on_other, basis_on_oddFst_self
basisa 📖	CompOp	1 math math: basisa_linear_independent
basisaAsBasis 📖	CompOp	—
oddFst 📖	CompOp	7 math math: basis_oddSnd_eq_minus_oddFst, oddShiftShiftZero_eq_oddFst_zero, sum_odd, basis_on_oddFst_other, P_oddFst, oddShiftShiftFst_eq_oddFst_succ, basis_on_oddFst_self
oddMid 📖	CompOp	4 math math: basis_on_oddMid, oddShiftShiftMid_eq_oddMid, sum_odd, P_oddMid
oddShiftFst 📖	CompOp	11 math math: oddShiftShiftFst_eq_oddShiftFst_castSucc, sum_oddShift, PureU1.Odd.P_P_P!_accCube', basis!_on_oddShiftFst_self, P_P_P!_accCube, basis!_on_oddShiftFst_other, PureU1.Odd.lineInCubicPerm_last_cond, P!_oddShiftFst, oddShiftShiftMid_eq_oddShiftFst_last, PureU1.Odd.lineInCubicPerm_swap, basis!_oddShiftSnd_eq_minus_oddShiftFst
oddShiftShiftFst 📖	CompOp	3 math math: oddShiftShiftFst_eq_oddShiftFst_castSucc, Pa_oddShiftShiftFst, oddShiftShiftFst_eq_oddFst_succ
oddShiftShiftMid 📖	CompOp	3 math math: oddShiftShiftMid_eq_oddMid, Pa_oddShiftShiftMid, oddShiftShiftMid_eq_oddShiftFst_last
oddShiftShiftSnd 📖	CompOp	3 math math: oddShiftShiftSnd_eq_oddSnd, Pa_oddShiftShiftSnd, oddShiftShiftSnd_eq_oddShiftSnd
oddShiftShiftZero 📖	CompOp	3 math math: oddShiftShiftZero_eq_oddFst_zero, oddShiftShiftZero_eq_oddShiftZero, Pa_oddShiftShiftZero
oddShiftSnd 📖	CompOp	10 math math: sum_oddShift, PureU1.Odd.P_P_P!_accCube', basis!_on_oddShiftSnd_self, PureU1.Odd.lineInCubicPerm_last_cond, oddSnd_eq_oddShiftSnd, basis!_on_oddShiftSnd_other, P!_oddShiftSnd, PureU1.Odd.lineInCubicPerm_swap, basis!_oddShiftSnd_eq_minus_oddShiftFst, oddShiftShiftSnd_eq_oddShiftSnd
oddShiftZero 📖	CompOp	6 math math: sum_oddShift, PureU1.Odd.P_P_P!_accCube', oddShiftShiftZero_eq_oddShiftZero, PureU1.Odd.lineInCubicPerm_last_cond, P!_oddShiftZero, basis!_on_oddShiftZero
oddSnd 📖	CompOp	7 math math: oddShiftShiftSnd_eq_oddSnd, basis_oddSnd_eq_minus_oddFst, basis_on_oddSnd_other, sum_odd, oddSnd_eq_oddShiftSnd, P_oddSnd, basis_on_oddSnd_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
P!'_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 P!' P!	—	PureU1.sum_of_anomaly_free_linear PureU1.sum_of_charges
P!_accCube 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun PureU1.accCube P!	—	PureU1.accCube_explicit sum_oddShift P!_oddShiftZero P!_oddShiftFst P!_oddShiftSnd
P!_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav P!	—	PureU1.accGrav.eq_1 sum_oddShift P!_oddShiftZero P!_oddShiftFst P!_oddShiftSnd
P!_oddShiftFst 📖	mathematical	—	P! oddShiftFst	—	P!.eq_1 PureU1.sum_of_charges basis!_on_oddShiftFst_other basis!_on_oddShiftFst_self
P!_oddShiftSnd 📖	mathematical	—	P! oddShiftSnd	—	P!.eq_1 PureU1.sum_of_charges basis!_on_oddShiftSnd_other basis!_on_oddShiftSnd_self
P!_oddShiftZero 📖	mathematical	—	P! oddShiftZero	—	P!.eq_1 PureU1.sum_of_charges basis!_on_oddShiftZero
P!_zero 📖	—	P! ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	P!_oddShiftFst
P'_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 P' P	—	PureU1.sum_of_anomaly_free_linear PureU1.sum_of_charges
P_P_P!_accCube 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule TriLinearSymm TriLinearSymm.instFun PureU1.accCubeTriLinSymm P basis!AsCharges oddShiftFst	—	sum_oddShift basis!_on_oddShiftZero basis!_on_oddShiftFst_other basis!_on_oddShiftSnd_other basis!_on_oddShiftFst_self basis!_on_oddShiftSnd_self oddSnd_eq_oddShiftSnd P_oddSnd
P_accCube 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun PureU1.accCube P	—	PureU1.accCube_explicit sum_odd P_oddMid P_oddFst P_oddSnd
P_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav P	—	PureU1.accGrav.eq_1 sum_odd P_oddMid P_oddFst P_oddSnd
P_oddFst 📖	mathematical	—	P oddFst	—	P.eq_1 PureU1.sum_of_charges basis_on_oddFst_other basis_on_oddFst_self
P_oddMid 📖	mathematical	—	P oddMid	—	P.eq_1 PureU1.sum_of_charges basis_on_oddMid
P_oddSnd 📖	mathematical	—	P oddSnd	—	P.eq_1 PureU1.sum_of_charges basis_on_oddSnd_other basis_on_oddSnd_self
P_zero 📖	—	P ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	P_oddFst
Pa'_P'_P!' 📖	mathematical	—	Pa' ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemLinear.linSolsAddCommMonoid P' P!'	—	—
Pa'_elim_eq_iff 📖	mathematical	—	Pa' Pa	—	Pa'_eq ACCSystemLinear.LinSols.ext Pa'_P'_P!' P'_val P!'_val
Pa'_eq 📖	mathematical	—	Pa'	—	Pa'.eq_1 basisa_linear_independent
Pa_eq 📖	mathematical	—	Pa	—	Pa'_elim_eq_iff Pa'_eq
Pa_oddShiftShiftFst 📖	mathematical	—	Pa oddShiftShiftFst	—	Pa.eq_1 oddShiftShiftFst_eq_oddFst_succ oddShiftShiftFst_eq_oddShiftFst_castSucc P_oddFst P!_oddShiftFst
Pa_oddShiftShiftMid 📖	mathematical	—	Pa oddShiftShiftMid	—	Pa.eq_1 oddShiftShiftMid_eq_oddMid oddShiftShiftMid_eq_oddShiftFst_last P_oddMid P!_oddShiftFst
Pa_oddShiftShiftSnd 📖	mathematical	—	Pa oddShiftShiftSnd	—	Pa.eq_1 oddShiftShiftSnd_eq_oddSnd oddShiftShiftSnd_eq_oddShiftSnd P_oddSnd P!_oddShiftSnd
Pa_oddShiftShiftZero 📖	mathematical	—	Pa oddShiftShiftZero	—	Pa.eq_1 oddShiftShiftZero_eq_oddFst_zero oddShiftShiftZero_eq_oddShiftZero P_oddFst P!_oddShiftZero
Pa_zero 📖	—	Pa ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	Pa_oddShiftShiftZero Pa_oddShiftShiftSnd Pa_oddShiftShiftFst
Pa_zero! 📖	—	Pa ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	Pa_zero P!_zero P.eq_1 Pa.eq_1
basis!_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav basis!AsCharges	—	PureU1.accGrav.eq_1 sum_oddShift basis!_on_oddShiftZero basis!_oddShiftSnd_eq_minus_oddShiftFst
basis!_linear_independent 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis! ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	P!_zero P!'_val
basis!_oddShiftSnd_eq_minus_oddShiftFst 📖	mathematical	—	basis!AsCharges oddShiftSnd oddShiftFst	—	odd_shift_eq
basis!_on_oddShiftFst_other 📖	mathematical	—	basis!AsCharges oddShiftFst	—	odd_shift_eq
basis!_on_oddShiftFst_self 📖	mathematical	—	basis!AsCharges oddShiftFst	—	—
basis!_on_oddShiftSnd_other 📖	mathematical	—	basis!AsCharges oddShiftSnd	—	basis!_oddShiftSnd_eq_minus_oddShiftFst basis!_on_oddShiftFst_other
basis!_on_oddShiftSnd_self 📖	mathematical	—	basis!AsCharges oddShiftSnd	—	basis!_oddShiftSnd_eq_minus_oddShiftFst basis!_on_oddShiftFst_self
basis!_on_oddShiftZero 📖	mathematical	—	basis!AsCharges oddShiftZero	—	—
basis!_on_other 📖	mathematical	—	basis!AsCharges	—	—
basis!_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis! basis!AsCharges	—	—
basis_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav basisAsCharges	—	PureU1.accGrav.eq_1 sum_odd basis_on_oddMid basis_oddSnd_eq_minus_oddFst
basis_linear_independent 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	P_zero P'_val
basis_oddSnd_eq_minus_oddFst 📖	mathematical	—	basisAsCharges oddSnd oddFst	—	PureU1.split_odd
basis_on_oddFst_other 📖	mathematical	—	basisAsCharges oddFst	—	PureU1.split_odd
basis_on_oddFst_self 📖	mathematical	—	basisAsCharges oddFst	—	—
basis_on_oddMid 📖	mathematical	—	basisAsCharges oddMid	—	—
basis_on_oddSnd_other 📖	mathematical	—	basisAsCharges oddSnd	—	basis_oddSnd_eq_minus_oddFst basis_on_oddFst_other
basis_on_oddSnd_self 📖	mathematical	—	basisAsCharges oddSnd	—	basis_oddSnd_eq_minus_oddFst basis_on_oddFst_self
basis_on_other 📖	mathematical	—	basisAsCharges	—	—
basis_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis basisAsCharges	—	—
basisa_card 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	PureU1.BasisLinear.finrank_AnomalyFreeLinear
basisa_linear_independent 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basisa ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	Pa_zero Pa_zero! P'_val P!'_val Pa'_P'_P!'
oddShiftShiftFst_eq_oddFst_succ 📖	mathematical	—	oddShiftShiftFst oddFst	—	—
oddShiftShiftFst_eq_oddShiftFst_castSucc 📖	mathematical	—	oddShiftShiftFst oddShiftFst	—	—
oddShiftShiftMid_eq_oddMid 📖	mathematical	—	oddShiftShiftMid oddMid	—	—
oddShiftShiftMid_eq_oddShiftFst_last 📖	mathematical	—	oddShiftShiftMid oddShiftFst	—	—
oddShiftShiftSnd_eq_oddShiftSnd 📖	mathematical	—	oddShiftShiftSnd oddShiftSnd	—	—
oddShiftShiftSnd_eq_oddSnd 📖	mathematical	—	oddShiftShiftSnd oddSnd	—	—
oddShiftShiftZero_eq_oddFst_zero 📖	mathematical	—	oddShiftShiftZero oddFst	—	—
oddShiftShiftZero_eq_oddShiftZero 📖	mathematical	—	oddShiftShiftZero oddShiftZero	—	—
oddSnd_eq_oddShiftSnd 📖	mathematical	—	oddSnd oddShiftSnd	—	—
odd_shift_eq 📖	—	—	—	—	—
odd_shift_shift_eq 📖	—	—	—	—	—
span_basis 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid P P!	—	P'_val P!'_val basisa_linear_independent basisa_card
span_basis_swap! 📖	mathematical	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule ACCSystemGroupAction.group PureU1.FamilyPermutations ACCSystemGroupAction.instGroupGroup ACCSystemGroupAction.linSolRep oddShiftFst oddShiftSnd ACCSystemLinear.LinSols.val ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid P P!	ACCSystemCharges.ChargesAddCommGroup ACCSystemCharges.chargesModule basis!AsCharges	—	swap!_as_add
sum_odd 📖	mathematical	—	oddMid oddFst oddSnd	—	PureU1.split_odd
sum_oddShift 📖	mathematical	—	oddShiftZero oddShiftFst oddShiftSnd	—	odd_shift_eq
swap!_as_add 📖	mathematical	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule ACCSystemGroupAction.group PureU1.FamilyPermutations ACCSystemGroupAction.instGroupGroup ACCSystemGroupAction.linSolRep oddShiftFst oddShiftSnd	ACCSystemLinear.LinSols.val ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.ChargesAddCommGroup ACCSystemCharges.chargesModule basis!AsCharges	—	PureU1.FamilyPermutations_anomalyFreeLinear_apply basis!_on_oddShiftFst_self basis!_on_oddShiftSnd_self basis!_on_other

---

← Back to Index