OAI/Combinatorics/EditApproximation/Binary/BitSourceRanked.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Source draws and table requests share the same concrete binary memo. Rank-zero sources are stored once; each tagged recursive request pays for its tag construction before entering the shared dictionary.

  1. theorem OAI.EditApproximation.SourceRanked.bitBody_refines line 18