Skip to content

AUDIT_LEDGER.md

Latest commit

 

History

History
531 lines (504 loc) · 56 KB

AUDIT_LEDGER.md

File metadata and controls

531 lines (504 loc) · 56 KB
Raw

ArkLib proof-debt ledger (generated by scripts/audit_ledger.py)

Goal: zero sorry/admit, zero axiom, zero native_decide, and every Residual/CONJECTURE-named surface either proven, deleted, or honestly documented as open research with the paper trail.

subsystem sorry/admit native_decide axioms residual-named
MCACapacityTrivial 0 0 0 1
MCAGSRefutationCore 0 0 0 1
ResidualAxioms 0 0 0 2
ToMathlib 0 0 0 69
ProofSystem/Logup 0 0 0 51
ProofSystem/Whir 0 0 0 25
ProofSystem/Stir 0 0 0 3
ProofSystem/Spartan 0 0 0 5
ProofSystem/Sumcheck 0 0 0 1
Data/CodingTheory 0 0 0 196
OracleReduction/Composition 0 0 0 46
OracleReduction/FiatShamir 0 0 0 61
TOTAL 0 0 0 461

Data/CodingTheory

residual-named declarations

  • ArkLib/Data/CodingTheory/AGL24EvalToSymbolic.lean:98 theorem symbolicFullRankResidual_of_evaluated_witness
  • ArkLib/Data/CodingTheory/AGL24ExtensionLift.lean:46 theorem symbolicFullRankResidual_of_extension
  • ArkLib/Data/CodingTheory/AGL24FrankInterface.lean:154 theorem frankOrientationResidual_of_rootedOutCutTheorem
  • ArkLib/Data/CodingTheory/AGL24GMMDSInterface.lean:74 theorem gmmDsResidual_of_dualZeroPatternTheorem
  • ArkLib/Data/CodingTheory/AGL24GrandAssembly.lean:42 def FrankOrientationResidual
  • ArkLib/Data/CodingTheory/AGL24GrandAssembly.lean:54 def GMMDSResidual
  • ArkLib/Data/CodingTheory/AGL24SymbolicRank.lean:45 def SymbolicFullRankResidual
  • ArkLib/Data/CodingTheory/AGL24UnionBound.lean:88 def RIMFullRankFailureProbResidual
  • ArkLib/Data/CodingTheory/ProximityGap/141Math.lean:187 def epsMCAgsPrizeUniformConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/141Progress.lean:78 theorem epsMCA_le_mcaConjectureBound_of_one_le_bound
  • ArkLib/Data/CodingTheory/ProximityGap/141Progress.lean:116 theorem mcaConjecture_iff_abstractRSMcaPolyBound
  • ArkLib/Data/CodingTheory/ProximityGap/141Progress.lean:121 theorem mcaConjecture_of_abstractRSMcaPolyBound
  • ArkLib/Data/CodingTheory/ProximityGap/141Progress.lean:126 theorem abstractRSMcaPolyBound_of_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/141UniformResolved.lean:126 def epsMCAgsPrizeUniversalConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/141UniformResolved.lean:150 theorem epsMCA_le_of_universalGSConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/141UniformResolved.lean:205 theorem epsMCAgsPrizeUniversalConjecture_of_UniversalGSListMassBound
  • ArkLib/Data/CodingTheory/ProximityGap/141UniformVacuity.lean:36 theorem epsMCAgsPrizeUniformConjecture_holds_as_stated
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardLatticeSlice.lean:131 def BoundaryCardLatticeSubResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardLatticeSlice.lean:157 theorem subResiduals_iff_latticeData
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardLatticeSlice.lean:180 theorem boundaryCardLatticeResidual_of_subResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardLatticeSlice.lean:194 theorem boundaryProbabilityResidual_of_subResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardLatticeSlice.lean:223 theorem latticeResidual_target_is_boundary_good_set
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:236 theorem boundaryCardResidual_of_not_lattice
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:271 def BoundaryCardLatticeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:395 theorem boundaryCardLatticeResidual_zero
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:417 def BoundaryCardQuantizationResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:424 theorem BoundaryCardQuantizationResiduals.ofStrictInterior_zero
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:433 theorem BoundaryCardQuantizationResiduals.strictInterior
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:441 theorem BoundaryCardQuantizationResiduals.lattice
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:458 theorem boundaryCardResidual_of_lattice_residual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:478 theorem BoundaryCardQuantizationResiduals.toBoundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:491 theorem BoundaryCardLatticeData.toLatticeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:509 theorem BoundaryCardQuantizationResiduals.ofLatticeData
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:520 theorem BoundaryCardLatticeData.toBoundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:540 theorem boundaryProbabilityResidual_of_lattice_residual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:559 theorem BoundaryCardLatticeData.toBoundaryProbabilityResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:578 theorem BoundaryCardQuantizationResiduals.toBoundaryProbabilityResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:768 theorem boundaryCardResidual_of_not_isSquare_deg_mul_card
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:785 theorem boundaryProbabilityResidual_of_not_isSquare_deg_mul_card
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:807 theorem boundaryCardResidual_of_isSquare_deg_mul_card
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:825 theorem boundaryProbabilityResidual_of_isSquare_deg_mul_card
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:972 theorem BoundaryCardLatticeData.toBoundaryCardResidual_isSquare
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:984 theorem BoundaryCardLatticeData.toBoundaryProbabilityResidual_isSquare
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:1020 theorem BoundaryCardQuantizationResiduals.toBoundaryCardResidual_isSquare
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidual.lean:1032 theorem BoundaryCardQuantizationResiduals.toBoundaryProbResidual_isSquare
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidualAffineLineRefutation.lean:118 theorem not_boundaryCardResidual_affineLine
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidualRefutation.lean:246 theorem not_boundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidualRefutation.lean:252 theorem not_boundaryCardLatticeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidualRefutation.lean:267 theorem not_boundaryCardQuantizationResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardResidualRefutation.lean:274 theorem not_boundaryProbabilityResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryCardStrictInteriorRefutation.lean:311 theorem not_boundaryCardResidual_nonSquareEndpoint
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryLatticeThresholdLeaf.lean:196 def BoundaryCardLatticeThresholdResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryLatticeThresholdLeaf.lean:206 theorem boundaryCardLatticeThresholdResidual_of_extraction
  • ArkLib/Data/CodingTheory/ProximityGap/BoundaryLatticeThresholdLeaf.lean:266 theorem boundaryCardLatticeThresholdResidual_of_canonical
  • ArkLib/Data/CodingTheory/ProximityGap/Errors.lean:1597 def diffStackMCAResidualBelowUDR
  • ArkLib/Data/CodingTheory/ProximityGap/Errors.lean:1632 theorem diffStackMCAResidualBelowUDR_of_epsCA_ge
  • ArkLib/Data/CodingTheory/ProximityGap/GK16Lemma12.lean:399 theorem GK16Lemma12HardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/GK16Lemma12.lean:413 theorem GK16Lemma12HardResidual_reduces_hard
  • ArkLib/Data/CodingTheory/ProximityGap/GK16Lemma12.lean:435 theorem gk16Lemma12HardResidual_holds
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:489 def mcaConjectureBound
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:516 def mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:536 theorem nonempty_mcaLowerWitness_of_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:556 theorem exists_mcaLowerWitness_of_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:576 theorem nonempty_mcaLowerWitness_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:592 theorem exists_mcaLowerWitness_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:609 theorem exists_prize_mcaLowerWitness_of_ignored_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:632 theorem nonempty_prize_mcaLowerWitness_of_ignored_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:655 theorem exists_prize_mcaLowerWitnesses_allRates_of_ignored_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/GrandChallenges.lean:687 theorem nonempty_prize_mcaLowerWitnesses_allRates_of_ignored_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25Johnson.lean:329 structure Hab25JohnsonResiduals
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25Johnson.lean:339 def Hab25JohnsonResiduals.ofAlgebraicData
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25Johnson.lean:359 def Hab25JohnsonResiduals.toAlgebraicData
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25Johnson.lean:392 theorem Hab25JohnsonResiduals.disagree_card_le
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25JohnsonNumericBridge.lean:122 def Hab25JohnsonResiduals.ofAlgebraicData_card_le
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25JohnsonNumericBridge.lean:143 def Hab25JohnsonResiduals.ofAlgebraicData_card_le_nat
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25JohnsonNumericBridge.lean:167 def Hab25JohnsonResiduals.ofAlgebraicData_algebraic_cover
  • ArkLib/Data/CodingTheory/ProximityGap/Hab25JohnsonNumericBridge.lean:186 def Hab25JohnsonResiduals.ofAlgebraicData_algebraic_cover_nat
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:722 theorem exists_mcaPrizeLatticeResolved_with_spec_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:757 theorem exists_mcaPrizeLatticeSpec_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:791 theorem mcaThreshold_spec_and_lower_bracket_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:833 theorem mcaThreshold_lower_bracket_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:861 theorem mcaThreshold_spec_and_lower_bracket_prize_allRates_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:893 theorem mcaThreshold_lower_bracket_prize_allRates_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:926 theorem mcaThreshold_spec_and_bracket_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:963 theorem mcaThreshold_bracket_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:995 theorem mcaThreshold_spec_and_bracket_prize_allRates_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1036 theorem mcaThreshold_bracket_prize_allRates_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1077 theorem exists_mcaPrizeLatticeSpec_and_lower_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1127 theorem exists_mcaPrizeLatticeResolved_with_spec_and_lower_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1164 theorem exists_mcaPrizeLatticeResolved_with_lower_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1195 theorem exists_mcaPrizeLatticeSpec_and_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1252 theorem exists_mcaPrizeLatticeResolved_with_spec_and_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/LatticeSpec.lean:1297 theorem exists_mcaPrizeLatticeResolved_with_brackets_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAConjectureRefutation.lean:48 def CS25BreakdownBelowConjectureBound
  • ArkLib/Data/CodingTheory/ProximityGap/MCAConjectureRefutation.lean:63 theorem not_mcaConjecture_of_cs25BreakdownBelowBound
  • ArkLib/Data/CodingTheory/ProximityGap/MCAConjectureRefutation.lean:120 def CS25BreakdownLowerResidualUniversal
  • ArkLib/Data/CodingTheory/ProximityGap/MCAConjectureRefutation.lean:130 def CS25BandInstanceBelowConjectureBound
  • ArkLib/Data/CodingTheory/ProximityGap/MCAConjectureRefutation.lean:161 theorem not_mcaConjecture_of_bandInstances_and_cs25Lower
  • ArkLib/Data/CodingTheory/ProximityGap/MCAGS.lean:575 def uniformEpsMCAgsPrizeBoundConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAGSRefutation.lean:102 theorem not_uniformEpsMCAgsPrizeBoundConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAGeneralStaircaseRefuted.lean:185 theorem generalStaircaseConjecture_refuted
  • ArkLib/Data/CodingTheory/ProximityGap/MCAHalfDistanceGeneralRefuted.lean:172 theorem halfDistanceStaircaseConjecture_refuted
  • ArkLib/Data/CodingTheory/ProximityGap/MCAHalfDistanceGeneralRefuted.lean:206 def GeneralStaircaseConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAHalfDistanceGeneralRefuted.lean:216 def MDSStaircaseConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAHalfDistanceStaircase.lean:109 def HalfDistanceStaircaseConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/MCAMDSStaircaseRefuted.lean:226 theorem mdsStaircaseConjecture_refuted
  • ArkLib/Data/CodingTheory/ProximityGap/RSListDecodingCapacityGap.lean:51 def UniformPolyListSizeConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2505 def StrictCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2528 def StrictCanonicalCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2554 theorem strictCoeffPolysResidual_of_strictCanonicalCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2578 def BoundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2597 def BoundaryProbabilityResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2611 theorem boundaryProbabilityResidual_of_boundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2645 theorem correlatedAgreement_affine_curves_of_boundaryCardResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves.lean:2662 theorem correlatedAgreement_affine_curves_of_strictCanonicalCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/HenselNumerator.lean:1654 def βHenselSuccTermWeightResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/HenselNumerator.lean:1735 def βHenselSuccTermStructuredWeightResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/HenselNumerator.lean:1755 theorem βHenselSuccTermWeightResidual_of_structured
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/HenselNumerator.lean:2510 def FaaDiBrunoSuccSumZeroResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/HenselNumerator.lean:2746 theorem βHenselSuccTermStructuredWeightResidual_holds
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/LocalSeriesProducer.lean:502 theorem strictCoeffPolysResidual_of_rawGSCargo
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/LocalSeriesProducer.lean:526 theorem strictCoeffPolysLargeResidual_of_rawGSCargo
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/LocalSeriesProducer.lean:548 theorem strictCoeffPolysLargeResidual_of_rawGSCargoProducer
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/MonicFaaDiBrunoMatchAlt.lean:87 theorem faaDiBrunoSuccSumZeroResidual_of_monic
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2Assembly.lean:460 theorem faaDiBrunoSuccSumZeroResidual_of_forall_partitionMatchAt
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2Assembly.lean:538 theorem faaDiBrunoSuccSumZeroResidual_of_partitionMatch
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2MatchProof.lean:30 def RestrictedFaaDiBrunoMatchResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2MonicConsequences.lean:45 theorem faaDiBrunoSuccSumZeroResidual_of_leadingCoeff_one
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2MonicWfreeGlobal.lean:127 theorem FaaDiBrunoSuccSumZeroResidual.of_WfreeMatch
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2MonicWfreeRangeConsumers.lean:47 theorem FaaDiBrunoSuccSumZeroResidual.of_rangeWfreeMatch
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2OrderZeroRefutation.lean:309 theorem faaDiBrunoSuccSumZeroResidual_false_of_constant_of_nonmonic
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2OrderZeroRefutation.lean:321 theorem faaDiBrunoSuccSumZeroResidual_false_of_constant_of_leadingCoeff_pow_ne_one
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2OrderZeroRefutation.lean:335 theorem faaDiBrunoSuccSumZeroResidual_false_of_constant_of_nonmonic_of_evalX_eq
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2OrderZeroRefutationWitness.lean:168 theorem faaDiBrunoSuccSumZeroResidual_false
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2RootBridge.lean:54 theorem faaDiBrunoSuccSumZeroResidual_iff_coeff_succ_eval
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2RootBridge.lean:125 theorem FaaDiBrunoSuccSumZeroResidual.of_eval_βHenselAssembled_eq_zero
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2Vanish.lean:188 theorem faaDiBrunoSuccSumZeroResidual_of_fullVanishes
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/P2Vanish.lean:197 theorem faaDiBrunoSuccSumZeroResidual_of_restrictedMatch
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffLargeReduction.lean:96 def StrictCoeffPolysLargeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffLargeReduction.lean:119 theorem strictCoeffPolysResidual_of_large
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffLargeReduction.lean:133 theorem strictCoeffPolysLargeResidual_of_residual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffLargeReduction.lean:142 theorem strictCoeffPolysResidual_iff_large
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffLargeReduction.lean:150 theorem correlatedAgreement_affine_curves_of_largeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysExceptional.lean:157 def StrictCoeffPolysExcResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysExceptional.lean:178 theorem strictCoeffPolysExcResidual_of_strictCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysExceptional.lean:190 theorem strictCoeffPolysExcResidual_mono
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysExceptional.lean:200 theorem strictCoeffPolysResidual_of_strictCoeffPolysExcResidual_zero
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShare.lean:76 def StrictCoeffPolysShareResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShare.lean:102 theorem strictCoeffPolysShareResidual_of_cell_decomposition
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShare.lean:180 theorem strictCoeffPolysShareResidual_of_strictCoeffPolysResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShare.lean:195 theorem strictCoeffPolysShareResidual_of_exc
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShareOr.lean:54 def StrictCoeffPolysResidualShareOr
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffPolysShareOr.lean:78 theorem strictCoeffPolysResidualShareOr_of_share
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffProducer.lean:426 theorem strictCoeffPolysResidual_of_localSeriesDatumOn
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/StrictCoeffProducer.lean:450 theorem strictCoeffPolysLargeResidual_of_localSeriesDatumOn
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean:1815 class Claim57Residuals
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean:1843 def Claim57Residuals.ofGraphExtractionHypotheses
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/DescendedRset.lean:410 class Claim57ResidualsDescended
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/DescendedRset.lean:538 def Claim57ResidualsDescended.ofInTree
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/DescendedRset.lean:682 def Claim57Residuals.ofDescended
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/DescendedRset.lean:714 def Claim57Residuals.ofDescendedInTree
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/FieldDischarge.lean:449 def Claim57Residuals.ofInTree
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/FieldDischarge.lean:494 def Claim57Residuals.ofInTree2
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionResidual.lean:30 def CurveCommonAgreementResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionResidual.lean:59 theorem strictCoeffPolysResidual_of_commonAgreement
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:42 theorem curveCommonAgreementResidual_of_one_le_mul
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:51 theorem curveCommonAgreementResidual_of_card_le
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:71 theorem strictCoeffPolysResidual_of_one_le_mul
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:79 theorem strictCoeffPolysResidual_of_card_le
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:164 theorem curveCommonAgreementResidual_of_card_le_e7
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/CoeffExtractionVacuous.lean:183 theorem strictCoeffPolysResidual_of_card_le_e7
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/ListSizeResidual.lean:45 def RSCurveListSizeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/Curves/ListSizeResidual.lean:61 theorem RS_jointAgreement_of_curveListSizeResidual
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Spec.lean:227 theorem exists_mcaPrizeLatticeResolved_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:400 theorem mcaThresholdExists_of_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:422 theorem mcaThreshold_spec_of_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:445 theorem mcaThresholdExists_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:461 theorem mcaThreshold_spec_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:479 theorem mcaThresholdExists_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ProximityGap/Lattice2/Witnesses.lean:501 theorem mcaThreshold_spec_prize_of_ignoredSource_mcaConjecture
  • ArkLib/Data/CodingTheory/ListDecoding/Bounds/RandomAndReedSolomon.lean:142 def randomLinearLambdaLowerFirstMomentResidual
  • ArkLib/Data/CodingTheory/ListDecoding/Bounds/RandomAndReedSolomon.lean:200 theorem randomLinearLambdaLowerFirstMomentResidual_of_exists_event
  • ArkLib/Data/CodingTheory/ListDecoding/Bounds/RandomAndReedSolomon.lean:224 theorem exists_code_of_randomLinearLambdaLowerFirstMomentResidual
  • ArkLib/Data/CodingTheory/ListDecoding/Bounds/RandomAndReedSolomon.lean:431 theorem randomLinearLambdaLowerFirstMomentResidual_of_combinatorialWitness
  • ArkLib/Data/CodingTheory/ListDecoding/Bounds/RandomAndReedSolomon.lean:443 theorem combinatorialWitness_of_randomLinearLambdaLowerFirstMomentResidual
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1046 def GKL24FirstMomentResidual
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1058 theorem GKL24FirstMomentResidual_inTree_card
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1080 theorem GKL24FirstMomentResidual_inTree_two_delta_card
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1107 def GKL24FirstMomentWitnessCoverResidual
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1127 theorem GKL24FirstMomentWitnessCoverResidual_inTree_two_delta_card
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1309 def GKL24MaxCorrStrictWitnessCoverResidual
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1376 theorem GKL24FirstMomentWitnessCoverResidual_of_maxCorr_cover
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1393 theorem GKL24FirstMomentWitnessCoverResidual_of_strict_cover
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1480 theorem GKL24FirstMomentWitnessCoverResidual_of_petal_cover
  • ArkLib/Data/CodingTheory/Connections/GKL24FirstMoment.lean:1529 theorem GKL24FirstMomentResidual_inTree_delta_add_one_card
  • ArkLib/Data/CodingTheory/Connections/GKL24PetalWitnessCover.lean:56 def GKL24MaxDomainWitnessCoverResidual

