Splitting one hybrid coordinate into a next-bit experiment -- proof internals

theorem Complexity.BitGenerator.candidateAcceptanceProbability_eq_hybrid_internal {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) (step : Fin outputLength) : NextBitPrediction.candidateAcceptanceProbability (generator.testAtCandidate test step) = generator.hybridAcceptanceProbability test ↑step

theorem Complexity.BitGenerator.targetAcceptanceProbability_eq_nextHybrid_internal {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) (step : Fin outputLength) : NextBitPrediction.targetAcceptanceProbability (generator.targetBit step) (generator.testAtCandidate test step) = generator.hybridAcceptanceProbability test (↑step + 1)

theorem Complexity.BitGenerator.predictionSuccessProbability_eq_half_add_hybridGap_internal {seedLength outputLength : ℕ} (generator : BitGenerator seedLength outputLength) (test : Finset (Fin outputLength → Bool)) (step : Fin outputLength) : NextBitPrediction.successProbability (generator.targetBit step) (generator.testAtCandidate test step) = 1 / 2 + generator.hybridGap test ↑step