pith. machine review for the scientific record. sign in
theorem proved tactic proof

box_phase_hit_gives_balanced_pair

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  57theorem box_phase_hit_gives_balanced_pair {n c : ℕ}
  58    (h : HitsBalancedPhase n c) :
  59    BalancedPairPhaseSupport n c := by

proof body

Tactic-mode proof.

  60  rcases h with ⟨x, N, box, hn, hc, hx, hNpos, hN, hcdef, hdvd, hevd⟩
  61  refine ⟨x, N, boxDivisor box, boxComplement box,
  62    hn, hc, hx, hNpos, box.d_pos, box.e_pos, hN, hcdef, ?_, hdvd, hevd⟩
  63  exact box_divisor_mul_complement box
  64
  65/-- A box phase hit already gives a rational Erdős-Straus representation,
  66by composing the finite closure lemma with the RCL ledger theorem. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.