MCACapacityTrivial

residual-named declarations

  • ArkLib/MCACapacityTrivial.lean:20 theorem mca_capacity_bound_CONJECTURE_trivially_true

MCAGSRefutationCore

residual-named declarations

  • ArkLib/MCAGSRefutationCore.lean:101 theorem not_uniformEpsMCAgsPrizeBoundConjecture

OracleReduction/Composition

residual-named declarations

  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:901 def reductionAppendCompletenessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:920 def reductionAppendPerfectCompletenessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:957 def appendSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:996 def appendKnowledgeSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1020 def appendRbrSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1059 def appendRbrKnowledgeSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1107 def appendCompletenessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1128 def appendPerfectCompletenessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1154 def appendSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1184 def appendKnowledgeSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1205 def appendRbrSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:1227 def appendRbrKnowledgeSoundnessResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:4134 def appendRunRightResidual
  • ArkLib/OracleReduction/Composition/Sequential/Append.lean:4160 theorem appendRunRightResidual_holds_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendCompletenessEmptyErr.lean:155 theorem reductionAppendCompletenessResidual_holds
  • ArkLib/OracleReduction/Composition/Sequential/AppendCompletenessEmptyErr.lean:187 theorem appendCompletenessResidual_holds
  • ArkLib/OracleReduction/Composition/Sequential/AppendCompletenessMsgKeystone.lean:290 theorem appendCompletenessResidual_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendKnowledgeOracleTransport.lean:66 theorem appendKnowledgeSoundnessResidual_of_plain
  • ArkLib/OracleReduction/Composition/Sequential/AppendPerfectCompletenessMsg.lean:392 theorem reductionAppendPerfectCompletenessResidual_of_message
  • ArkLib/OracleReduction/Composition/Sequential/AppendPerfectCompletenessOracle.lean:67 def appendToReductionResidual
  • ArkLib/OracleReduction/Composition/Sequential/AppendPerfectCompletenessOracle.lean:122 theorem appendToReductionResidual_iff_verifier
  • ArkLib/OracleReduction/Composition/Sequential/AppendPerfectCompletenessTotal.lean:78 theorem reductionAppendPerfectCompletenessResidual_holds
  • ArkLib/OracleReduction/Composition/Sequential/AppendPerfectCompletenessTotal.lean:158 theorem appendPerfectCompletenessResidual_holds
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKeystone.lean:282 def appendRbrSoundnessPhase2Residual
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgeOracleLift.lean:94 theorem appendRbrKnowledgeSoundnessResidual_msg_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgePerRoundDischarge.lean:46 theorem appendRbrKnowledgeSoundnessPerRoundResidual_msg_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgeStateCollapse.lean:71 theorem appendRbrKnowledgeSoundnessResidual_of_message_collapse
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgeStateCollapse.lean:119 theorem appendRbrSoundnessResidual_of_message_collapse
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgeStateFunction.lean:944 def appendRbrKnowledgeSoundnessPerRoundResidual
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrKnowledgeStateFunction.lean:1226 def appendRbrKnowledgeSoundnessPhase2Residual
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrSoundnessOracleLift.lean:91 theorem appendRbrSoundnessResidual_msg_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendRbrSoundnessPhase2Proof.lean:639 theorem appendRbrSoundnessResidual_msg_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischarges.lean:54 theorem reductionAppendCompletenessResidual_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischarges.lean:93 theorem appendRbrKnowledgeSoundnessResidual_msg_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischarges.lean:138 theorem appendPerfectCompletenessResidual_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischargesSeams.lean:51 theorem appendRbrKnowledgeSoundnessResidual_challenge_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischargesSeams.lean:80 theorem appendRbrKnowledgeSoundnessResidual_failingDet_subsingleton
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischargesSeams.lean:105 theorem appendRbrKnowledgeSoundnessResidual_failingDet_empty
  • ArkLib/OracleReduction/Composition/Sequential/AppendResidualDischargesSeams.lean:142 theorem reductionAppendCompletenessResidual_total_pos
  • ArkLib/OracleReduction/Composition/Sequential/AppendRunEvalDist.lean:53 def appendRunRightResidualDist
  • ArkLib/OracleReduction/Composition/Sequential/AppendRunEvalDist.lean:104 theorem appendRunRightResidualDist_holds_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendRunEvalDistChallenge.lean:266 theorem appendRunRightResidualDist_holds_challenge
  • ArkLib/OracleReduction/Composition/Sequential/AppendRunEvalDistChallenge.lean:347 theorem appendRunRightResidualDist_holds
  • ArkLib/OracleReduction/Composition/Sequential/AppendSoundnessOracleMsg.lean:91 theorem appendSoundnessResidual_msg
  • ArkLib/OracleReduction/Composition/Sequential/AppendToVerifierKeystone.lean:148 theorem appendToReductionResidual_proof
  • ArkLib/OracleReduction/Composition/Sequential/EmptyAppend.lean:84 theorem appendRunRightResidual_holds_empty

