# Machine-readable index of the verified proofs hosted in this repo.
#
# This repository-native file is the canonical machine-readable index. External
# tools may consume an exact Git revision, but no downstream service is required
# to discover, build, or audit the proofs.
#
# `axioms_clean: true` is enforced by scripts/check_axioms.sh on every push.
repo: williamjblair/lean-proofs
toolchain: leanprover/lean4:v4.33.0
mathlib: db584cd6d46c92f209a44c0f1c829460d327499d

proofs:
  - problem: 154
    source: erdosproblems
    file: ErdosProblems/Erdos154/Sumset.lean
    theorem: Erdos154.erdos_154_sumset
    statement: >-
      For Sidon sets A with |A| ~ N^{1/2}, the sumset A+A is equidistributed
      over residue classes mod m: each class holds ~1/m of A+A.
    depends_on:
      - "ErdosProblems/Erdos154/Lindstrom.lean (Lindström residue distribution for A; formal authors Aristotle and Wouter van Doorn, via plby/lean-proofs)"
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/154.lean
    fc_pr: https://github.com/google-deepmind/formal-conjectures/pull/4340
  - problem: 94
    source: erdosproblems
    file: ErdosProblems/Erdos94.lean
    theorem: Erdos94.variants.sum_multiplicity
    statement: >-
      The sum of the multiplicities of all distances determined by a finite
      planar point set is the number of unordered pairs of distinct points.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/94.lean
  - problem: 399
    source: erdosproblems
    file: ErdosProblems/Erdos399.lean
    theorem: Erdos399.erdos_399.variants.cambie
    statement: >-
      If x and y are coprime natural numbers with 1 < x*y, then no factorial
      is the sum of their fourth powers.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/399.lean
    fc_commit: 9c4d5821819656af53c5473ded2116ea14a7ff1c
    fc_source_sha256: 79c50670ecacbd211abb8211814729c8e3aacc5c7055f3790842e381e53f36be
    producer_commit: badf9efb9723561d096defbfb7a4567c38fdeb24
    candidate_sha256: ea3d15995219e918c862d01353cbff12c2a74c924335143b0a01366b597dafb6
    evaluation_commit: 08b6fa7c3db48e1cb2fdda1e71c7c7e601e38fd2
    rights: Original proof bytes MIT; exact Formal Conjectures target Apache-2.0
  - problem: 1074
    source: erdosproblems
    file: ErdosProblems/Erdos1074.lean
    theorem: Erdos1074.erdos_1074.variants.EHSNumbers_init
    statement: >-
      The first seven EHS numbers, enumerated by Nat.nth, are exactly
      8, 9, 13, 14, 15, 16, and 17.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/1074.lean
    fc_commit: 9c4d5821819656af53c5473ded2116ea14a7ff1c
    fc_source_sha256: 72b74c90c3fbdf66fedcd744d6c90da05fdfc7e87673a016787ae4586c705c45
    producer_commit: 082a118ea6ce7c9ca6a62f72aa425373228f7efe
    evaluation_commit: be883fe7808e1860373ce19d12d0cb38b409a687
    handoff_commit: beb0b4e6e68a4646c0d7da96597e1f175e2a8d22
    certificate_sha256: aa18c73e7d44b4b45210256370f4d04fce97b5239a37caf7df55be7b223d0637
    certificate_stdout_sha256: 32dbde16b9754e8d3c8419b93bfd95f766e7930967103a1a3b80c8c11e1a0685
    certificate_role: Computational evidence only; not a Lean proof
    rights: Original proof and certificate bytes MIT; exact Formal Conjectures target Apache-2.0
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityTheorem.lean
    theorem: Erdos730.FullDensityTheorem.pairSet_infinite
    statement: >-
      Erdős #730, answered affirmatively: there are infinitely many pairs n < m
      whose central binomial coefficients have identical prime support (the
      proof produces infinitely many consecutive pairs).
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
    palomar_config: Palomar/Erdos730/comparator.json
    palomar_entry: PALOMAR-2026-08-22-000001
    palomar_entry_version: 1
    palomar_entry_url: https://palomar-registry.org/entry.html?id=PALOMAR-2026-08-22-000001&version=1
    palomar_registered_commit: 03729c9cbb0b602f5a828bb850c85e84c5a6d460
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.eight_mul_sq_le_succ_cube
    statement: >-
      For every p at least five, the exact cubic inequality
      8 p squared at most (p+1) cubed certifies the kappa envelope.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.nearEnvelope_forces_high_exponent
    statement: >-
      The rational near-affine envelope forces exponent a at least two and
      the strict relation 19r less than 12a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.nearEnvelope_prime_power_clearance
    statement: >-
      The near envelope gives the exact powered comparison between the next
      analytic block scale and the valuation prime power.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.powered_threshold_of_near_maximal
    statement: >-
      Quantified residue-count maximality and the near envelope imply the
      cleared 38-to-81 prime-power threshold over the rationals.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.finite_prime_power_pair_count
    statement: >-
      A finite exponent-bounded prime-power family obeys the explicit square-
      and cube-root pair-count envelope.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.finite_reciprocal_tail_from_root_envelopes
    statement: >-
      Finite prime-power pair and threshold hypotheses give an exact rational
      reciprocal-tail bound from certified root envelopes.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.finite_geometric_prime_power_tail
    statement: >-
      Every finite exponent tail from a base at least two is bounded by twice
      its first reciprocal cube.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.finite_reciprocal_square_tail
    statement: >-
      Finite reciprocal-square tails satisfy the explicit telescoping upper
      envelope used by the near-affine payment.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.dyadicThresholdBase_strictMono_step
    statement: >-
      The exact rational lower-threshold base increases from one dyadic range
      to the next for every exponent at least 57.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.endpoint_powered_threshold_certificate
    statement: >-
      Exact rational powering certifies the 1210239 threshold at the initial
      dyadic endpoint X equals 2 to the 57.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.endpoint_payment_identity
    statement: >-
      The endpoint tail and boundary envelopes assemble to the recorded exact
      rational payment with no decimal arithmetic.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/NearAffinePayment.lean
    theorem: Erdos730.endpoint_payment_lt_one_percent
    statement: >-
      The exact endpoint rational payment is strictly below one percent.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HalfBandPayment.lean
    theorem: Erdos730.halfBandEnvelope_forces_high_exponent
    statement: >-
      The enlarged half-band condition forces a valuation exponent at least
      two and the exact relation three r less than two a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HalfBandPayment.lean
    theorem: Erdos730.halfBandEnvelope_prime_power_clearance
    statement: >-
      The half-band exponent relation gives the powered comparison needed to
      clear p to the r plus one against p to the a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HalfBandPayment.lean
    theorem: Erdos730.powered_threshold_of_halfBand_maximal
    statement: >-
      Maximal block length in the enlarged half band forces the exact powered
      threshold X to the sixth below the q to the thirteenth envelope.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HalfBandPayment.lean
    theorem: Erdos730.halfBand_endpoint_powered_threshold_certificate
    statement: >-
      Exact rational powers certify the enlarged endpoint threshold floor
      937824 at X equals two to the 57.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HalfBandPayment.lean
    theorem: Erdos730.halfBand_endpoint_payment_lt_one_percent
    statement: >-
      The enlarged half-band endpoint payment remains strictly below one
      percent with a positive exact rational margin.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBandEnvelope_forces_high_exponent
    statement: >-
      The full strict high-valuation band forces exponent at least two and
      the exact clearance r plus one at most a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBandEnvelope_prime_power_clearance
    statement: >-
      The strict-band exponent clearance gives p to r plus one at most p to a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.cutoff_lt_of_unitBand_maximal
    statement: >-
      Residue count and maximal block length force the clean threshold X
      below two times the global weight times q squared.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBandDyadicThresholdBase_strictMono_step
    statement: >-
      The exact dyadic threshold base for the full strict band increases from
      every dyadic exponent at least 57.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_threshold_certificate
    statement: >-
      Exact integer squares certify the endpoint threshold floor 3441480 at
      X equal to two to the 57.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_sqrt_floor_certificate
    statement: >-
      Exact squares certify the square-root floor used in the endpoint tail.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_cuberoot_floor_certificate
    statement: >-
      Exact cubes certify the cube-root floor used in the endpoint tail.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_payment_identity
    statement: >-
      The reciprocal tail and boundary terms assemble to one exact rational
      endpoint payment.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_payment_lt_one_percent
    statement: >-
      The full strict-band endpoint payment is strictly below one percent.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPayment.lean
    theorem: Erdos730.unitBand_endpoint_payment_margin
    statement: >-
      Exact subtraction records the positive cleared one-percent margin.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPaymentAudit.lean
    theorem: Erdos730.audit_unitBandEnvelope_iff
    statement: >-
      For positive r, the paid strict band is exactly equivalent to r plus
      one at most a.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPaymentAudit.lean
    theorem: Erdos730.audit_unitBand_complement_iff
    statement: >-
      For positive r, the unpaid complement is exactly a at most r.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitBandPaymentAudit.lean
    theorem: Erdos730.audit_unitBand_slack_ge_iff
    statement: >-
      The same unpaid complement is equivalent to the natural slack being at
      least r.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitRangeBlock.lean
    theorem: Erdos730.UnitRangeBlock.quadratic_block_expansion
    statement: >-
      Every quadratic branch has an exact Taylor expansion across an aligned
      prime-power block.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitRangeBlock.lean
    theorem: Erdos730.UnitRangeBlock.quadratic_block_difference_dvd_sq
    statement: >-
      After removing the affine block-index term, the aligned quadratic
      remainder is divisible by the square block modulus.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitRangeBlock.lean
    theorem: Erdos730.UnitRangeBlock.normalized_block_cover_cross_bound
    statement: >-
      The critical-length, root-class, and aligned-cover hypotheses imply
      the exact cross-multiplied normalized block bound.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/UnitRangeBlock.lean
    theorem: Erdos730.UnitRangeBlock.higher_prime_power_payment_ceiling_lt_half
    statement: >-
      The exact rational ceiling for the audited higher-prime-power payment
      is strictly below one half.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.first_power_fixed_upper_slope
    statement: >-
      At first power, subtracting the fixed block shift leaves a multiple of
      the square prime modulus.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.normalized_block_cover_six_fifths
    statement: >-
      The sharpened critical length gives the exact cleared six-fifths block
      normalization inequality.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.q_top_low_digit_large
    statement: >-
      The Q-branch top equation and small cofactor force its low digit above
      the restricted half.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.s_top_low_digit_large
    statement: >-
      The S-branch top equation and small cofactor force its low digit above
      the restricted half.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.q_top_small_cofactor_of_square_lt
    statement: >-
      The Q-branch two-digit square bound implies the small-cofactor
      inequality from the explicit threshold 66.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.s_top_small_cofactor_of_square_lt
    statement: >-
      The S-branch two-digit square bound implies the small-cofactor
      inequality from the explicit threshold 1856.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.q_top_two_digit_large
    statement: >-
      Beyond the finite Q threshold, the two-digit top regime is excluded by
      its low base-p digit.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.s_top_two_digit_large
    statement: >-
      Beyond the finite S threshold, the two-digit top regime is excluded by
      its low base-p digit.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.improved_higher_power_ceiling_lt_three_tenths
    statement: >-
      The sharpened higher-prime-power payment ceiling 174 over 625 is below
      three tenths.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FirstPowerRoutes.lean
    theorem: Erdos730.FirstPowerRoutes.remaining_first_power_budget
    statement: >-
      After strict-band and higher-power payments, the exact remaining budget
      is 1779 over 2500.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/KummerTransition.lean
    theorem: Erdos730.KummerTransition.not_dvd_centralBinom_iff_lowerHalfDigits
    statement: >-
      For every odd prime p, p is absent from the central binomial
      coefficient of t exactly when every base-p digit of t lies in the
      lower half; this is the kernel-checked Kummer transition used by the
      full-density proof.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityCore.lean
    theorem: Erdos730.FullDensityCore.product_identity
    statement: >-
      The explicit four-linear-form family satisfies the exact product
      identity 2 P(x) Q(x) = 3 R(x) S(x) + 1 for every parameter x.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityCore.lean
    theorem: Erdos730.FullDensityCore.branches_pairwise_coprime
    statement: >-
      The four branch values P(x), Q(x), R(x), and S(x) in the explicit
      positive-density family are pairwise coprime for every parameter x.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityCore.lean
    theorem: Erdos730.FullDensityCore.switching_allowed_class_count_certificate
    statement: >-
      Exact finite enumeration certifies 20160 allowed reduced classes modulo
      222138 and 13440 allowed reduced classes modulo 148092 in the top-prime
      divisor-switching step.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/PadicIsometry.lean
    theorem: Erdos730.padicBranchMap_bijective
    statement: >-
      A quadratic branch map whose quadratic part is divisible by p and whose
      residual linear coefficient is a p-adic unit permutes every residue
      system modulo p to the j.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/PadicIsometry.lean
    theorem: Erdos730.restrictedDigitBox_card
    statement: >-
      Removing one allowed endpoint from the first digit of a depth-d digit
      box leaves exactly (H-1) times H to the d-1 admissible strings.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityBudget.lean
    theorem: Erdos730.densityBudget_final_lt
    statement: >-
      The complete infinite logarithmic-series certificate proves that four
      times the small-prime budget plus two-thirds log 2 is strictly below
      2393 over 2500.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FixedDepthParity.lean
    theorem: Erdos730.halfDigitParity_probabilityError
    statement: >-
      For the odd half-digit alphabet, the exact normalized even-parity
      discrepancy at depth d is one over twice the d-th power of the alphabet
      size.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HigherPowerCount.lean
    theorem: Erdos730.padicBranchAllowedCount_le
    statement: >-
      A consecutive parameter interval meets an allowed p-adic branch-map
      digit box at most the number of padded complete blocks times the exact
      full-period digit-box count, including depth zero.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ObstructionMaps.lean
    theorem: Erdos730.ObstructionMaps.PhiP_root_progression
    statement: >-
      Substitution along a P-branch prime-power root progression gives the
      exact common quadratic branch map with residual coefficient -246T.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ObstructionMaps.lean
    theorem: Erdos730.ObstructionMaps.PhiQ_root_progression
    statement: >-
      Substitution along a Q-branch prime-power root progression gives the
      exact common quadratic branch map with residual coefficient 246T.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ObstructionMaps.lean
    theorem: Erdos730.ObstructionMaps.PhiR_root_progression
    statement: >-
      Substitution along an R-branch prime-power root progression gives the
      exact common quadratic branch map with residual coefficient 258T.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ObstructionMaps.lean
    theorem: Erdos730.ObstructionMaps.PhiS_root_progression
    statement: >-
      Substitution along an S-branch prime-power root progression gives the
      exact common quadratic branch map with residual coefficient -258T.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ObstructionMaps.lean
    theorem: Erdos730.ObstructionMaps.prime_dvd_residual_support
    statement: >-
      Every prime divisor of the four residual linear coefficients belongs to
      the exact exceptional set 2, 3, 41, 43.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/HigherPowerCount.lean
    theorem: Erdos730.higherPrimePowerPairs_card_le
    statement: >-
      The finite number of prime-power pairs with exponent at least two and
      p to the a at most Z is bounded by the square-root row plus the exact
      cube-root and binary-logarithm rectangle.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ConsecutiveTransition.lean
    theorem: Erdos730.ConsecutiveTransition.consecutive_primeFactors_eq_iff_transitionConditions
    statement: >-
      For every positive n, equality of the prime-factor sets of the two
      consecutive central binomial coefficients is equivalent to the exact
      odd-prime drop and entry cofactor conditions.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/ConsecutiveTransition.lean
    theorem: Erdos730.ConsecutiveTransition.exists_obstruction_of_primeFactors_ne
    statement: >-
      If the two consecutive central binomial coefficients have different
      prime support, a fully quantified drop or entry obstruction witnesses
      the failure; this is the exact event-coverage implication Bad into E.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/DominatedLimit.lean
    theorem: Erdos730.tendsto_tsum_higherPower_of_dominated
    statement: >-
      Tannery dominated convergence applies to nonnegative higher-prime-power
      contributions bounded by the summable exact majorant 2 over p to the a
      for exponents a at least two.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/DominatedLimit.lean
    theorem: Erdos730.tendsto_higherPrimePowerPairs_card_div
    statement: >-
      The number of prime-power pairs with exponent at least two and value at
      most Z is sublinear in Z, closing the normalized terminal-pair count.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean
  - problem: 730
    source: erdosproblems
    file: ErdosProblems/Erdos730/FullDensityTheorem.lean
    theorem: Erdos730.FullDensityTheorem.pairSet_infinite
    statement: >-
      There are infinitely many pairs m less than n whose central binomial
      coefficients have identical prime-factor support; the proof gives
      infinitely many consecutive pairs from an explicit positive-density
      family.
    axioms_clean: true
    fc_target: FormalConjectures/ErdosProblems/730.lean