ConstAbs

📁 Source: PhysLean/QFT/QED/AnomalyCancellation/ConstAbs.lean

Statistics

Metric	Count
Definitions ConstAbs, ConstAbsProp, ConstAbsSorted, Boundary, HasBoundary	5
Theorems boundary_value_even, boundary_value_odd, AFL_even_Boundary, AFL_even_above, AFL_even_above', AFL_even_below, AFL_even_below', AFL_hasBoundary, AFL_odd, AFL_odd_noBoundary, AFL_odd_zero, boundary_accGrav', boundary_accGrav'', boundary_castSucc, boundary_split, boundary_succ, gt_eq, is_zero, lt_eq, not_hasBoundary_grav, not_hasBoundary_zero_le, not_hasBoundry_zero, opposite_signs_eq_neg, val_le_zero, zero_gt, constAbs_perm, constAbs_sort	27
Total	32

PureU1

Definitions

Name	Category	Theorems
ConstAbs 📖	MathDef	6 math math: Odd.lineInCubicPerm_constAbs, linesInPlane_constAbs_four, Even.lineInCubicPerm_constAbs, linesInPlane_constAbs_AF, linesInPlane_constAbs, constAbs_perm
ConstAbsProp 📖	MathDef	4 math math: linesInPlane_four, linesInPlane_eq_sq, linesInPlane_eq_sq_four, lineInPlaneCond_eq_last
ConstAbsSorted 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constAbs_perm 📖	mathematical	—	ConstAbs ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule ACCSystemGroupAction.group FamilyPermutations ACCSystemGroupAction.groupInst ACCSystemGroupAction.rep	—	—
constAbs_sort 📖	mathematical	ConstAbs	sort	—	sort.eq_1 constAbs_perm

PureU1.ConstAbs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundary_value_even 📖	mathematical	PureU1.ConstAbs ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	PureU1.VectorLikeEven	—	PureU1.constAbs_sort PureU1.sort_sorted PureU1.split_equal PureU1.ConstAbsSorted.AFL_even_above PureU1.sortAFL_val
boundary_value_odd 📖	mathematical	PureU1.ConstAbs ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemLinear.LinSols ACCSystemLinear.linSolsAddCommGroup	—	PureU1.constAbs_sort PureU1.sort_sorted PureU1.sortAFL_zero PureU1.ConstAbsSorted.AFL_odd

PureU1.ConstAbsSorted

Definitions

Name	Category	Theorems
Boundary 📖	MathDef	—
HasBoundary 📖	MathDef	2 math math: AFL_odd_noBoundary, AFL_hasBoundary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AFL_even_Boundary 📖	—	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 Boundary	—	—	boundary_accGrav'' pureU1_linear
AFL_even_above 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges PureU1.split_equal	—	PureU1.split_equal is_zero AFL_even_above'
AFL_even_above' 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges PureU1.split_equal	—	PureU1.split_equal AFL_hasBoundary boundary_succ gt_eq AFL_even_Boundary
AFL_even_below 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges PureU1.split_equal	—	PureU1.split_equal is_zero AFL_even_below'
AFL_even_below' 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges PureU1.split_equal	—	PureU1.split_equal AFL_hasBoundary boundary_castSucc lt_eq AFL_even_Boundary
AFL_hasBoundary 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	HasBoundary	—	not_hasBoundary_grav pureU1_linear
AFL_odd 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	ACCSystemLinear.LinSols ACCSystemLinear.linSolsAddCommGroup	—	ACCSystemLinear.LinSols.ext is_zero AFL_odd_zero
AFL_odd_noBoundary 📖	mathematical	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	HasBoundary	—	boundary_accGrav'' pureU1_linear
AFL_odd_zero 📖	—	PureU1.ConstAbsSorted ACCSystemLinear.LinSols.val ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1	—	—	AFL_odd_noBoundary AFL_hasBoundary
boundary_accGrav' 📖	mathematical	—	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav ACCSystemCharges.numberCharges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 boundary_split	—	boundary_split
boundary_accGrav'' 📖	mathematical	PureU1.ConstAbsSorted Boundary	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav	—	boundary_split boundary_accGrav' lt_eq gt_eq boundary_castSucc boundary_succ
boundary_castSucc 📖	—	PureU1.ConstAbsSorted Boundary	—	—	lt_eq
boundary_split 📖	—	—	—	—	—
boundary_succ 📖	—	PureU1.ConstAbsSorted Boundary	—	—	boundary_castSucc opposite_signs_eq_neg
gt_eq 📖	—	PureU1.ConstAbsSorted	—	—	—
is_zero 📖	mathematical	PureU1.ConstAbsSorted	ACCSystemCharges.Charges ACCSystemLinear.toACCSystemCharges ACCSystemQuad.toACCSystemLinear ACCSystem.toACCSystemQuad PureU1 ACCSystemCharges.ChargesAddCommGroup	—	—
lt_eq 📖	—	PureU1.ConstAbsSorted	—	—	—
not_hasBoundary_grav 📖	mathematical	PureU1.ConstAbsSorted HasBoundary	ACCSystemCharges.Charges PureU1.PureU1Charges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule PureU1.accGrav	—	not_hasBoundry_zero
not_hasBoundary_zero_le 📖	—	PureU1.ConstAbsSorted HasBoundary	—	—	val_le_zero
not_hasBoundry_zero 📖	—	PureU1.ConstAbsSorted HasBoundary	—	—	not_hasBoundary_zero_le zero_gt
opposite_signs_eq_neg 📖	—	PureU1.ConstAbsSorted	—	—	—
val_le_zero 📖	—	PureU1.ConstAbsSorted	—	—	lt_eq
zero_gt 📖	—	PureU1.ConstAbsSorted	—	—	gt_eq

---

← Back to Index