OracleReduction/FiatShamir

residual-named declarations

  • ArkLib/OracleReduction/FiatShamir/Basic.lean:303 def fiatShamir_runCollapseResidual
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:318 theorem fiatShamir_runCollapseResidual_of_run_eq_honestExecution
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:893 def fiatShamir_soundnessTransferResidual
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1002 def fiatShamir_knowledgeSoundnessTransferResidual
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1159 def fiatShamir_statisticalHVZKTransferResidual
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1174 theorem fiatShamir_statisticalHVZKTransferResidual.mono_error
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1192 theorem fiatShamir_statisticalHVZKTransferResidual.of_zero
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1286 def fiatShamir_hvzkTransferResidual
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1299 theorem fiatShamir_statisticalHVZKTransferResidual.of_perfectTransfer
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1315 theorem fiatShamir_hvzkTransferResidual.of_statistical_zero
  • ArkLib/OracleReduction/FiatShamir/Basic.lean:1332 theorem fiatShamir_hvzkTransferResidual_iff_statistical_zero
  • ArkLib/OracleReduction/FiatShamir/HVZKCanonicalClose.lean:79 theorem fiatShamir_statisticalHVZKTransferResidual_canonical_proved
  • ArkLib/OracleReduction/FiatShamir/HVZKKernelClose.lean:1080 theorem fiatShamir_hvzkTransferResidual_canonical_proved
  • ArkLib/OracleReduction/FiatShamir/HVZKTransferReduction.lean:315 theorem fiatShamir_hvzkTransferResidual_canonical
  • ArkLib/OracleReduction/FiatShamir/HVZKTransferReduction.lean:343 theorem fiatShamir_hvzkTransferResidual_canonical_of_perStateCoupling
  • ArkLib/OracleReduction/FiatShamir/RunEqHonestExecution.lean:155 theorem fiatShamir_runCollapseResidual_holds
  • ArkLib/OracleReduction/FiatShamir/StateRestorationTransport.lean:899 theorem fiatShamir_soundnessTransferResidual_canonical
  • ArkLib/OracleReduction/FiatShamir/StateRestorationTransport.lean:3301 theorem fiatShamir_knowledgeSoundnessTransferResidual_canonical
  • ArkLib/OracleReduction/FiatShamir/ZKResidualBridge.lean:55 theorem fiatShamir_hvzkTransferResidual_of_statisticalHVZKTransferResidual_zero
  • ArkLib/OracleReduction/FiatShamir/ZKResidualBridge.lean:68 theorem fiatShamir_statisticalHVZKTransferResidual_zero_of_hvzkTransferResidual
  • ArkLib/OracleReduction/FiatShamir/ZKResidualBridge.lean:81 theorem fiatShamir_hvzkTransferResidual_iff_statisticalHVZKTransferResidual_zero
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BirthdayBoundPaper.lean:92 def Lemma5_8EagerPaperResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BirthdayBoundPaper.lean:109 theorem honestBad_birthday_of_paperResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BirthdayBoundPaper.lean:130 theorem honestBad_claim5_21Bound_of_paperResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/BirthdayBoundPaper.lean:152 theorem lemma5_8EagerPaperResidual_of_lazy
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Completeness.lean:200 def duplexSpongeFiatShamir_runCollapseResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Completeness.lean:212 def duplexSpongeFiatShamirSalted_runCollapseResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/ConsistencyPaperCascade.lean:441 theorem lemma5_12HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/ConsistencyPaperCascade.lean:508 theorem lemma5_16HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/ForkPaperFork.lean:705 theorem lemma5_14HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/HonestConsistencyPaper.lean:658 def Lemma5_12HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/HonestConsistencyPaper.lean:666 def Lemma5_14HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/HonestConsistencyPaper.lean:676 def Lemma5_16HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Hyb34LogShapeFalse.lean:643 def Hyb4ChallengeEntryResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Hyb34LogShapeFalse.lean:679 theorem hyb34StepResidual_logShape_false
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Hyb4ChallengeEntry.lean:246 theorem hyb4ChallengeEntryResidual_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemma.lean:245 def KeyLemmaResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:634 def Lemma5_12HonestResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:934 def SimulatedProverChallengeBudgetResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:951 def SimulatedProverSharedBudgetResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:971 def KeyLemmaEagerResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:1011 def D2sQueryStepGSpecBudgetResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaFoundations.lean:1027 def D2fOuterImplSharedBudgetResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaHybrids.lean:709 def Hyb01StepResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaHybrids.lean:731 def Hyb12StepResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaHybrids.lean:754 def Hyb23StepResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaHybrids.lean:773 def Hyb34StepResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaSalted.lean:590 def Hyb01StepResidualS
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaSalted.lean:612 def Hyb12StepResidualS
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaSalted.lean:635 def Hyb23StepResidualS
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaSalted.lean:655 def Hyb34StepResidualS
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/KeyLemmaSalted.lean:714 def KeyLemmaEagerSaltedResidual
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma512HonestPaper.lean:658 def Lemma5_12HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma512HonestPaper.lean:666 def Lemma5_14HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma512HonestPaper.lean:676 def Lemma5_16HonestResidualPaper
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma512PaperCascade.lean:441 theorem lemma5_12HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma512PaperCascade.lean:508 theorem lemma5_16HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma514PaperFork.lean:705 theorem lemma5_14HonestResidualPaper_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Lemma58Reduction.lean:46 theorem lemma5_8EagerPaperResidual_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/Reduction.lean:46 theorem lemma5_8EagerPaperResidual_holds
  • ArkLib/OracleReduction/FiatShamir/DuplexSponge/Security/RunEqHonest.lean:417 theorem duplexSpongeFiatShamir_runCollapseResidual_holds

