BasisLinear

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

Statistics

Metric	Count
Definitions P, P!, P!', P', Pa, Pa', basis, basis!, basis!AsCharges, basisAsCharges, basisa, basisaAsBasis, evenFst, evenShiftFst, evenShiftLast, evenShiftSnd, evenShiftZero, evenSnd	18
Theorems P!'_val, P!_accCube, P!_evenShiftFst, P!_evenShiftLast, P!_evenShiftSnd, P!_evenShiftZero, P!_in_span, P!_zero, P'_val, P_P!_P!_accCube, P_P_P!_accCube, P_accCube, P_evenFst, P_evenSnd, P_evenSnd_evenFst, P_linearACC, P_zero, Pa'_P'_P!', Pa'_elim_eq_iff, Pa'_eq, Pa_eq, Pa_evenShiftFst, Pa_evenShiftLast, Pa_evenShiftSnd, Pa_evenShitZero, Pa_zero, Pa_zero!, basis!_accCube, basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_linearACC, basis!_linear_independent, basis!_on_evenShiftFst_other, basis!_on_evenShiftFst_self, basis!_on_evenShiftLast, basis!_on_evenShiftSnd_other, basis!_on_evenShiftSnd_self, basis!_on_evenShiftZero, basis!_on_other, basis!_val, basis_accCube, basis_evenSnd_eq_neg_evenFst, basis_linearACC, basis_linear_independent, basis_on_evenFst_other, basis_on_evenFst_self, basis_on_evenSnd_other, basis_on_evenSnd_self, basis_on_other, basis_val, basisa_card, basisa_linear_independent, evenShiftFst_eq_evenFst_succ, evenShiftLast_eq_evenSnd_last, evenShiftSnd_eq_evenSnd_castSucc, evenShiftZero_eq_evenFst_zero, ext_even, n_cond₂, smul_basis!AsCharges_in_span, span_basis, span_basis_swap!, sum_even, sum_evenShift, swap!_as_add, vectorLikeEven_in_span	64
Total	82

PureU1.VectorLikeEvenPlane

Definitions

