OAI/Combinatorics/UniformKServer/ActualPublicFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Law-dependent but genuinely online configuration/action flows for the actual pilot, partition, allocation, anchor, and rounding construction.

  1. def OAI.UniformKServer.HiddenFlow.Data.transcript line 17
  2. theorem OAI.UniformKServer.HiddenFlow.Data.transcript_zero line 20
  3. theorem OAI.UniformKServer.HiddenFlow.Data.transcript_snoc line 22
  4. theorem OAI.UniformKServer.HiddenFlow.Data.transcript_length line 26
  5. def OAI.UniformKServer.HiddenFlow.Data.Public line 29
  6. def OAI.UniformKServer.PartitionTree.publicInput line 40
  7. def OAI.UniformKServer.PartitionTree.componentFlow line 51
  8. theorem OAI.UniformKServer.PartitionTree.component_valid line 56
  9. theorem OAI.UniformKServer.PartitionTree.component_bound line 62