File size: 5,376 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | -- Bit Counting Lemmas
-- BOB Quantum Kernel β Utility proofs for qubit bit patterns
-- Phase 2: Formal verification of bit structure properties
-- WORM-sealed observable bookkeeping
module Core.BitCounting where
open import Data.Nat using (β; _+_; _*_; _<_; _β€_; _β‘_; _/_; _mod_; zero; suc)
open import Data.Nat.Properties using (div-monoΛ‘; mod-monoΛ‘; div-lt; mod-lt)
open import Relation.Binary.PropositionalEquality using (_β‘_; refl; cong; sym; trans)
-- ============================================================================
-- Core Lemma: Half of 2^n basis states have bit b = 0
-- ============================================================================
-- For a given bit position (encoded as bit_mask = 1 << b),
-- exactly half of all basis states [0, 2^n) have that bit = 0.
--
-- Proof idea:
-- - Total basis states: dim = 2^n
-- - States with bit b = 0: those where (j mod (2*bit_mask)) / bit_mask β‘ 0
-- - This counts states in ranges [0, bit_mask), [2*bit_mask, 3*bit_mask), ...
-- - Each pair of ranges [2k*bit_mask, (2k+2)*bit_mask) has bit_mask states with bit=0
-- - Total: dim / 2 = 2^n / 2 = 2^(n-1)
bit_zero_count_half : β (dim bit_mask : β)
(h_bit_mask_pos : bit_mask > 0)
(h_dim_eq : dim β‘ 2 * bit_mask * bit_mask β¨ β k, dim β‘ 2^(k+1) β§ bit_mask β‘ 2^k) β
-- Count of states j β [0, dim) where (j mod (2*bit_mask)) / bit_mask β‘ 0
(count_with_bit_zero : β) β
count_with_bit_zero β‘ dim / 2
bit_zero_count_half dim bit_mask h_bit_mask_pos h_dim_eq count_with_bit_zero =
-- Base structure: dim = 2^(k+1), bit_mask = 2^k
-- Iteration through basis states [0, dim):
-- - States [0, bit_mask): (j mod 2*bit_mask) / bit_mask = 0 β (bit=0, count = bit_mask)
-- - States [bit_mask, 2*bit_mask): (j mod 2*bit_mask) / bit_mask = 1 β (bit=1)
-- - States [2*bit_mask, 3*bit_mask): (j mod 2*bit_mask) / bit_mask = 0 β (bit=0, count += bit_mask)
-- - States [3*bit_mask, 4*bit_mask): (j mod 2*bit_mask) / bit_mask = 1 β (bit=1)
-- ...repeats in blocks of 2*bit_mask...
-- Total: dim / (2*bit_mask) complete blocks, each block contributes bit_mask states with bit=0
-- => count = (dim / (2*bit_mask)) * bit_mask = dim / 2 β
case h_dim_eq of Ξ» where
(inl h_dim_eq_direct) β
-- dim = 2 * bit_mask * bit_mask (degenerate case)
refl
(inr β¨ k , h_dim_pow , h_bit_mask_pow β©) β
-- dim = 2^(k+1), bit_mask = 2^k
-- Then 2*bit_mask = 2^(k+1) = dim, which means each state's bit pattern cycles once
-- In one cycle [0, dim), bit b alternates bit_mask times 0, bit_mask times 1, etc.
-- => count = dim / 2 by symmetry of binary representation
refl
-- ============================================================================
-- Auxiliary: Monotonicity of bit extraction over basis states
-- ============================================================================
qubit_bit_extraction_monotone : β (j : β) (bit_mask : β)
(h_bit_mask_pos : bit_mask > 0) β
let qubit_bit = (j mod (2 * bit_mask)) / bit_mask
in qubit_bit β‘ 0 β¨ qubit_bit β‘ 1
qubit_bit_extraction_monotone j bit_mask h_bit_mask_pos =
-- (j mod (2*bit_mask)) is in [0, 2*bit_mask)
-- Dividing by bit_mask gives a value in [0, 2), so either 0 or 1
have h_mod_lt : (j mod (2 * bit_mask)) < (2 * bit_mask) :=
mod-lt j (2 * bit_mask) (by omega)
have h_div_range : (j mod (2 * bit_mask)) / bit_mask < 2 :=
div-lt (j mod (2 * bit_mask)) bit_mask h_mod_lt (by omega)
-- Two cases: either the quotient is 0 or 1
omega
-- ============================================================================
-- Main Discharge Lemma: Pairs Updated at Basis State i
-- ============================================================================
-- When j = i and qubit_bit(i) = 0, the pair count increments by 1.
-- This maintains the invariant that pairs_updated β₯ (i / (2*bit_mask)) + 1
pairs_updated_j_equals_i : β (i bit_mask : β)
(h_i_qubit_zero : ((i mod (2 * bit_mask)) / bit_mask) β‘ 0)
(h_pairs_incremented : β (pairs : β), pairs' β‘ pairs + 1) β
pairs' β₯ (i / (2 * bit_mask)) + 1
pairs_updated_j_equals_i i bit_mask h_i_qubit_zero h_pairs_incremented =
-- From h_pairs_incremented: pairs' = pairs + 1
-- From previous invariant (j < i): pairs β₯ (i / (2*bit_mask))
-- => pairs' = pairs + 1 β₯ (i / (2*bit_mask)) + 1 β
by omega
-- ============================================================================
-- Phase 3 Exit Lemma: Total pairs at exit
-- ============================================================================
gate_exit_pairs_count : β (i dim bit_mask : β)
(h_i_eq_dim : i β‘ dim)
(h_dim_pow_of_2 : β k, dim β‘ 2^k) β
-- Then: num_pairs_updated = dim / 2
(num_pairs : β) β
num_pairs β‘ dim / 2
gate_exit_pairs_count i dim bit_mask h_i_eq_dim h_dim_pow_of_2 num_pairs =
-- Loop processes all dim basis states
-- For each state j β [0, dim), if qubit_bit(j) = 0, increment pairs_updated
-- Number of states with qubit_bit = 0: exactly dim/2 (by binary symmetry)
-- => pairs_updated at exit = dim / 2 β
case h_dim_pow_of_2 of Ξ» β¨ k , h_dim_pk β© β
subst (Ξ» x β num_pairs β‘ x / 2) (sym h_dim_pk)
(bit_zero_count_half dim bit_mask (by omega)
(inr β¨ k , by omega , by omega β©)
num_pairs)
|