Name	Category	Theorems
P 📖	CompOp	12 math math: PureU1.Even.lineInCubicPerm_swap, P_evenSnd_evenFst, P_evenFst, P'_val, P_linearACC, PureU1.Even.parameterizationAsLinear_val, P_P_P!_accCube, P_accCube, P_evenSnd, PureU1.Even.P_P_P!_accCube', span_basis, PureU1.Even.lineInCubic_expand
P! 📖	CompOp	11 math math: P!_evenShiftZero, P!_evenShiftSnd, PureU1.Even.parameterizationAsLinear_val, P!_evenShiftFst, P!_evenShiftLast, P!'_val, P!_in_span, P!_accCube, P_P!_P!_accCube, span_basis, PureU1.Even.lineInCubic_expand
P!' 📖	CompOp	2 math math: P!'_val, Pa'_P'_P!'
P' 📖	CompOp	2 math math: P'_val, Pa'_P'_P!'
Pa 📖	CompOp	6 math math: Pa_evenShiftFst, Pa_evenShiftSnd, Pa'_elim_eq_iff, Pa_eq, Pa_evenShiftLast, Pa_evenShitZero
Pa' 📖	CompOp	3 math math: Pa'_eq, Pa'_elim_eq_iff, Pa'_P'_P!'
basis 📖	CompOp	5 math math: basis_val, vectorLikeEven_in_span, PureU1.Even.lineInCubicPerm_in_plane, PureU1.Even.special_case, basis_linear_independent
basis! 📖	CompOp	2 math math: basis!_linear_independent, basis!_val
basis!AsCharges 📖	CompOp	18 math math: basis!_on_evenShiftFst_self, PureU1.Even.lineInCubicPerm_swap, basis!_linearACC, basis!_on_evenShiftZero, basis!_on_evenShiftFst_other, basis!_on_evenShiftSnd_other, P_P_P!_accCube, P!_in_span, span_basis_swap!, basis!_accCube, smul_basis!AsCharges_in_span, swap!_as_add, basis!_evenShftSnd_eq_neg_evenShiftFst, basis!_val, basis!_on_other, basis!_on_evenShiftLast, PureU1.Even.P_P_P!_accCube', basis!_on_evenShiftSnd_self
basisAsCharges 📖	CompOp	10 math math: basis_on_evenSnd_other, basis_evenSnd_eq_neg_evenFst, basis_on_evenFst_other, basis_on_evenSnd_self, basis_val, basis_accCube, basis_on_evenFst_self, P_P!_P!_accCube, basis_linearACC, basis_on_other
basisa 📖	CompOp	1 math math: basisa_linear_independent
basisaAsBasis 📖	CompOp	—
evenFst 📖	CompOp	9 math math: sum_even, basis_evenSnd_eq_neg_evenFst, evenShiftZero_eq_evenFst_zero, P_evenSnd_evenFst, basis_on_evenFst_other, P_evenFst, evenShiftFst_eq_evenFst_succ, basis_on_evenFst_self, P_P!_P!_accCube
evenShiftFst 📖	CompOp	11 math math: basis!_on_evenShiftFst_self, PureU1.Even.lineInCubicPerm_swap, Pa_evenShiftFst, basis!_on_evenShiftFst_other, P!_evenShiftFst, evenShiftFst_eq_evenFst_succ, sum_evenShift, PureU1.Even.lineInCubicPerm_last_cond, smul_basis!AsCharges_in_span, basis!_evenShftSnd_eq_neg_evenShiftFst, PureU1.Even.P_P_P!_accCube'
evenShiftLast 📖	CompOp	7 math math: evenShiftLast_eq_evenSnd_last, P!_evenShiftLast, sum_evenShift, PureU1.Even.lineInCubicPerm_last_cond, Pa_evenShiftLast, basis!_on_evenShiftLast, PureU1.Even.P_P_P!_accCube'
evenShiftSnd 📖	CompOp	11 math math: PureU1.Even.lineInCubicPerm_swap, basis!_on_evenShiftSnd_other, P!_evenShiftSnd, Pa_evenShiftSnd, evenShiftSnd_eq_evenSnd_castSucc, sum_evenShift, PureU1.Even.lineInCubicPerm_last_cond, smul_basis!AsCharges_in_span, basis!_evenShftSnd_eq_neg_evenShiftFst, PureU1.Even.P_P_P!_accCube', basis!_on_evenShiftSnd_self
evenShiftZero 📖	CompOp	5 math math: evenShiftZero_eq_evenFst_zero, basis!_on_evenShiftZero, P!_evenShiftZero, sum_evenShift, Pa_evenShitZero
evenSnd 📖	CompOp	9 math math: sum_even, basis_on_evenSnd_other, basis_evenSnd_eq_neg_evenFst, P_evenSnd_evenFst, basis_on_evenSnd_self, evenShiftLast_eq_evenSnd_last, evenShiftSnd_eq_evenSnd_castSucc, P_evenSnd, P_P!_P!_accCube

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_evenShift P!_evenShiftZero P!_evenShiftLast P!_evenShiftFst P!_evenShiftSnd
P!_evenShiftFst 📖	mathematical	—	P! evenShiftFst	—	P!.eq_1 PureU1.sum_of_charges basis!_on_evenShiftFst_other basis!_on_evenShiftFst_self
P!_evenShiftLast 📖	mathematical	—	P! evenShiftLast	—	P!.eq_1 PureU1.sum_of_charges basis!_on_evenShiftLast
P!_evenShiftSnd 📖	mathematical	—	P! evenShiftSnd	—	P!.eq_1 PureU1.sum_of_charges basis!_on_evenShiftSnd_other basis!_on_evenShiftSnd_self
P!_evenShiftZero 📖	mathematical	—	P! evenShiftZero	—	P!.eq_1 PureU1.sum_of_charges basis!_on_evenShiftZero
P!_in_span 📖	mathematical	—	ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule basis!AsCharges P!	—	—
P!_zero 📖	—	P! ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	P!_evenShiftFst
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! basisAsCharges evenFst evenSnd	—	TriLinearSymm.mk₃.congr_simp sum_even basis_on_evenFst_other basis_on_evenSnd_other basis_on_evenFst_self basis_on_evenSnd_self
P_P_P!_accCube 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule TriLinearSymm TriLinearSymm.instFun PureU1.accCubeTriLinSymm P basis!AsCharges	—	TriLinearSymm.mk₃.congr_simp sum_evenShift basis!_on_evenShiftZero basis!_on_evenShiftLast basis!_on_evenShiftFst_other basis!_on_evenShiftSnd_other basis!_on_evenShiftFst_self basis!_on_evenShiftSnd_self evenShiftFst_eq_evenFst_succ evenShiftSnd_eq_evenSnd_castSucc P_evenFst P_evenSnd
P_accCube 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun PureU1.accCube P	—	PureU1.accCube_explicit sum_even P_evenFst P_evenSnd
P_evenFst 📖	mathematical	—	P evenFst	—	P.eq_1 PureU1.sum_of_charges basis_on_evenFst_other basis_on_evenFst_self
P_evenSnd 📖	mathematical	—	P evenSnd	—	P.eq_1 PureU1.sum_of_charges basis_on_evenSnd_other basis_on_evenSnd_self
P_evenSnd_evenFst 📖	mathematical	—	ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 P evenSnd evenFst	—	P_evenFst P_evenSnd
P_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav P	—	PureU1.accGrav.eq_1 sum_even P_evenFst P_evenSnd
P_zero 📖	—	P ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	P_evenFst
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_evenShiftFst 📖	mathematical	—	Pa evenShiftFst	—	Pa.eq_1 P!_evenShiftFst evenShiftFst_eq_evenFst_succ P_evenFst
Pa_evenShiftLast 📖	mathematical	—	Pa evenShiftLast	—	Pa.eq_1 P!_evenShiftLast evenShiftLast_eq_evenSnd_last P_evenSnd
Pa_evenShiftSnd 📖	mathematical	—	Pa evenShiftSnd	—	Pa.eq_1 P!_evenShiftSnd evenShiftSnd_eq_evenSnd_castSucc P_evenSnd
Pa_evenShitZero 📖	mathematical	—	Pa evenShiftZero	—	Pa.eq_1 P!_evenShiftZero evenShiftZero_eq_evenFst_zero P_evenFst
Pa_zero 📖	—	Pa ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—	Pa_evenShitZero Pa_evenShiftFst Pa_evenShiftSnd
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!_accCube 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun PureU1.accCube basis!AsCharges	—	PureU1.accCube_explicit sum_evenShift basis!_on_evenShiftLast basis!_on_evenShiftZero basis!_evenShftSnd_eq_neg_evenShiftFst
basis!_evenShftSnd_eq_neg_evenShiftFst 📖	mathematical	—	basis!AsCharges evenShiftSnd evenShiftFst	—	n_cond₂
basis!_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav basis!AsCharges	—	PureU1.accGrav.eq_1 sum_evenShift basis!_on_evenShiftZero basis!_on_evenShiftLast basis!_evenShftSnd_eq_neg_evenShiftFst
basis!_linear_independent 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis! ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	P!_zero P!'_val
basis!_on_evenShiftFst_other 📖	mathematical	—	basis!AsCharges evenShiftFst	—	n_cond₂
basis!_on_evenShiftFst_self 📖	mathematical	—	basis!AsCharges evenShiftFst	—	—
basis!_on_evenShiftLast 📖	mathematical	—	basis!AsCharges evenShiftLast	—	—
basis!_on_evenShiftSnd_other 📖	mathematical	—	basis!AsCharges evenShiftSnd	—	basis!_evenShftSnd_eq_neg_evenShiftFst basis!_on_evenShiftFst_other
basis!_on_evenShiftSnd_self 📖	mathematical	—	basis!AsCharges evenShiftSnd	—	basis!_evenShftSnd_eq_neg_evenShiftFst basis!_on_evenShiftFst_self
basis!_on_evenShiftZero 📖	mathematical	—	basis!AsCharges evenShiftZero	—	n_cond₂
basis!_on_other 📖	mathematical	—	basis!AsCharges	—	—
basis!_val 📖	mathematical	—	ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis! basis!AsCharges	—	—
basis_accCube 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun PureU1.accCube basisAsCharges	—	PureU1.accCube_explicit sum_even basis_evenSnd_eq_neg_evenFst
basis_evenSnd_eq_neg_evenFst 📖	mathematical	—	basisAsCharges evenSnd evenFst	—	—
basis_linearACC 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav basisAsCharges	—	PureU1.accGrav.eq_1 sum_even basis_evenSnd_eq_neg_evenFst
basis_linear_independent 📖	mathematical	—	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 basis ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule	—	P_zero P'_val
basis_on_evenFst_other 📖	mathematical	—	basisAsCharges evenFst	—	—
basis_on_evenFst_self 📖	mathematical	—	basisAsCharges evenFst	—	—
basis_on_evenSnd_other 📖	mathematical	—	basisAsCharges evenSnd	—	basis_evenSnd_eq_neg_evenFst basis_on_evenFst_other
basis_on_evenSnd_self 📖	mathematical	—	basisAsCharges evenSnd	—	basis_evenSnd_eq_neg_evenFst basis_on_evenFst_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 PureU1.split_odd
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!'
evenShiftFst_eq_evenFst_succ 📖	mathematical	—	evenShiftFst evenFst	—	evenFst.eq_1 n_cond₂ evenShiftFst.eq_1
evenShiftLast_eq_evenSnd_last 📖	mathematical	—	evenShiftLast evenSnd	—	—
evenShiftSnd_eq_evenSnd_castSucc 📖	mathematical	—	evenShiftSnd evenSnd	—	evenSnd.eq_1 n_cond₂ evenShiftSnd.eq_1
evenShiftZero_eq_evenFst_zero 📖	mathematical	—	evenShiftZero evenFst	—	—
ext_even 📖	—	evenFst evenSnd	—	—	—
n_cond₂ 📖	—	—	—	—	—
smul_basis!AsCharges_in_span 📖	mathematical	—	ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule basis!AsCharges ACCSystemCharges.ChargesAddCommGroup ACCSystemLinear.LinSols.val evenShiftSnd evenShiftFst	—	—
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 evenShiftFst evenShiftSnd ACCSystemLinear.LinSols.val ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid P P!	ACCSystemCharges.ChargesAddCommGroup ACCSystemCharges.chargesModule basis!AsCharges	—	P!_in_span smul_basis!AsCharges_in_span swap!_as_add
sum_even 📖	mathematical	—	evenFst evenSnd	—	PureU1.split_equal
sum_evenShift 📖	mathematical	—	evenShiftZero evenShiftLast evenShiftFst evenShiftSnd	—	n_cond₂
swap!_as_add 📖	mathematical	ACCSystemLinear.LinSols ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule ACCSystemGroupAction.group PureU1.FamilyPermutations ACCSystemGroupAction.instGroupGroup ACCSystemGroupAction.linSolRep evenShiftFst evenShiftSnd	ACCSystemLinear.LinSols.val ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.ChargesAddCommGroup ACCSystemCharges.chargesModule basis!AsCharges	—	PureU1.FamilyPermutations_anomalyFreeLinear_apply basis!_on_evenShiftFst_self basis!_on_evenShiftSnd_self basis!_on_other
vectorLikeEven_in_span 📖	mathematical	PureU1.VectorLikeEven ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemLinear.LinSols ACCSystemLinear.linSolsAddCommMonoid ACCSystemLinear.linSolsModule basis ACCSystemGroupAction.group PureU1.FamilyPermutations ACCSystemGroupAction.instGroupGroup ACCSystemGroupAction.linSolRep	—	ACCSystemLinear.LinSols.ext PureU1.sortAFL_val P'_val ext_even P_evenFst P_evenSnd PureU1.split_equal

---

← Back to Index