OAI/Combinatorics/EditApproximation/Queries/QueryFamilyNormalize.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The complete mixed memo is normalized on the physical table grid. Its actual ranked binary values and adaptive reference trace agree on every coarse seed and every finite scalar draw.

  1. theorem OAI.EditApproximation.familyBase_pos line 12
  2. theorem OAI.EditApproximation.queryFamilyMemoNormalized_correct line 50
  3. theorem OAI.EditApproximation.queryFamilyMemoNormalized_width line 89
  4. theorem OAI.EditApproximation.queryFamilyMemoNormalized_decode line 128
  5. theorem OAI.EditApproximation.queryFamilyMemoNormalized_work_transfer line 145