OAI/Analysis/MatrixSigning/Arithmetic/
1324 declarations, 0 contain sorry, 0 declared as axioms; 97 files
Files
- Alpha.lean 16 declarations
- Alpha2.lean 15 declarations
- ArithmeticBounds.lean 10 declarations
- ArithmeticEncodingSize.lean 17 declarations
- BinaryAdder.lean 21 declarations
- BinaryAdderCompose.lean 6 declarations
- BinaryAddressLookup.lean 9 declarations
- BinaryDivision.lean 46 declarations
- BinaryGCD.lean 11 declarations
- BinaryMultiply.lean 19 declarations
- BinaryMultiplySemantics.lean 14 declarations
- BinaryRationalAdd.lean 12 declarations
- BinaryRationalCanonical.lean 5 declarations
- BinaryRationalCore.lean 16 declarations
- BinaryRationalNormalize.lean 6 declarations
- BinarySubtractor.lean 15 declarations
- BisectionArithmetic.lean 27 declarations
- BorrowSubtractor.lean 13 declarations
- CanonicalRationalPairParser.lean 8 declarations
- CanonicalSubtraction.lean 5 declarations
- CleanRationalCompare.lean 25 declarations
- ComplexScalarNodes.lean 25 declarations
- ConvexInnerBall.lean 3 declarations
- CubeInterval.lean 9 declarations
- DivisionBodyTime.lean 8 declarations
- DivisionCompatibility.lean 3 declarations
- DivisionInput.lean 25 declarations
- DivisionLoopBridge.lean 3 declarations
- DivisionLoopModel.lean 10 declarations
- DivisionLoopRun.lean 5 declarations
- DivisionMachine.lean 38 declarations
- DivisionOutput.lean 16 declarations
- EncodedDivision.lean 10 declarations
- EventuallyInterior.lean 4 declarations
- ExactStepDecrease.lean 4 declarations
- FixedBinaryAdder.lean 8 declarations
- FixedSubtraction.lean 2 declarations
- FloorRationalMachine.lean 19 declarations
- GCDMachine.lean 19 declarations
- GCDMachineRun.lean 4 declarations
- GCDMachineStep.lean 5 declarations
- Kappa₁.lean 7 declarations
- MixedYoungBound.lean 2 declarations
- MultiplicationBody.lean 15 declarations
- MultiplicationDeterministic.lean 10 declarations
- MultiplicationInitialize.lean 12 declarations
- MultiplicationLoop.lean 12 declarations
- MultiplicationMachine.lean 15 declarations
- MultiplicationNormalize.lean 9 declarations
- NegativeDivision.lean 13 declarations
- RationalAddCorrect.lean 9 declarations
- RationalAddModel.lean 8 declarations
- RationalAddPorts.lean 4 declarations
- RationalAddPrimitives.lean 10 declarations
- RationalAddProducts.lean 28 declarations
- RationalAddProgram.lean 14 declarations
- RationalAddSigned.lean 26 declarations
- RationalArithmetic.lean 16 declarations
- RationalArithmeticMeter.lean 18 declarations
- RationalBounds.lean 10 declarations
- RationalCompareBranch.lean 13 declarations
- RationalCompareCorrectness.lean 14 declarations
- RationalCompareDeterministic.lean 16 declarations
- RationalCompareParser.lean 13 declarations
- RationalComparePrimitives.lean 16 declarations
- RationalCompareProgram.lean 24 declarations
- RationalDivisionMachine.lean 13 declarations
- RationalDivisionStages.lean 29 declarations
- RationalExpressionHeight.lean 9 declarations
- RationalMagnitudeCorrect.lean 5 declarations
- RationalMagnitudeDivision.lean 17 declarations
- RationalMagnitudeMachine.lean 35 declarations
- RationalMagnitudePositive.lean 2 declarations
- RationalMagnitudeSetup.lean 16 declarations
- RationalMagnitudeSign.lean 11 declarations
- RationalMultiplicationMachine.lean 17 declarations
- RationalMultiplyNormalize.lean 13 declarations
- RationalMultiplyProducts.lean 12 declarations
- RationalReciprocalCore.lean 3 declarations
- RationalReciprocalMachine.lean 13 declarations
- RationalReciprocalSerialize.lean 2 declarations
- RationalReciprocalSwap.lean 13 declarations
- RationalSignAction.lean 34 declarations
- RationalSignClassifier.lean 22 declarations
- RationalSignPorts.lean 4 declarations
- RationalSubtractCorrect.lean 9 declarations
- RationalSubtractPorts.lean 4 declarations
- RationalSubtractProgram.lean 41 declarations
- RealifyAdd.lean 4 declarations
- ScalarPsi.lean 15 declarations
- SignedRationalSerializer.lean 37 declarations
- SingleRationalParser.lean 24 declarations
- SparseScalarNodes.lean 13 declarations
- SubtractionBorrow.lean 7 declarations
- SubtractorSequential.lean 7 declarations
- UnaryArithmetic.lean 11 declarations
- ZeroPaddedRow.lean 12 declarations