ProofSystem/Logup

residual-named declarations

  • ArkLib/ProofSystem/Logup/Security/BridgeAndAppendResiduals.lean:237 theorem oracleReductionToReductionResidual_of_binary
  • ArkLib/ProofSystem/Logup/Security/Completeness.lean:237 def SubPhaseCompletenessResidual
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessClose.lean:139 theorem appendCompletenessResidual_iff_toReduction
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessMsgSeam.lean:114 theorem appendCompletenessResidual_msgSeam
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessUncond.lean:169 theorem sumcheckCompletenessResidual_of_perRound
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessWired.lean:185 theorem appendCompletenessResidual_wired
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessWired.lean:264 theorem logupCompletenessBrickResidual_holds
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessWired.lean:327 theorem appendCompletenessResidual_unconditional
  • ArkLib/ProofSystem/Logup/Security/LogupCompletenessWired.lean:349 theorem appendCompletenessResidual_forall
  • ArkLib/ProofSystem/Logup/Security/LogupProtocol2Status.lean:333 theorem issue13_sumcheckSoundnessResidual_projClosed
  • ArkLib/ProofSystem/Logup/Security/LogupResidualDischarge.lean:70 theorem outerSoundnessResidual_holds
  • ArkLib/ProofSystem/Logup/Security/LogupResidualDischarge.lean:82 theorem sumcheckSoundnessResidual_holds_pointwise
  • ArkLib/ProofSystem/Logup/Security/LogupResidualDischarge.lean:96 theorem subPhaseSoundnessResidual_holds
  • ArkLib/ProofSystem/Logup/Security/LogupResidualDischarge.lean:113 theorem appendSoundnessResidual_holds
  • ArkLib/ProofSystem/Logup/Security/LogupResidualDischarge.lean:128 theorem logupSoundnessBrickResidual_holds
  • ArkLib/ProofSystem/Logup/Security/LogupSoundnessUncond.lean:117 theorem oracleAppendSoundnessResidual_of_plain
  • ArkLib/ProofSystem/Logup/Security/LogupSoundnessUncond.lean:166 theorem logupAppendSoundnessResidual_of_plain
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:139 def OuterCompletenessRunResidual
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:149 def OuterCompletenessRunFactsResidual
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:209 theorem outer_completeness_of_runResidual
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:811 theorem outer_completenessRunFactsResidual
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:829 theorem outerCompletenessRunResidual_proved
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:838 theorem subPhaseCompletenessResidual_of_sumcheck
  • ArkLib/ProofSystem/Logup/Security/OuterCompleteness.lean:845 theorem outerCompletenessRunResidual_iff
  • ArkLib/ProofSystem/Logup/Security/OuterRunSamplesChallenge.lean:185 theorem outerSoundnessResidual_real_of_marginal
  • ArkLib/ProofSystem/Logup/Security/OuterSoundnessReal.lean:466 theorem outerSoundnessResidual_real_of_runUnfolding
  • ArkLib/ProofSystem/Logup/Security/RbrToSoundBridge.lean:264 theorem sumcheckSoundnessResidual_holds_of_rbr
  • ArkLib/ProofSystem/Logup/Security/Soundness.lean:118 def SubPhaseSoundnessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:70 def OuterSoundnessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:78 def SumcheckSoundnessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:83 theorem subPhaseSoundnessResidual_iff_split
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:108 def AppendSoundnessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:115 def LogupSoundnessBrickResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:122 theorem logupSoundnessBrickResidual_iff_subPhase_append
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:163 def OuterCompletenessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:169 def SumcheckCompletenessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:174 theorem subPhaseCompletenessResidual_iff_split
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:183 def AppendCompletenessResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:206 def LogupCompletenessBrickResidual
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:213 theorem logupCompletenessBrickResidual_iff_subPhase_append
  • ArkLib/ProofSystem/Logup/Security/SubPhaseSplit.lean:252 theorem outerCompletenessResidual_of_neverFail
  • ArkLib/ProofSystem/Logup/Security/SumcheckCompleteness.lean:45 theorem sumcheckCompletenessResidual_proved
  • ArkLib/ProofSystem/Logup/Security/SumcheckCompletenessClose.lean:140 theorem sumcheckCompletenessResidual_holds
  • ArkLib/ProofSystem/Logup/Security/SumcheckCompletenessUncond.lean:51 theorem sumcheckCompletenessResidual_unconditional
  • ArkLib/ProofSystem/Logup/Security/SumcheckCompletenessUncond.lean:67 theorem subPhaseCompletenessResidual_unconditional
  • ArkLib/ProofSystem/Logup/Security/SumcheckLensProjComplete.lean:122 theorem sumcheckCompletenessResidual_of_inner
  • ArkLib/ProofSystem/Logup/Security/SumcheckSoundness.lean:44 theorem sumcheckSoundnessResidual_proved
  • ArkLib/ProofSystem/Logup/Security/SumcheckSoundnessLift.lean:193 theorem sumcheckSoundnessResidual_holds
  • ArkLib/ProofSystem/Logup/Security/SumcheckSoundnessPointwise.lean:134 theorem sumcheckSoundnessResidual_pointwise
  • ArkLib/ProofSystem/Logup/Security/SumcheckSoundnessProjClosed.lean:109 theorem sumcheckSoundnessResidual_holds_projClosed
  • ArkLib/ProofSystem/Logup/Security/SumcheckSoundnessWired.lean:88 theorem sumcheckSoundnessResidual_holds_wired

