Packed integer vertex table (GENERATED) #
GENERATED by scripts/gen_python_nat.lean — do not edit.
The 90×3 scale-10¹⁶ vertex coordinates of pythonVertexNum, packed
into one Nat literal: flat vertex j = 45ℓ + 15i + k occupies bits
[171j, 171(j+1)), coordinate c the 57-bit field at offset 57c,
offset-encoded as coord + 2^56 (so all fields are nonnegative and
< 2^57). Under decide +kernel a vertex access is one accelerated
shift + mask; pythonVertexBig_spec (proved by the kernel itself)
certifies every field against pythonVertexNum, in exactly the
let-shape the fast checkers use.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Noperthedron.pythonVertexBig_spec
(j : Fin 90)
:
have v := pythonVertexBig >>> (171 * ↑j) &&& 2 ^ 171 - 1;
↑(v &&& 2 ^ 57 - 1) = pythonVertexNum (VertexIndex.ofFin90 j) 0 + 2 ^ 56 ∧ ↑(v >>> 57 &&& 2 ^ 57 - 1) = pythonVertexNum (VertexIndex.ofFin90 j) 1 + 2 ^ 56 ∧ ↑(v >>> 114) = pythonVertexNum (VertexIndex.ofFin90 j) 2 + 2 ^ 56