OAI/Combinatorics/EditApproximation/Geometry/SourceRankedWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Source leaves add only their executed read count to each table body. Projecting them away preserves the table dependency program, so a uniform local source budget multiplies its uncached request bound.

  1. def OAI.EditApproximation.SourceRanked.projectedBody line 18
  2. theorem OAI.EditApproximation.SourceRanked.projectedBody_value line 22
  3. theorem OAI.EditApproximation.SourceRanked.projectedProgram_value line 28
  4. theorem OAI.EditApproximation.SourceRanked.uncachedCalls_le_source_factor line 34
  5. theorem OAI.EditApproximation.SourceRanked.memo_requests_le_source_factor line 109