ProofSystem/Spartan

residual-named declarations

  • ArkLib/ProofSystem/Spartan/Basic.lean:700 def r1csResidualAt
  • ArkLib/ProofSystem/Spartan/Composition.lean:477 theorem composedPIOPResidual_holds_proof
  • ArkLib/ProofSystem/Spartan/Composition.lean:482 theorem composedPIOPWithClaimResidual_holds_proof
  • ArkLib/ProofSystem/Spartan/R1CSMleEquivalence.lean:201 def r1csResidual
  • ArkLib/ProofSystem/Spartan/R1CSMleEquivalence.lean:235 theorem zeroCheckVirtualPolynomial_eq_mle'_r1csResidual

ProofSystem/Stir

residual-named declarations

  • ArkLib/ProofSystem/Stir/CheckingVerifier.lean:964 def stirCheckingRbrSoundnessResidual
  • ArkLib/ProofSystem/Stir/MultiRoundAssembly.lean:224 def stirMultiRoundRbrSoundnessResidual
  • ArkLib/ProofSystem/Stir/MultiRoundSpecT.lean:360 def stirCheckingRbrSoundnessResidualT

ProofSystem/Sumcheck

residual-named declarations

  • ArkLib/ProofSystem/Sumcheck/Spec/OracleCompleteness.lean:69 abbrev oracleReductionToReductionResidual

