Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.voter-readings

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/voter_readings.clj0 definitions, 2 theorems

General lemmas: voter readings. The mathematical facts the corresponding checks rest on, each checked by the kernel.

Depends onmath.sums.value-appendmath.nat.infinitemath.rational.nnrat.identitiesmath.nat.at-most-cancellationmath.rational.nnrat.order-equivalencemath.rational.nnrat.archimedeanmath.rational.nnrat.add-monotonemath.rational.nnrat.add-cancellationmath.rational.nnrat.additive-reassociationmath.rational.signed.order-transitivitymath.rational.signed.convergencemath.rational.signed.order-respectsmath.rational.signed.limit-uniquenessmath.rational.signed.strict-ordermath.rational.signed.multiplymath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociationmath.rational.nnrat.distribute-rightmath.rational.nnrat.ringmath.rational.nnrat.multiply-monotonemath.rational.nnrat.order-differencemath.rational.signed.multiply-ordermath.rational.signed.equivalence-lawsmath.rational.nnrat.minmaxmath.rational.nnrat.farkas-elim-listmath.rational.signed.no-zero-divisorsmath.rational.signed.decide-ordermath.rational.signed.decide-reflexivemath.logic.boolean-andmath.rational.signed.decide-equivalencemath.rational.signed.decide-completenessmath.rational.signed.unit-lawsmath.nat.strict-below-splitmath.nat.strict-below-moremath.checksmath.nat.at-most-addmath.rational.nnrat.harmonic-convergencemath.nat.divmodmath.rational.signed.minmaxmath.rational.signed.minmax-algebramath.rational.signed.clampmath.rational.signed.deviation-rowsmath.rational.signed.absolutemath.rational.signed.absolute-algebramath.rational.signed.distancemath.nat.linear-ordermath.rational.signed.add-associativemath.nat.semiringmath.nat.multiply-zero-splitmath.rational.nnrat.multiply-zero-splitmath.nat.monusmath.rational.nnrat.monusmath.rational.nnrat.add-zero-splitmath.rational.nnrat.add-cancel-zeromath.finite.rational-argmaxmath.rational.nnrat.order-totalmath.rational.nnrat.multiply-difference-zeromath.linear.vector.norm-nonnegativemath.linear.vector.norm-zero-reflectionalgorithms.proofs.counterfactual-distance-separationalgorithms.proofs.counterfactual-distance-lawsmath.finite.matrixmath.linear.matrix.equivalencemath.linear.matrix.transposemath.linear.matrix.transpose-equivalencemath.linear.matrix.multiplymath.linear.matrix.multiply-shapemath.linear.matrix.composablemath.linear.matrix.composable-multiplymath.linear.vector.additive-unitsmath.linear.vector.shape-cancellationmath.linear.vector.shape-mapmath.linear.vector.shape-addmath.linear.vector.dot-additivemath.linear.vector.dot-bilinearmath.linear.vector.dot-negatemath.linear.vector.dot-subtractmath.linear.vector.dot-scalemath.linear.matrix.action-scalemath.rational.signed.multiply-nonzeromath.rational.signed.order-monotonemath.rational.signed.list-summath.rational.signed.multiply-monotonemath.rational.signed.map-sum-algebramath.rational.signed.negate-additivemath.rational.signed.lp-objective-negatemath.nat.pair-index-inversemath.sums.flow-cutmath.sums.nonneg-zeromath.rational.signed.multiply-ringmath.rational.signed.distributivemath.linear.matrix.row-length-shapemath.linear.matrix.row-length-decidermath.rational.signed.structural-equalitymath.linear.vector.equivalencemath.linear.vector.uniform-clampmath.linear.vector.pointwise-ordermath.linear.matrix.action-prependmath.linear.matrix.action-associativemath.linear.matrix.transpose-multiplymath.linear.matrix.transpose-shapemath.linear.matrix.transpose-involutionmath.linear.matrix.transpose-involution-positivemath.linear.matrix.transpose-multiply-reversemath.linear.matrix.composable-transposemath.linear.matrix.associativity-counterexamplemath.linear.matrix.signed-scalemath.linear.matrix.signed-scale-rightmath.linear.matrix.addmath.linear.matrix.add-shapemath.linear.matrix.prepend-addmath.linear.matrix.add-rightmath.linear.matrix.add-algebramath.linear.matrix.additive-groupmath.linear.matrix.negate-linearmath.linear.matrix.subtract-linearmath.linear.matrix.signed-scale-algebramath.linear.matrix.signed-scale-unitsmath.linear.matrix.signed-scale-congruencemath.linear.matrix.signed-scale-subtractmath.rational.signed.distance-multiply-nonnegativemath.rational.signed.vector-sup-distancealgorithms.proofs.inner-productmath.rational.signed.distance-trianglemath.rational.signed.distance-translationmath.rational.signed.distance-additivemath.linear.vector.dot-distance-boundmath.linear.vector.row-sum-lipschitzmath.linear.matrix.action-sup-boundmath.linear.matrix.signed-scale-ordermath.linear.matrix.pointwise-order-lawsmath.linear.matrix.signed-scale-antitonemath.linear.matrix.add-ordermath.linear.matrix.signed-scale-positivemath.linear.matrix.signed-scale-signmath.linear.matrix.positive-actionmath.linear.matrix.transpose-ordermath.linear.matrix.positive-multiplymath.linear.matrix.gram-positivemath.linear.matrix.gram-kernelmath.linear.matrix.row-grammath.linear.matrix.row-gram-kernelmath.linear.vector.norm-pythagoreanmath.linear.matrix.least-squares-normalmath.linear.matrix.least-squares-equalitymath.linear.matrix.mixed-sign-actionmath.linear.matrix.mixed-sign-multiplymath.linear.matrix.antitonemath.linear.matrix.interval-ordermath.linear.matrix.affine-ordermath.linear.matrix.linearmath.rational.signed.vector-sup-congruencemath.finite.vectormath.linear.vector.pointwise-order-lawsmath.linear.vector.add-ordermath.rational.signed.vector-sup-translationmath.linear.matrix.affine-sup-distancemath.linear.matrix.row-sum-lipschitzmath.linear.matrix.row-sum-fixed-point-uniquenessmath.linear.matrix.half-row-sum-fixed-point-uniquenessmath.linear.matrix.affine-half-iterate-contractionmath.linear.matrix.affine-half-iterate-ratemath.rational.signed.geometric-bridgemath.linear.matrix.affine-half-iterate-convergesmath.linear.matrix.affine-strong-row-contractionmath.linear.matrix.affine-residual-certificatemath.linear.matrix.affine-inverse-gap-certificatemath.linear.matrix.affine-general-rate-certificatemath.sums.of-natmath.lemmas.one-center

