Paper IX · Lean sources
Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Source files 633
Source locations and editions
Files are shown relative to preserved/PRSC_IX_Consolidated_Manuscript/.
Historical editions keep their original paths. Package caches and build files are omitted.
633 files
CompactSelfIsometryAudit.leanhistorical/development_audit_drivers/isometry/DensePadicIsometryAudit.leanhistorical/development_audit_drivers/isometry/DyadicControlsAudit.leanhistorical/development_audit_drivers/isometry/RationalAudit.leanhistorical/development_audit_drivers/isometry/NewtonDominanceAudit.leanhistorical/development_audit_drivers/least_periods/AllRowsAxioms.leanhistorical/development_audit_drivers/strengthening/AxiomAudit.leanhistorical/development_audit_drivers/strengthening/BridgeAxiomAudit.leanhistorical/development_audit_drivers/strengthening/DyadicFourSharpeningAudit.leanhistorical/development_audit_drivers/strengthening/SharedUniversal.leanhistorical/shared_correction_development/universal_work/AffineObstructionControls.leannative/lean/FiniteAffineObstruction.leannative/lean/AffineObstructionControls.leannative/lean/replay_02/sources/FiniteAffineObstruction.leannative/lean/replay_02/sources/NegativePrecisionUpgrade.leannative/lean/replay_02/sources/NegativeUnconditionalLift.leannative/lean/replay_02/sources/PolynomialCoefficientPerturbationContract.leanpolynomial_charts/contracts/PolynomialGeneralChartContract.leanpolynomial_charts/contracts/PolynomialHomeomorphContract.leanpolynomial_charts/contracts/PolynomialLocalMapContract.leanpolynomial_charts/contracts/PolynomialPadicUniqueContract.leanpolynomial_charts/contracts/PolynomialRootStabilityContract.leanpolynomial_charts/contracts/InvalidGlobalUniqueness.leanpolynomial_charts/controls/InvalidPerturbationExtraPrecision.leanpolynomial_charts/controls/InvalidPrescribedParameter.leanpolynomial_charts/controls/InvalidRectangularUniqueness.leanpolynomial_charts/controls/PolynomialDeformationControls.leanpolynomial_charts/controls/PolynomialParameterControls.leanpolynomial_charts/controls/AffineObstructionCore.leanpolynomial_charts/formalization/FiniteFiberCounts.leanpolynomial_charts/formalization/IntegerFiniteCokernel.leanpolynomial_charts/formalization/PadicTowerLimit.leanpolynomial_charts/formalization/PolynomialCoefficientPerturbation.leanpolynomial_charts/formalization/PolynomialCoordinateReorder.leanpolynomial_charts/formalization/PolynomialDigitBridge.leanpolynomial_charts/formalization/PolynomialGeneralChart.leanpolynomial_charts/formalization/PolynomialIntegerTower.leanpolynomial_charts/formalization/PolynomialInverseCongruence.leanpolynomial_charts/formalization/PolynomialLiftCounts.leanpolynomial_charts/formalization/PolynomialLocalInverse.leanpolynomial_charts/formalization/PolynomialLocalSurjective.leanpolynomial_charts/formalization/PolynomialMinorSelection.leanpolynomial_charts/formalization/PolynomialObstruction.leanpolynomial_charts/formalization/PolynomialPadicLift.leanpolynomial_charts/formalization/PolynomialPadicUnique.leanpolynomial_charts/formalization/PolynomialParameterChart.leanpolynomial_charts/formalization/PolynomialParameterSystem.leanpolynomial_charts/formalization/PolynomialRootStability.leanpolynomial_charts/formalization/PolynomialSmoothCounts.leanpolynomial_charts/formalization/PolynomialSurjectiveStep.leanpolynomial_charts/formalization/PolynomialTaylor.leanpolynomial_charts/formalization/PolynomialTowerControls.leanpolynomial_charts/formalization/ResidueLiftDigits.leanpolynomial_charts/formalization/PolynomialChartsAxiomAudit.leanpolynomial_charts/verification/FiniteFiberCountsContract.leanpolynomial_counts/contracts/PolynomialLiftCountContract.leanpolynomial_counts/contracts/ResidueDigitsContract.leanpolynomial_counts/contracts/InvalidDroppingLowerResidue.leanpolynomial_counts/controls/InvalidSingularUniqueLift.leanpolynomial_counts/controls/InvalidUnconditionalLiftCount.leanpolynomial_counts/controls/IntegerFiniteCokernel.leanpolynomial_counts/development/cokernel/PolynomialLiftCounts.leanpolynomial_counts/development/counts/PolynomialDigitBridge.leanpolynomial_counts/development/digits/FiniteFiberCounts.leanpolynomial_counts/development/linear/FiniteFiberCountsAudit.leanpolynomial_counts/development/linear/ResidueLiftDigits.leanpolynomial_counts/development/residues/AffineObstructionCore.leanpolynomial_counts/formalization/FiniteFiberCounts.leanpolynomial_counts/formalization/IntegerFiniteCokernel.leanpolynomial_counts/formalization/PolynomialCountControls.leanpolynomial_counts/formalization/PolynomialDigitBridge.leanpolynomial_counts/formalization/PolynomialLiftCounts.leanpolynomial_counts/formalization/PolynomialObstruction.leanpolynomial_counts/formalization/PolynomialTaylor.leanpolynomial_counts/formalization/ResidueLiftDigits.leanpolynomial_counts/formalization/PolynomialCountsAxiomAudit.leanpolynomial_counts/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_deformation/contracts/PolynomialPadicUniqueContract.leanpolynomial_deformation/contracts/PolynomialRootStabilityContract.leanpolynomial_deformation/contracts/InvalidGlobalUniqueness.leanpolynomial_deformation/controls/InvalidPerturbationExtraPrecision.leanpolynomial_deformation/controls/InvalidRectangularUniqueness.leanpolynomial_deformation/controls/PolynomialDeformationControls.leanpolynomial_deformation/controls/AffineObstructionCore.leanpolynomial_deformation/formalization/FiniteFiberCounts.leanpolynomial_deformation/formalization/IntegerFiniteCokernel.leanpolynomial_deformation/formalization/PadicTowerLimit.leanpolynomial_deformation/formalization/PolynomialCoefficientPerturbation.leanpolynomial_deformation/formalization/PolynomialDigitBridge.leanpolynomial_deformation/formalization/PolynomialIntegerTower.leanpolynomial_deformation/formalization/PolynomialLiftCounts.leanpolynomial_deformation/formalization/PolynomialObstruction.leanpolynomial_deformation/formalization/PolynomialPadicLift.leanpolynomial_deformation/formalization/PolynomialPadicUnique.leanpolynomial_deformation/formalization/PolynomialRootStability.leanpolynomial_deformation/formalization/PolynomialSmoothCounts.leanpolynomial_deformation/formalization/PolynomialSurjectiveStep.leanpolynomial_deformation/formalization/PolynomialTaylor.leanpolynomial_deformation/formalization/PolynomialTowerControls.leanpolynomial_deformation/formalization/ResidueLiftDigits.leanpolynomial_deformation/formalization/PolynomialDeformationAxiomAudit.leanpolynomial_deformation/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_joint_motion/contracts/PolynomialGeneralChartContract.leanpolynomial_joint_motion/contracts/PolynomialHomeomorphContract.leanpolynomial_joint_motion/contracts/PolynomialJointMotionContracts.leanpolynomial_joint_motion/contracts/PolynomialLocalMapContract.leanpolynomial_joint_motion/contracts/PolynomialPadicUniqueContract.leanpolynomial_joint_motion/contracts/PolynomialParameterTowerContracts.leanpolynomial_joint_motion/contracts/PolynomialPrescribedContract.leanpolynomial_joint_motion/contracts/PolynomialRootMotionContract.leanpolynomial_joint_motion/contracts/PolynomialRootStabilityContract.leanpolynomial_joint_motion/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_joint_motion/contracts/PolynomialWeightedLiftContract.leanpolynomial_joint_motion/contracts/InvalidGlobalUniqueness.leanpolynomial_joint_motion/controls/InvalidJointMissingParameterTerm.leanpolynomial_joint_motion/controls/InvalidJointParameterSign.leanpolynomial_joint_motion/controls/InvalidMotionExtraErrorDigit.leanpolynomial_joint_motion/controls/InvalidPerturbationExtraPrecision.leanpolynomial_joint_motion/controls/InvalidPrescribedFullJacobian.leanpolynomial_joint_motion/controls/InvalidPrescribedParameter.leanpolynomial_joint_motion/controls/InvalidPrescribedRectangularUniqueness.leanpolynomial_joint_motion/controls/InvalidRectangularUniqueness.leanpolynomial_joint_motion/controls/InvalidWeightedBoundary.leanpolynomial_joint_motion/controls/InvalidWeightedExtraPrecision.leanpolynomial_joint_motion/controls/PolynomialDeformationControls.leanpolynomial_joint_motion/controls/PolynomialJointMotionControls.leanpolynomial_joint_motion/controls/PolynomialMotionControls.leanpolynomial_joint_motion/controls/PolynomialParameterControls.leanpolynomial_joint_motion/controls/PolynomialParameterTowerControls.leanpolynomial_joint_motion/controls/PolynomialPrescribedControls.leanpolynomial_joint_motion/controls/PolynomialWeightedControls.leanpolynomial_joint_motion/controls/AffineObstructionCore.leanpolynomial_joint_motion/formalization/FiniteFiberCounts.leanpolynomial_joint_motion/formalization/IntegerFiniteCokernel.leanpolynomial_joint_motion/formalization/PadicTowerLimit.leanpolynomial_joint_motion/formalization/PolynomialBlockInverse.leanpolynomial_joint_motion/formalization/PolynomialCoefficientPerturbation.leanpolynomial_joint_motion/formalization/PolynomialCoordinateReorder.leanpolynomial_joint_motion/formalization/PolynomialDigitBridge.leanpolynomial_joint_motion/formalization/PolynomialGeneralChart.leanpolynomial_joint_motion/formalization/PolynomialIntegerTower.leanpolynomial_joint_motion/formalization/PolynomialInverseCongruence.leanpolynomial_joint_motion/formalization/PolynomialJointDeformation.leanpolynomial_joint_motion/formalization/PolynomialJointMotion.leanpolynomial_joint_motion/formalization/PolynomialJointSystem.leanpolynomial_joint_motion/formalization/PolynomialLiftCounts.leanpolynomial_joint_motion/formalization/PolynomialLocalInverse.leanpolynomial_joint_motion/formalization/PolynomialLocalSurjective.leanpolynomial_joint_motion/formalization/PolynomialMinorSelection.leanpolynomial_joint_motion/formalization/PolynomialMotionEstimate.leanpolynomial_joint_motion/formalization/PolynomialMotionNormalization.leanpolynomial_joint_motion/formalization/PolynomialMotionRational.leanpolynomial_joint_motion/formalization/PolynomialObstruction.leanpolynomial_joint_motion/formalization/PolynomialPadicContraction.leanpolynomial_joint_motion/formalization/PolynomialPadicLift.leanpolynomial_joint_motion/formalization/PolynomialPadicUnique.leanpolynomial_joint_motion/formalization/PolynomialParameterChart.leanpolynomial_joint_motion/formalization/PolynomialParameterPath.leanpolynomial_joint_motion/formalization/PolynomialParameterSystem.leanpolynomial_joint_motion/formalization/PolynomialPrescribedCounts.leanpolynomial_joint_motion/formalization/PolynomialPrescribedIntegerTower.leanpolynomial_joint_motion/formalization/PolynomialPrescribedLifts.leanpolynomial_joint_motion/formalization/PolynomialPrescribedObstruction.leanpolynomial_joint_motion/formalization/PolynomialPrescribedPadicTower.leanpolynomial_joint_motion/formalization/PolynomialPrescribedStep.leanpolynomial_joint_motion/formalization/PolynomialPrescribedSystem.leanpolynomial_joint_motion/formalization/PolynomialPrescribedTowerLimit.leanpolynomial_joint_motion/formalization/PolynomialPrescribedTowerUnique.leanpolynomial_joint_motion/formalization/PolynomialRootMotion.leanpolynomial_joint_motion/formalization/PolynomialRootStability.leanpolynomial_joint_motion/formalization/PolynomialSmoothCounts.leanpolynomial_joint_motion/formalization/PolynomialSurjectiveStep.leanpolynomial_joint_motion/formalization/PolynomialTaylor.leanpolynomial_joint_motion/formalization/PolynomialTaylorDisplacement.leanpolynomial_joint_motion/formalization/PolynomialTaylorRing.leanpolynomial_joint_motion/formalization/PolynomialTowerControls.leanpolynomial_joint_motion/formalization/PolynomialWeightedInverse.leanpolynomial_joint_motion/formalization/PolynomialWeightedLift.leanpolynomial_joint_motion/formalization/PolynomialWeightedNormalization.leanpolynomial_joint_motion/formalization/ResidueLiftDigits.leanpolynomial_joint_motion/formalization/PolynomialJointMotionAxiomAudit.leanpolynomial_joint_motion/verification/PolynomialObstructionContract.leanpolynomial_lifting/contracts/PolynomialRepresentativeContract.leanpolynomial_lifting/contracts/PolynomialSharedContract.leanpolynomial_lifting/contracts/PolynomialTaylorContract.leanpolynomial_lifting/contracts/InvalidSeparateImpliesCommon.leanpolynomial_lifting/controls/InvalidSingularLift.leanpolynomial_lifting/controls/InvalidZeroDepthTaylor.leanpolynomial_lifting/controls/PolynomialObstruction.leanpolynomial_lifting/development/obstruction/PolynomialShared.leanpolynomial_lifting/development/obstruction/PolynomialRepresentative.leanpolynomial_lifting/development/representative/PolynomialTaylor.leanpolynomial_lifting/development/taylor/TaylorAudit.leanpolynomial_lifting/development/taylor/AffineObstructionCore.leanpolynomial_lifting/formalization/AffinePairTransport.leanpolynomial_lifting/formalization/AffineSharedCorrection.leanpolynomial_lifting/formalization/PolynomialControls.leanpolynomial_lifting/formalization/PolynomialObstruction.leanpolynomial_lifting/formalization/PolynomialRepresentative.leanpolynomial_lifting/formalization/PolynomialShared.leanpolynomial_lifting/formalization/PolynomialTaylor.leanpolynomial_lifting/formalization/SharedCorrection.leanpolynomial_lifting/formalization/PolynomialAxiomAudit.leanpolynomial_lifting/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_motion/contracts/PolynomialGeneralChartContract.leanpolynomial_motion/contracts/PolynomialHomeomorphContract.leanpolynomial_motion/contracts/PolynomialLocalMapContract.leanpolynomial_motion/contracts/PolynomialPadicUniqueContract.leanpolynomial_motion/contracts/PolynomialRootMotionContract.leanpolynomial_motion/contracts/PolynomialRootStabilityContract.leanpolynomial_motion/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_motion/contracts/PolynomialWeightedLiftContract.leanpolynomial_motion/contracts/InvalidGlobalUniqueness.leanpolynomial_motion/controls/InvalidMotionExtraErrorDigit.leanpolynomial_motion/controls/InvalidPerturbationExtraPrecision.leanpolynomial_motion/controls/InvalidPrescribedParameter.leanpolynomial_motion/controls/InvalidRectangularUniqueness.leanpolynomial_motion/controls/InvalidWeightedBoundary.leanpolynomial_motion/controls/InvalidWeightedExtraPrecision.leanpolynomial_motion/controls/PolynomialDeformationControls.leanpolynomial_motion/controls/PolynomialMotionControls.leanpolynomial_motion/controls/PolynomialParameterControls.leanpolynomial_motion/controls/PolynomialWeightedControls.leanpolynomial_motion/controls/compile_01.leanpolynomial_motion/dev/normalization/AffineObstructionCore.leanpolynomial_motion/formalization/FiniteFiberCounts.leanpolynomial_motion/formalization/IntegerFiniteCokernel.leanpolynomial_motion/formalization/PadicTowerLimit.leanpolynomial_motion/formalization/PolynomialCoefficientPerturbation.leanpolynomial_motion/formalization/PolynomialCoordinateReorder.leanpolynomial_motion/formalization/PolynomialDigitBridge.leanpolynomial_motion/formalization/PolynomialGeneralChart.leanpolynomial_motion/formalization/PolynomialIntegerTower.leanpolynomial_motion/formalization/PolynomialInverseCongruence.leanpolynomial_motion/formalization/PolynomialLiftCounts.leanpolynomial_motion/formalization/PolynomialLocalInverse.leanpolynomial_motion/formalization/PolynomialLocalSurjective.leanpolynomial_motion/formalization/PolynomialMinorSelection.leanpolynomial_motion/formalization/PolynomialMotionEstimate.leanpolynomial_motion/formalization/PolynomialMotionNormalization.leanpolynomial_motion/formalization/PolynomialMotionRational.leanpolynomial_motion/formalization/PolynomialObstruction.leanpolynomial_motion/formalization/PolynomialPadicContraction.leanpolynomial_motion/formalization/PolynomialPadicLift.leanpolynomial_motion/formalization/PolynomialPadicUnique.leanpolynomial_motion/formalization/PolynomialParameterChart.leanpolynomial_motion/formalization/PolynomialParameterSystem.leanpolynomial_motion/formalization/PolynomialRootMotion.leanpolynomial_motion/formalization/PolynomialRootStability.leanpolynomial_motion/formalization/PolynomialSmoothCounts.leanpolynomial_motion/formalization/PolynomialSurjectiveStep.leanpolynomial_motion/formalization/PolynomialTaylor.leanpolynomial_motion/formalization/PolynomialTaylorDisplacement.leanpolynomial_motion/formalization/PolynomialTaylorRing.leanpolynomial_motion/formalization/PolynomialTowerControls.leanpolynomial_motion/formalization/PolynomialWeightedInverse.leanpolynomial_motion/formalization/PolynomialWeightedLift.leanpolynomial_motion/formalization/PolynomialWeightedNormalization.leanpolynomial_motion/formalization/ResidueLiftDigits.leanpolynomial_motion/formalization/PolynomialMotionAxiomAudit.leanpolynomial_motion/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_parameter_towers/contracts/PolynomialGeneralChartContract.leanpolynomial_parameter_towers/contracts/PolynomialHomeomorphContract.leanpolynomial_parameter_towers/contracts/PolynomialLocalMapContract.leanpolynomial_parameter_towers/contracts/PolynomialPadicUniqueContract.leanpolynomial_parameter_towers/contracts/PolynomialParameterTowerContracts.leanpolynomial_parameter_towers/contracts/PolynomialPrescribedContract.leanpolynomial_parameter_towers/contracts/PolynomialRootMotionContract.leanpolynomial_parameter_towers/contracts/PolynomialRootStabilityContract.leanpolynomial_parameter_towers/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_parameter_towers/contracts/PolynomialWeightedLiftContract.leanpolynomial_parameter_towers/contracts/InvalidGlobalUniqueness.leanpolynomial_parameter_towers/controls/InvalidMotionExtraErrorDigit.leanpolynomial_parameter_towers/controls/InvalidPerturbationExtraPrecision.leanpolynomial_parameter_towers/controls/InvalidPrescribedFullJacobian.leanpolynomial_parameter_towers/controls/InvalidPrescribedParameter.leanpolynomial_parameter_towers/controls/InvalidPrescribedRectangularUniqueness.leanpolynomial_parameter_towers/controls/InvalidRectangularUniqueness.leanpolynomial_parameter_towers/controls/InvalidWeightedBoundary.leanpolynomial_parameter_towers/controls/InvalidWeightedExtraPrecision.leanpolynomial_parameter_towers/controls/PolynomialDeformationControls.leanpolynomial_parameter_towers/controls/PolynomialMotionControls.leanpolynomial_parameter_towers/controls/PolynomialParameterControls.leanpolynomial_parameter_towers/controls/PolynomialParameterTowerControls.leanpolynomial_parameter_towers/controls/PolynomialPrescribedControls.leanpolynomial_parameter_towers/controls/PolynomialWeightedControls.leanpolynomial_parameter_towers/controls/AffineObstructionCore.leanpolynomial_parameter_towers/formalization/FiniteFiberCounts.leanpolynomial_parameter_towers/formalization/IntegerFiniteCokernel.leanpolynomial_parameter_towers/formalization/PadicTowerLimit.leanpolynomial_parameter_towers/formalization/PolynomialCoefficientPerturbation.leanpolynomial_parameter_towers/formalization/PolynomialCoordinateReorder.leanpolynomial_parameter_towers/formalization/PolynomialDigitBridge.leanpolynomial_parameter_towers/formalization/PolynomialGeneralChart.leanpolynomial_parameter_towers/formalization/PolynomialIntegerTower.leanpolynomial_parameter_towers/formalization/PolynomialInverseCongruence.leanpolynomial_parameter_towers/formalization/PolynomialLiftCounts.leanpolynomial_parameter_towers/formalization/PolynomialLocalInverse.leanpolynomial_parameter_towers/formalization/PolynomialLocalSurjective.leanpolynomial_parameter_towers/formalization/PolynomialMinorSelection.leanpolynomial_parameter_towers/formalization/PolynomialMotionEstimate.leanpolynomial_parameter_towers/formalization/PolynomialMotionNormalization.leanpolynomial_parameter_towers/formalization/PolynomialMotionRational.leanpolynomial_parameter_towers/formalization/PolynomialObstruction.leanpolynomial_parameter_towers/formalization/PolynomialPadicContraction.leanpolynomial_parameter_towers/formalization/PolynomialPadicLift.leanpolynomial_parameter_towers/formalization/PolynomialPadicUnique.leanpolynomial_parameter_towers/formalization/PolynomialParameterChart.leanpolynomial_parameter_towers/formalization/PolynomialParameterPath.leanpolynomial_parameter_towers/formalization/PolynomialParameterSystem.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedCounts.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedIntegerTower.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedLifts.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedObstruction.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedPadicTower.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedStep.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedSystem.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedTowerLimit.leanpolynomial_parameter_towers/formalization/PolynomialPrescribedTowerUnique.leanpolynomial_parameter_towers/formalization/PolynomialRootMotion.leanpolynomial_parameter_towers/formalization/PolynomialRootStability.leanpolynomial_parameter_towers/formalization/PolynomialSmoothCounts.leanpolynomial_parameter_towers/formalization/PolynomialSurjectiveStep.leanpolynomial_parameter_towers/formalization/PolynomialTaylor.leanpolynomial_parameter_towers/formalization/PolynomialTaylorDisplacement.leanpolynomial_parameter_towers/formalization/PolynomialTaylorRing.leanpolynomial_parameter_towers/formalization/PolynomialTowerControls.leanpolynomial_parameter_towers/formalization/PolynomialWeightedInverse.leanpolynomial_parameter_towers/formalization/PolynomialWeightedLift.leanpolynomial_parameter_towers/formalization/PolynomialWeightedNormalization.leanpolynomial_parameter_towers/formalization/ResidueLiftDigits.leanpolynomial_parameter_towers/formalization/PolynomialParameterTowerAxiomAudit.leanpolynomial_parameter_towers/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_prescribed/contracts/PolynomialGeneralChartContract.leanpolynomial_prescribed/contracts/PolynomialHomeomorphContract.leanpolynomial_prescribed/contracts/PolynomialLocalMapContract.leanpolynomial_prescribed/contracts/PolynomialPadicUniqueContract.leanpolynomial_prescribed/contracts/PolynomialPrescribedContract.leanpolynomial_prescribed/contracts/PolynomialRootMotionContract.leanpolynomial_prescribed/contracts/PolynomialRootStabilityContract.leanpolynomial_prescribed/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_prescribed/contracts/PolynomialWeightedLiftContract.leanpolynomial_prescribed/contracts/InvalidGlobalUniqueness.leanpolynomial_prescribed/controls/InvalidMotionExtraErrorDigit.leanpolynomial_prescribed/controls/InvalidPerturbationExtraPrecision.leanpolynomial_prescribed/controls/InvalidPrescribedFullJacobian.leanpolynomial_prescribed/controls/InvalidPrescribedParameter.leanpolynomial_prescribed/controls/InvalidRectangularUniqueness.leanpolynomial_prescribed/controls/InvalidWeightedBoundary.leanpolynomial_prescribed/controls/InvalidWeightedExtraPrecision.leanpolynomial_prescribed/controls/PolynomialDeformationControls.leanpolynomial_prescribed/controls/PolynomialMotionControls.leanpolynomial_prescribed/controls/PolynomialParameterControls.leanpolynomial_prescribed/controls/PolynomialPrescribedControls.leanpolynomial_prescribed/controls/PolynomialWeightedControls.leanpolynomial_prescribed/controls/compile_02.leanpolynomial_prescribed/dev/counts/PolynomialPrescribedLifts_attempt01.leanpolynomial_prescribed/dev/lifts/compile_02_source.leanpolynomial_prescribed/dev/main/AffineObstructionCore.leanpolynomial_prescribed/formalization/FiniteFiberCounts.leanpolynomial_prescribed/formalization/IntegerFiniteCokernel.leanpolynomial_prescribed/formalization/PadicTowerLimit.leanpolynomial_prescribed/formalization/PolynomialCoefficientPerturbation.leanpolynomial_prescribed/formalization/PolynomialCoordinateReorder.leanpolynomial_prescribed/formalization/PolynomialDigitBridge.leanpolynomial_prescribed/formalization/PolynomialGeneralChart.leanpolynomial_prescribed/formalization/PolynomialIntegerTower.leanpolynomial_prescribed/formalization/PolynomialInverseCongruence.leanpolynomial_prescribed/formalization/PolynomialLiftCounts.leanpolynomial_prescribed/formalization/PolynomialLocalInverse.leanpolynomial_prescribed/formalization/PolynomialLocalSurjective.leanpolynomial_prescribed/formalization/PolynomialMinorSelection.leanpolynomial_prescribed/formalization/PolynomialMotionEstimate.leanpolynomial_prescribed/formalization/PolynomialMotionNormalization.leanpolynomial_prescribed/formalization/PolynomialMotionRational.leanpolynomial_prescribed/formalization/PolynomialObstruction.leanpolynomial_prescribed/formalization/PolynomialPadicContraction.leanpolynomial_prescribed/formalization/PolynomialPadicLift.leanpolynomial_prescribed/formalization/PolynomialPadicUnique.leanpolynomial_prescribed/formalization/PolynomialParameterChart.leanpolynomial_prescribed/formalization/PolynomialParameterSystem.leanpolynomial_prescribed/formalization/PolynomialPrescribedCounts.leanpolynomial_prescribed/formalization/PolynomialPrescribedLifts.leanpolynomial_prescribed/formalization/PolynomialPrescribedObstruction.leanpolynomial_prescribed/formalization/PolynomialPrescribedSystem.leanpolynomial_prescribed/formalization/PolynomialRootMotion.leanpolynomial_prescribed/formalization/PolynomialRootStability.leanpolynomial_prescribed/formalization/PolynomialSmoothCounts.leanpolynomial_prescribed/formalization/PolynomialSurjectiveStep.leanpolynomial_prescribed/formalization/PolynomialTaylor.leanpolynomial_prescribed/formalization/PolynomialTaylorDisplacement.leanpolynomial_prescribed/formalization/PolynomialTaylorRing.leanpolynomial_prescribed/formalization/PolynomialTowerControls.leanpolynomial_prescribed/formalization/PolynomialWeightedInverse.leanpolynomial_prescribed/formalization/PolynomialWeightedLift.leanpolynomial_prescribed/formalization/PolynomialWeightedNormalization.leanpolynomial_prescribed/formalization/ResidueLiftDigits.leanpolynomial_prescribed/formalization/PolynomialPrescribedAxiomAudit.leanpolynomial_prescribed/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_regularity/contracts/PolynomialGeneralChartContract.leanpolynomial_regularity/contracts/PolynomialHomeomorphContract.leanpolynomial_regularity/contracts/PolynomialJointMotionContracts.leanpolynomial_regularity/contracts/PolynomialLocalMapContract.leanpolynomial_regularity/contracts/PolynomialPadicUniqueContract.leanpolynomial_regularity/contracts/PolynomialParameterTowerContracts.leanpolynomial_regularity/contracts/PolynomialPrescribedContract.leanpolynomial_regularity/contracts/PolynomialRegularityContracts.leanpolynomial_regularity/contracts/PolynomialRootMotionContract.leanpolynomial_regularity/contracts/PolynomialRootStabilityContract.leanpolynomial_regularity/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_regularity/contracts/PolynomialWeightedLiftContract.leanpolynomial_regularity/contracts/InvalidGlobalUniqueness.leanpolynomial_regularity/controls/InvalidJointMissingParameterTerm.leanpolynomial_regularity/controls/InvalidJointParameterSign.leanpolynomial_regularity/controls/InvalidMotionExtraErrorDigit.leanpolynomial_regularity/controls/InvalidPerturbationExtraPrecision.leanpolynomial_regularity/controls/InvalidPrescribedFullJacobian.leanpolynomial_regularity/controls/InvalidPrescribedParameter.leanpolynomial_regularity/controls/InvalidPrescribedRectangularUniqueness.leanpolynomial_regularity/controls/InvalidRectangularUniqueness.leanpolynomial_regularity/controls/InvalidRegularityDerivativeSign.leanpolynomial_regularity/controls/InvalidWeightedBoundary.leanpolynomial_regularity/controls/InvalidWeightedExtraPrecision.leanpolynomial_regularity/controls/PolynomialDeformationControls.leanpolynomial_regularity/controls/PolynomialJointMotionControls.leanpolynomial_regularity/controls/PolynomialMotionControls.leanpolynomial_regularity/controls/PolynomialParameterControls.leanpolynomial_regularity/controls/PolynomialParameterTowerControls.leanpolynomial_regularity/controls/PolynomialPrescribedControls.leanpolynomial_regularity/controls/PolynomialRegularityControls.leanpolynomial_regularity/controls/PolynomialWeightedControls.leanpolynomial_regularity/controls/AffineObstructionCore.leanpolynomial_regularity/formalization/FiniteFiberCounts.leanpolynomial_regularity/formalization/IntegerFiniteCokernel.leanpolynomial_regularity/formalization/PadicTowerLimit.leanpolynomial_regularity/formalization/PolynomialAnalyticBlocks.leanpolynomial_regularity/formalization/PolynomialAnalyticEvaluation.leanpolynomial_regularity/formalization/PolynomialAnalyticImplicit.leanpolynomial_regularity/formalization/PolynomialAnalyticInverse.leanpolynomial_regularity/formalization/PolynomialAnalyticSelection.leanpolynomial_regularity/formalization/PolynomialBlockInverse.leanpolynomial_regularity/formalization/PolynomialCoefficientPerturbation.leanpolynomial_regularity/formalization/PolynomialCoordinateReorder.leanpolynomial_regularity/formalization/PolynomialDigitBridge.leanpolynomial_regularity/formalization/PolynomialGeneralChart.leanpolynomial_regularity/formalization/PolynomialIntegerTower.leanpolynomial_regularity/formalization/PolynomialInverseCongruence.leanpolynomial_regularity/formalization/PolynomialJointDeformation.leanpolynomial_regularity/formalization/PolynomialJointMotion.leanpolynomial_regularity/formalization/PolynomialJointSystem.leanpolynomial_regularity/formalization/PolynomialLiftCounts.leanpolynomial_regularity/formalization/PolynomialLocalInverse.leanpolynomial_regularity/formalization/PolynomialLocalSurjective.leanpolynomial_regularity/formalization/PolynomialMinorSelection.leanpolynomial_regularity/formalization/PolynomialMotionEstimate.leanpolynomial_regularity/formalization/PolynomialMotionNormalization.leanpolynomial_regularity/formalization/PolynomialMotionRational.leanpolynomial_regularity/formalization/PolynomialObstruction.leanpolynomial_regularity/formalization/PolynomialPadicContraction.leanpolynomial_regularity/formalization/PolynomialPadicLift.leanpolynomial_regularity/formalization/PolynomialPadicUnique.leanpolynomial_regularity/formalization/PolynomialParameterChart.leanpolynomial_regularity/formalization/PolynomialParameterPath.leanpolynomial_regularity/formalization/PolynomialParameterSystem.leanpolynomial_regularity/formalization/PolynomialPrescribedCounts.leanpolynomial_regularity/formalization/PolynomialPrescribedIntegerTower.leanpolynomial_regularity/formalization/PolynomialPrescribedLifts.leanpolynomial_regularity/formalization/PolynomialPrescribedObstruction.leanpolynomial_regularity/formalization/PolynomialPrescribedPadicTower.leanpolynomial_regularity/formalization/PolynomialPrescribedStep.leanpolynomial_regularity/formalization/PolynomialPrescribedSystem.leanpolynomial_regularity/formalization/PolynomialPrescribedTowerLimit.leanpolynomial_regularity/formalization/PolynomialPrescribedTowerUnique.leanpolynomial_regularity/formalization/PolynomialRegularityIntegral.leanpolynomial_regularity/formalization/PolynomialRootMotion.leanpolynomial_regularity/formalization/PolynomialRootStability.leanpolynomial_regularity/formalization/PolynomialSmoothCounts.leanpolynomial_regularity/formalization/PolynomialSurjectiveStep.leanpolynomial_regularity/formalization/PolynomialTaylor.leanpolynomial_regularity/formalization/PolynomialTaylorDisplacement.leanpolynomial_regularity/formalization/PolynomialTaylorRing.leanpolynomial_regularity/formalization/PolynomialTowerControls.leanpolynomial_regularity/formalization/PolynomialWeightedInverse.leanpolynomial_regularity/formalization/PolynomialWeightedLift.leanpolynomial_regularity/formalization/PolynomialWeightedNormalization.leanpolynomial_regularity/formalization/ResidueLiftDigits.leanpolynomial_regularity/formalization/PolynomialRegularityAxiomAudit.leanpolynomial_regularity/verification/PadicTowerLimitContract.leanpolynomial_towers/contracts/PolynomialPadicLiftContract.leanpolynomial_towers/contracts/PolynomialTowerContract.leanpolynomial_towers/contracts/InvalidExtraPrecision.leanpolynomial_towers/controls/InvalidRectangularUniqueness.leanpolynomial_towers/controls/InvalidSingularInfiniteLift.leanpolynomial_towers/controls/PadicTowerLimit.leanpolynomial_towers/development/limit/PadicTowerLimitAudit.leanpolynomial_towers/development/limit/PolynomialPadicLift.leanpolynomial_towers/development/padic/PolynomialSurjectiveStep.leanpolynomial_towers/development/step/PolynomialIntegerTower.leanpolynomial_towers/development/tower/PolynomialSmoothCounts.leanpolynomial_towers/development/tower/AffineObstructionCore.leanpolynomial_towers/formalization/FiniteFiberCounts.leanpolynomial_towers/formalization/IntegerFiniteCokernel.leanpolynomial_towers/formalization/PadicTowerLimit.leanpolynomial_towers/formalization/PolynomialDigitBridge.leanpolynomial_towers/formalization/PolynomialIntegerTower.leanpolynomial_towers/formalization/PolynomialLiftCounts.leanpolynomial_towers/formalization/PolynomialObstruction.leanpolynomial_towers/formalization/PolynomialPadicLift.leanpolynomial_towers/formalization/PolynomialSmoothCounts.leanpolynomial_towers/formalization/PolynomialSurjectiveStep.leanpolynomial_towers/formalization/PolynomialTaylor.leanpolynomial_towers/formalization/PolynomialTowerControls.leanpolynomial_towers/formalization/ResidueLiftDigits.leanpolynomial_towers/formalization/PolynomialTowersAxiomAudit.leanpolynomial_towers/verification/PolynomialCoefficientPerturbationContract.leanpolynomial_weighted/contracts/PolynomialGeneralChartContract.leanpolynomial_weighted/contracts/PolynomialHomeomorphContract.leanpolynomial_weighted/contracts/PolynomialLocalMapContract.leanpolynomial_weighted/contracts/PolynomialPadicUniqueContract.leanpolynomial_weighted/contracts/PolynomialRootStabilityContract.leanpolynomial_weighted/contracts/PolynomialWeightedAuxiliaryContract.leanpolynomial_weighted/contracts/PolynomialWeightedLiftContract.leanpolynomial_weighted/contracts/InvalidGlobalUniqueness.leanpolynomial_weighted/controls/InvalidPerturbationExtraPrecision.leanpolynomial_weighted/controls/InvalidPrescribedParameter.leanpolynomial_weighted/controls/InvalidRectangularUniqueness.leanpolynomial_weighted/controls/InvalidWeightedBoundary.leanpolynomial_weighted/controls/InvalidWeightedExtraPrecision.leanpolynomial_weighted/controls/PolynomialDeformationControls.leanpolynomial_weighted/controls/PolynomialParameterControls.leanpolynomial_weighted/controls/PolynomialWeightedControls.leanpolynomial_weighted/controls/ContractionAxiomAudit.leanpolynomial_weighted/dev/contraction/AffineObstructionCore.leanpolynomial_weighted/formalization/FiniteFiberCounts.leanpolynomial_weighted/formalization/IntegerFiniteCokernel.leanpolynomial_weighted/formalization/PadicTowerLimit.leanpolynomial_weighted/formalization/PolynomialCoefficientPerturbation.leanpolynomial_weighted/formalization/PolynomialCoordinateReorder.leanpolynomial_weighted/formalization/PolynomialDigitBridge.leanpolynomial_weighted/formalization/PolynomialGeneralChart.leanpolynomial_weighted/formalization/PolynomialIntegerTower.leanpolynomial_weighted/formalization/PolynomialInverseCongruence.leanpolynomial_weighted/formalization/PolynomialLiftCounts.leanpolynomial_weighted/formalization/PolynomialLocalInverse.leanpolynomial_weighted/formalization/PolynomialLocalSurjective.leanpolynomial_weighted/formalization/PolynomialMinorSelection.leanpolynomial_weighted/formalization/PolynomialObstruction.leanpolynomial_weighted/formalization/PolynomialPadicContraction.leanpolynomial_weighted/formalization/PolynomialPadicLift.leanpolynomial_weighted/formalization/PolynomialPadicUnique.leanpolynomial_weighted/formalization/PolynomialParameterChart.leanpolynomial_weighted/formalization/PolynomialParameterSystem.leanpolynomial_weighted/formalization/PolynomialRootStability.leanpolynomial_weighted/formalization/PolynomialSmoothCounts.leanpolynomial_weighted/formalization/PolynomialSurjectiveStep.leanpolynomial_weighted/formalization/PolynomialTaylor.leanpolynomial_weighted/formalization/PolynomialTaylorRing.leanpolynomial_weighted/formalization/PolynomialTowerControls.leanpolynomial_weighted/formalization/PolynomialWeightedInverse.leanpolynomial_weighted/formalization/PolynomialWeightedLift.leanpolynomial_weighted/formalization/PolynomialWeightedNormalization.leanpolynomial_weighted/formalization/ResidueLiftDigits.leanpolynomial_weighted/formalization/PolynomialWeightedAxiomAudit.leanpolynomial_weighted/verification/Audit.leanreview/fresh_baseline/ExternalStatement.leanreview/fresh_baseline/negative_false_composite_binomial_divisibility.leanreview/fresh_baseline/negative_false_constant_normalization.leanreview/fresh_baseline/negative_false_dyadic_extra_power.leanreview/fresh_baseline/negative_false_dyadic_extra_precision.leanreview/fresh_baseline/negative_false_dyadic_scale.leanreview/fresh_baseline/negative_false_dyadic_sign_collapse.leanreview/fresh_baseline/negative_false_even_length.leanreview/fresh_baseline/negative_false_finite_sample_extension.leanreview/fresh_baseline/negative_false_global_no_factorial_loss.leanreview/fresh_baseline/negative_false_nonunit_gain.leanreview/fresh_baseline/negative_false_period_at_zero.leanreview/fresh_baseline/negative_false_period_mod_p_squared.leanreview/fresh_baseline/negative_false_singular_ratio_normalization.leanreview/fresh_baseline/negative_false_unjumped_matrix.leanreview/fresh_baseline/negative_false_unlifted_root.leanreview/fresh_baseline/negative_false_window_extra_power.leanreview/fresh_baseline/negative_placeholder.leanreview/fresh_baseline/AffinePairContract.leanshared_correction/controls/InvalidQuotientEquality.leanshared_correction/controls/InvalidUnconditionalSolvability.leanshared_correction/controls/NegativeAffineJointLift.leanshared_correction/controls/SharedCorrectionContract.leanshared_correction/controls/AffineObstructionCore.leanshared_correction/formalization/AffinePairControls.leanshared_correction/formalization/AffinePairTransport.leanshared_correction/formalization/AffineSharedCorrection.leanshared_correction/formalization/SharedCorrection.leanshared_correction/formalization/SharedCorrectionControls.leanshared_correction/formalization/SharedAxiomAudit.leanshared_correction/verification/DyadicIsometryContract.leanstrengthening/controls/ExactPeriodStatementContract.leanstrengthening/controls/InvalidKappaValuation.leanstrengthening/controls/InvalidSharpness.leanstrengthening/controls/NegativeAddressRange.leanstrengthening/controls/NegativeExactExtraDigit.leanstrengthening/controls/NegativeHalfPeriodAddress.leanstrengthening/controls/NegativeIsometrySign.leanstrengthening/controls/NegativeLeastPeriodOne.leanstrengthening/controls/NegativeOldRowBound.leanstrengthening/controls/NegativeOriginalSurjectivity.leanstrengthening/controls/NegativeZeroShiftExactness.leanstrengthening/controls/StrengtheningStatementContract.leanstrengthening/controls/WrongDyadicExponent.leanstrengthening/controls/AllResidueStepAmplification.leanstrengthening/formalization/AllRowsControls.leanstrengthening/formalization/ChargedDworkClosure.leanstrengthening/formalization/CompactSelfIsometry.leanstrengthening/formalization/DensePadicIsometry.leanstrengthening/formalization/DyadicFourAllRows.leanstrengthening/formalization/DyadicFourFinalStrengthening.leanstrengthening/formalization/DyadicFourIsometry.leanstrengthening/formalization/DyadicFourLeastPeriods.leanstrengthening/formalization/DyadicFourPrefix.leanstrengthening/formalization/DyadicFourSharpening.leanstrengthening/formalization/DyadicIsometryControls.leanstrengthening/formalization/DyadicLogThresholds.leanstrengthening/formalization/DyadicPacketRational.leanstrengthening/formalization/DyadicSharpTower.leanstrengthening/formalization/DyadicStepAmplification.leanstrengthening/formalization/ExactPeriodClassification.leanstrengthening/formalization/ExactPeriodControls.leanstrengthening/formalization/NewtonDominance.leanstrengthening/formalization/RationalPadicEmbedding.leanstrengthening/formalization/StepAmplification.leanstrengthening/formalization/StepAmplificationExamples.leanstrengthening/formalization/ContinuationAxiomAudit.leanstrengthening/provenance/exact_period_verification/ContinuationAxiomAudit.leanstrengthening/provenance/sharp_dyadic_verification/ContinuationAxiomAudit.leanstrengthening/verification/