ProofSystem/Whir

residual-named declarations

  • ArkLib/ProofSystem/Whir/MCAConjectureEllaryReduction.lean:436 theorem mca_johnson_bound_CONJECTURE_ellary_of_curveJohnsonNumericBound
  • ArkLib/ProofSystem/Whir/MCAConjectureEllaryReduction.lean:485 theorem mca_johnson_bound_CONJECTURE_ellary_of_claim1_cells
  • ArkLib/ProofSystem/Whir/MCAConjectureEllaryReduction.lean:522 theorem mca_johnson_bound_CONJECTURE_pair_via_ellary
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:100 theorem mca_johnson_bound_CONJECTURE_pair_of_johnsonNumericBound
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:142 theorem mca_johnson_bound_CONJECTURE_pair_of_claim1_cells
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:181 theorem mca_johnson_bound_CONJECTURE_pair_of_decode_family_pinning
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:226 theorem mca_johnson_bound_CONJECTURE_pair_of_decode_family_window
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:274 theorem mca_johnson_bound_CONJECTURE_pair_of_fixed_linear_factor_cells
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:330 theorem decode_family_affine_pinning_of_strictCoeffPolysResidual
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:371 theorem decode_family_affine_pinning_of_strictCoeffPolysLargeResidual
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:404 theorem hsteps57_of_strictCoeffPolysResidual
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:440 theorem hsteps57_of_strictCoeffPolysLargeResidual
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:525 theorem decode_family_affine_pinning_of_strictCoeffPolysResidual_cell_card_gt
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:563 theorem hsteps57_of_strictCoeffPolysResidual_cell_card_gt
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:594 theorem hsteps57_of_strictCoeffPolysLargeResidual_cell_card_gt
  • ArkLib/ProofSystem/Whir/MCAConjecturePairReduction.lean:1016 theorem mca_johnson_bound_CONJECTURE_pair_of_coeff_polys_cells
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:34 def johnsonConjectureEta
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:46 def K4GradedFactorCellResidual
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:64 def K4ComponentResidual
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:87 theorem K4GradedFactorCellResidual_of_component
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:107 theorem mca_johnson_bound_CONJECTURE_holds_of_rawGSCargo
  • ArkLib/ProofSystem/Whir/MCAJohnsonBound.lean:189 theorem mca_johnson_bound_CONJECTURE_pair_of_K4_graded_closed
  • ArkLib/ProofSystem/Whir/MCAJohnsonSmallField.lean:28 theorem mca_johnson_bound_CONJECTURE_smallField
  • ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean:319 def mca_johnson_bound_CONJECTURE
  • ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean:371 def mca_capacity_bound_CONJECTURE

