OAI/Computability/MaxCut/Analysis/CubeEquiv.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.cubeEquiv line 12

   Source documentation

   Fixed binary radix indexing, rather than a chosen Fintype.equivFin.

   def cubeEquiv (q : ℕ) : Cube (Fin q) ≃ Fin (2 ^ q) :=
   …

2. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.vertexEquiv line 16

   Source documentation

   Row-major indexing before the explicit finite-field blowup.

   def vertexEquiv (n q : ℕ) : (Fin n × Cube (Fin q)) ≃ Fin (n * 2 ^ q) :=
   …

3. def OAI.OptimalMaxCut.LongCode.InstanceAdapter.output line 19
4. theorem OAI.OptimalMaxCut.LongCode.InstanceAdapter.output_vertex_bound line 23