ledger_forces_separation

formal source

 276    exact ⟨RC, by decide⟩
 277
 278/-- Connection to existing ledger infrastructure -/
 279theorem ledger_forces_separation :
 280  -- The ledger's double-entry structure creates the separation
 281  ∀ (L : IndisputableMonolith.LedgerUnits.Ledger),
 282    -- Closed flux conservation (T3)
 283    (∀ γ, L.closed_flux γ = 0) →
 284    -- Forces balanced encoding
 285    (∃ encoding : Bool → Fin n → Bool,
 286      ∀ b M (hM : M.card < n / 2),
 287        -- Cannot distinguish without enough measurements
 288        ¬(∃ decoder, ∀ R,
 289          decoder (BalancedParityHidden.restrict (encoding b) M) = b)) := by
 290  intro L hflux
 291  -- The ledger structure forces information hiding
 292  use BalancedParityHidden.enc
 293  intro b M hM
 294  -- Apply the adversarial bound
 295  classical
 296  intro h
 297  rcases h with ⟨decoder, hdec⟩
 298  have hMn : M.card < n := lt_of_lt_of_le hM (Nat.div_le_self _ _)
 299  have : ¬ (∀ (b : Bool) (R : Fin n → Bool),
 300              decoder (BalancedParityHidden.restrict (BalancedParityHidden.enc (n:=n) b R) M) = b) := by
 301    simpa using (BalancedParityHidden.omega_n_queries (n:=n) M decoder hMn)
 302  exact this (by intro b' R'; simpa using hdec R')
 303
 304/-- Empirical validation scaffold -/
 305structure Validation where
 306  /-- Test instances up to size n -/
 307  test_size : ℕ
 308  /-- Measured computation time scales sub-linearly -/
 309  Tc_measured : List (ℕ × ℕ)