ResidualAxioms

residual-named declarations

  • ArkLib/ResidualAxioms.lean:27 def RingSwitchingKStateResidual
  • ArkLib/ResidualAxioms.lean:35 theorem ringSwitchingKStateResidual_holds

ToMathlib

residual-named declarations

  • ArkLib/ToMathlib/BCIKS20ConcreteJohnson.lean:113 def claim57Residuals_of_gsInterpolant
  • ArkLib/ToMathlib/BCIKS20PigeonholeSupply.lean:169 def claim57Residuals_of_johnson
  • ArkLib/ToMathlib/BCIKS20PigeonholeSupply.lean:205 def claim57Residuals_of_natCeil_johnson
  • ArkLib/ToMathlib/BoundaryDischarge.lean:285 theorem boundaryCardResidual_of_boundary_cards_and_coeffPolys
  • ArkLib/ToMathlib/BoundaryDischarge.lean:314 theorem boundaryCardLatticeResidual_of_boundary_cards_and_coeffPolys
  • ArkLib/ToMathlib/BoundaryDischarge.lean:343 theorem boundaryCardLatticeResidual_of_lattice_data
  • ArkLib/ToMathlib/BoundaryDischarge.lean:448 theorem BoundaryCardQuantizationData.toQuantizationResiduals
  • ArkLib/ToMathlib/BoundaryDischarge.lean:459 theorem BoundaryCardQuantizationData.toBoundaryCardResidual
  • ArkLib/ToMathlib/BoundaryDischarge.lean:468 theorem BoundaryCardQuantizationData.toBoundaryProbabilityResidual
  • ArkLib/ToMathlib/BoundaryDischarge.lean:497 theorem boundaryCardResidual_of_lattice_data
  • ArkLib/ToMathlib/BoundaryDischarge.lean:518 theorem boundaryProbabilityResidual_of_lattice_data
  • ArkLib/ToMathlib/BoundaryDischarge.lean:568 theorem boundaryCardResidual_of_lattice_data_isSquare
  • ArkLib/ToMathlib/BoundaryDischarge.lean:585 theorem boundaryProbabilityResidual_of_lattice_data_isSquare
  • ArkLib/ToMathlib/BoundaryDischarge.lean:628 theorem boundaryCardResidual_zero
  • ArkLib/ToMathlib/BoundaryDischarge.lean:638 theorem boundaryProbabilityResidual_zero
  • ArkLib/ToMathlib/BoundaryHalfState.lean:183 theorem correlatedAgreementCurves_boundary_of_largeResidual_cellMin
  • ArkLib/ToMathlib/CS25DeepHoleFinish.lean:264 def DeepHoleProbResidual
  • ArkLib/ToMathlib/CS25DeepHoleFinish.lean:282 theorem hDeepHole_of_probResidual
  • ArkLib/ToMathlib/CS25DeepHoleFinish2.lean:259 theorem deepHoleProbResidual_of_jointFar
  • ArkLib/ToMathlib/CS25JointFar.lean:205 theorem deepHoleProbResidual_holds
  • ArkLib/ToMathlib/CurveFamilyHensel.lean:143 theorem strictCoeffPolysResidual_of_curveHenselDatum
  • ArkLib/ToMathlib/CurveFamilyRoundConsumers.lean:95 theorem boundaryProbabilityResidual_of_strict
  • ArkLib/ToMathlib/CurveHenselSupply.lean:680 theorem strictCoeffPolysResidual_of_gsCurveInput
  • ArkLib/ToMathlib/FaithfulCurveExtraction.lean:195 theorem strictCoeffPolysResidual_of_curveFamilyData
  • ArkLib/ToMathlib/FaithfulFrontierComposition.lean:298 theorem strictCoeffPolysResidual_of_faithful_frontier
  • ArkLib/ToMathlib/FriComplete.lean:106 def foldRoundPerfectCompletenessResidual
  • ArkLib/ToMathlib/FriComplete.lean:131 def finalFoldRoundPerfectCompletenessResidual
  • ArkLib/ToMathlib/FriCompleteFinalRound.lean:125 theorem finalFoldRoundPerfectCompletenessResidual_holds
  • ArkLib/ToMathlib/FriCompletePerRound.lean:137 theorem foldRoundPerfectCompletenessResidual_holds
  • ArkLib/ToMathlib/FriCompleteQueryRound.lean:177 def queryRoundChainDeliveryResidual
  • ArkLib/ToMathlib/GSGradedBundle.lean:283 structure MonicHighYResidual
  • ArkLib/ToMathlib/GSLineInputSupply.lean:216 structure PerZResidual
  • ArkLib/ToMathlib/KeystoneStrictResidual.lean:411 theorem strictCoeffPolysResidual_of_betaRec
  • ArkLib/ToMathlib/KeystoneStrictResidual.lean:428 theorem strictCoeffPolysResidual_of_betaRec_offcentre
  • ArkLib/ToMathlib/KeystoneStrictResidual.lean:445 theorem strictCoeffPolysResidual_of_betaRec_offcentreFin
  • ArkLib/ToMathlib/KeystoneStrictResidual.lean:462 theorem strictCoeffPolysResidual_of_betaRecFin
  • ArkLib/ToMathlib/KeystoneStrictResidual.lean:478 theorem strictCoeffPolysResidual_zero
  • ArkLib/ToMathlib/L46DiffStackRS.lean:94 theorem diffStackMCAResidualBelowUDR_rs
  • ArkLib/ToMathlib/L46DiffStackRS.lean:133 theorem diffStackMCAResidualBelowUDR_rs_of_two_mul_lt_card_sub
  • ArkLib/ToMathlib/L46GSLowerBound.lean:187 theorem diffStackResidual_of_gsWitness
  • ArkLib/ToMathlib/L46GSWitnessRS.lean:263 theorem diffStackMCAResidualBelowUDR_rs_unconditional
  • ArkLib/ToMathlib/LatticeFrontierReduction.lean:101 theorem boundaryCardLatticeThresholdResidual_of_countFrontier
  • ArkLib/ToMathlib/MonicResidualBoundary.lean:131 theorem monicHighYResidual_of_isUnit_leadingCoeff
  • ArkLib/ToMathlib/MonicResidualBoundary.lean:144 theorem monicHighYResidual_graded_of_isUnit_leadingCoeff
  • ArkLib/ToMathlib/OffcentreFaithfulBundle.lean:199 theorem strictCoeffPolysResidual_of_section5DataOffcentreFaithful
  • ArkLib/ToMathlib/OffcentreKeystoneAssembly.lean:247 theorem strictCoeffPolysResidual_of_section5DataOffcentreFin
  • ArkLib/ToMathlib/RSPhases.lean:128 def BatchingConsistencyResidual
  • ArkLib/ToMathlib/RSPhases.lean:133 theorem batchingConsistencyResidual_sum
  • ArkLib/ToMathlib/SpartanBricks.lean:474 def secondSumcheckTerminalEndpointResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:482 theorem secondSumcheckTerminalEndpointResidual_holds
  • ArkLib/ToMathlib/SpartanBricks.lean:677 def finalCheckWithClaimValueRelResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:685 theorem finalCheckWithClaimValueRelResidual_holds
  • ArkLib/ToMathlib/SpartanBricks.lean:693 theorem finalCheckWithClaimValueRelResidual_of_secondSumcheckTerminalEndpointResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:703 theorem secondSumcheckTerminalEndpointResidual_of_finalCheckWithClaimValueRelResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:715 theorem finalCheckWithClaimValueRelResidual_iff_secondSumcheckTerminalEndpointResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:767 def secondSumcheckResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:773 theorem secondSumcheckResidual_holds
  • ArkLib/ToMathlib/SpartanBricks.lean:779 def firstSumcheckResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:785 theorem firstSumcheckResidual_holds
  • ArkLib/ToMathlib/SpartanBricks.lean:839 def r1csMleEncodingResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:855 theorem r1csMleEncodingResidual_holds
  • ArkLib/ToMathlib/SpartanBricks.lean:1020 def composedPIOPResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:1036 theorem composedPIOPResidual_of_reduction
  • ArkLib/ToMathlib/SpartanBricks.lean:1049 def composedPIOPWithClaimResidual
  • ArkLib/ToMathlib/SpartanBricks.lean:1061 theorem composedPIOPWithClaimResidual_of_reduction
  • ArkLib/ToMathlib/SurfaceFactorProduction.lean:210 def graphHypothesesOfResiduals
  • ArkLib/ToMathlib/UnifiedExtractionTarget.lean:96 theorem strictCoeffPolysLargeResidual_of_producer
  • ArkLib/ToMathlib/UnifiedProducerWindowGlue.lean:325 theorem strictCoeffPolysLargeResidual_of_window
  • ArkLib/ToMathlib/UnifiedProducerWindowGlue.lean:335 theorem strictCoeffPolysResidual_of_window