signed/max-select-cases :
  (mz-x mz-y : ℚ)
  → proposition/conjunction (mz-x ≤ data/Bool.rec (fun x₄₈ => ℚ) mz-x mz-y (signed/decide-at-most mz-x mz-y)) (proposition/conjunction (mz-y ≤ data/Bool.rec (fun x₇₂ => ℚ) mz-x mz-y (signed/decide-at-most mz-x mz-y)) (proposition/disjunction (data/Bool.rec (fun x₈₄ => ℚ) mz-x mz-y (signed/decide-at-most mz-x mz-y) = mz-x) (data/Bool.rec (fun x₈₈ => ℚ) mz-x mz-y (signed/decide-at-most mz-x mz-y) = mz-y)))

signed/voter-cell :
  (vc-a vc-b vc-c vc-m vc-s vc-f vc-T : ℚ)
  (vc-hm : vc-m = data/Bool.rec (fun x₁₅₂ => ℚ) (data/Bool.rec (fun x₁₅₆ => ℚ) vc-b vc-a (signed/decide-at-most vc-a vc-b)) (data/Bool.rec (fun x₁₇₆ => ℚ) vc-c (data/Bool.rec (fun x₁₈₀ => ℚ) vc-a vc-b (signed/decide-at-most vc-a vc-b)) (signed/decide-at-most (data/Bool.rec (fun x₁₈₈ => ℚ) vc-a vc-b (signed/decide-at-most vc-a vc-b)) vc-c)) (signed/decide-at-most (data/Bool.rec (fun x₂₂₈ => ℚ) vc-b vc-a (signed/decide-at-most vc-a vc-b)) (data/Bool.rec (fun x₂₄₈ => ℚ) vc-c (data/Bool.rec (fun x₂₅₂ => ℚ) vc-a vc-b (signed/decide-at-most vc-a vc-b)) (signed/decide-at-most (data/Bool.rec (fun x₂₆₀ => ℚ) vc-a vc-b (signed/decide-at-most vc-a vc-b)) vc-c))))
  (vc-hs : vc-s = data/Bool.rec (fun x₂₈₀ => ℚ) vc-a (data/Bool.rec (fun x₂₈₄ => ℚ) vc-b vc-c (signed/decide-at-most vc-b vc-c)) (signed/decide-at-most vc-a (data/Bool.rec (fun x₂₉₂ => ℚ) vc-b vc-c (signed/decide-at-most vc-b vc-c))) + signed/negate (data/Bool.rec (fun x₃₁₆ => ℚ) (data/Bool.rec (fun x₃₂₀ => ℚ) vc-c vc-b (signed/decide-at-most vc-b vc-c)) vc-a (signed/decide-at-most vc-a (data/Bool.rec (fun x₃₂₈ => ℚ) vc-c vc-b (signed/decide-at-most vc-b vc-c)))))
  (vc-hf : vc-f = data/Bool.rec (fun x₃₃₂ => ℚ) 0 1 (signed/decide-at-most vc-s vc-T))
  → proposition/conjunction (disjunction) (proposition/conjunction (data/Bool.rec (fun x₃₇₂ => ℚ) vc-b vc-a (signed/decide-at-most vc-a vc-b) ≤ vc-m) (proposition/conjunction (vc-m ≤ data/Bool.rec (fun x₃₈₀ => ℚ) vc-a vc-b (signed/decide-at-most vc-a vc-b)) (conjunction)))
  where conjunction := proposition/conjunction (0 ≤ vc-s) (proposition/disjunction (proposition/conjunction (vc-s ≤ vc-T) (vc-f = 1)) (proposition/conjunction (vc-T < vc-s) (vc-f = 0)))
  where disjunction := proposition/disjunction (vc-m = vc-a) (proposition/disjunction (vc-m = vc-b) (vc-m = vc-c))