OAI/Combinatorics/EditApproximation/Queries/QueryPhysicalScalarReads.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Concrete scalar-source adapters. Guards, finite source addresses and tag construction are executed before each read; rejected requests return the original zero value without exposing a random coordinate.

  1. theorem OAI.EditApproximation.queryPhysicalScalarRead_refines line 22
  2. theorem OAI.EditApproximation.queryGroup_transport line 33
  3. theorem OAI.EditApproximation.queryPhysicalScalarGroupRead_refines line 44
  4. theorem OAI.EditApproximation.queryPhysicalScalarOnlineRead_refines line 68