/- # EssentialBits — the COMPOSED, ∀-(T,n) essentiality theorem, stated in BITS ## What this closes `IsolationBound.lean` proves two halves and never joins them: * `spec_forces_injective` (∀ types) — the zero-leak + full-reuse spec forces the state map injective — but it takes matrix extensionality `hmem` as a **HYPOTHESIS**; * `essential_state_count` (∀ T,n) — an injection out of `Fin (2^(T*n))` forces `2^(T*n) ≤ s` — but it takes `Function.Injective σ` as a **HYPOTHESIS**. The only discharge of `hmem` anywhere in the estate was `IsolationBound.mem4_ext`, a `by decide` over `Fin 4 × Fin 2`, i.e. **T·n = 2**; `StateClassBound.kv_needs_four_states` then elaborates `emb := id` only because `2^2` reduces definitionally to `4`. So the headline "tenant-safe KV pooling needs ≥ T·n bits" rested on a composition that existed at exactly one size, and nothing anywhere took a logarithm — every "bits" in this estate was docstring prose over a `2^k ≤ s`. This file supplies the three missing pieces and states the conclusion the headline claims: 1. `authMatrix_ext` — matrix extensionality **∀ T,n** (`funext`), replacing the `decide` at 2. 2. `denseWorld_injective` — `Fin (2^(T*n)) ↪ AuthMatrix T n`, built from `TTEInjectivityFloor.bitWorld_injective` (already ∀ n in this package) composed with the row/column uncurry `pairIdx`. 3. `kv_pool_state_floor` / `kv_pool_bits_floor` — the single composed theorem `spec ⇒ 2^(T*n) ≤ s ⇒ T*n ≤ log₂ s`, general T and n, plus the deployable byte form. and then does the same for the model that actually ships (single owner per block), together with the machine-checked statement of **when the dense floor binds**. ## Honest scope — read before citing * The floor is NECESSARY, not sufficient: it bounds state, not timing channels, not content channels, not probabilistic isolators. * **BOTH spec hypotheses are load-bearing and the foils stay.** Zero-leak ALONE is provably 0 bits — `IsolationBound.deny_all_starves` exhibits a stateless deny-all policy that never leaks, costs nothing, and STARVES. Full-reuse alone is 0 bits by `serve_all_leaks`. * **T·n is the DENSE model.** It binds exactly when a block may be authorized to an arbitrary SUBSET of tenants (group / shared-read ACLs). Under single-owner rights the tight floor is `T^n` states = `n·log₂T` bits, exponentially smaller, and that bound is composed here too. `single_owner_below_dense_strict` + `single_owner_store_cannot_serve_dense` make the separation and its consequence theorems rather than prose. * The pigeonhole is classical. What is mechanized here is the COMPOSITION and the BIT-COUNT, not new mathematics. `le_log2_of_pow_le` is MIRRORED locally (~6 lines) from `theory/lean/PriorArtCost.lean:75` — a different Lake package, and cross-package `require` is forbidden in this estate. It uses only `Nat.log2_lt` from Lean 4 core. No mathlib. No `native_decide`. No `sorry`. No custom `axiom`. Axioms ⊆ {propext, Quot.sound}. ADDITIVE lib: own line, NOT in defaultTargets, NEVER summed into the serving-limits count or any other corpus. Imports IsolationBound / StructuredIsolation / TTEInjectivityFloor / InjectivityFloor (all same package). -/ import IsolationBound import StructuredIsolation import TTEInjectivityFloor import InjectivityFloor namespace EssentialBits /-! ## § 0 — the log₂ step (mirrored from PriorArtCost; core-only) -/ /-- `2^k ≤ x → k ≤ log₂ x`. Mirrored from `theory/lean/PriorArtCost.lean:75` (cross-package `require` is forbidden here). Uses only `Nat.log2_lt` from Lean 4 core. -/ theorem le_log2_of_pow_le {k x : Nat} (hx : x ≠ 0) (h : 2 ^ k ≤ x) : k ≤ Nat.log2 x := by apply Nat.le_of_not_lt intro h1 have h2 : x < 2 ^ k := (Nat.log2_lt hx).mp h1 omega /-! ## § 1 — the authorization world, ∀ T,n -/ /-- **The dense authorization matrix.** Row = tenant, column = a pooled KV-cache block. `M t i = true` means tenant `t` is authorized to be served pooled block `i`. Every one of the `T*n` rights is independent — this is the DENSE model, and its size is what the `T·n` headline counts. -/ abbrev AuthMatrix (T n : Nat) := Fin T → Fin n → Bool /-- A fetch: which tenant is asking for which pooled block. -/ abbrev Cell (T n : Nat) := Fin T × Fin n /-- Membership of the authorization matrix at a fetch — the observable the spec pins. -/ def memA {T n : Nat} (M : AuthMatrix T n) (c : Cell T n) : Bool := M c.1 c.2 /-- **MATRIX EXTENSIONALITY, ∀ T,n.** A matrix IS its cell membership. This is the hypothesis `IsolationBound.spec_forces_injective` takes and that `mem4_ext` previously discharged only at `Fin 4 × Fin 2` (T·n = 2). Here it is `funext`, for every T and n. -/ theorem authMatrix_ext {T n : Nat} : ∀ A B : AuthMatrix T n, (∀ c, memA A c = memA B c) → A = B := by intro A B h funext t i exact h (t, i) /-! ## § 2 — the missing bridge: `Fin (2^(T*n)) ↪ AuthMatrix T n`, ∀ T,n -/ /-- Row-major index of cell `(t, i)` in a `T×n` grid. -/ def pairIdx {T n : Nat} (t : Fin T) (i : Fin n) : Fin (T * n) := ⟨t.val * n + i.val, by have hi : i.val < n := i.isLt have ht : t.val + 1 ≤ T := t.isLt have h1 : (t.val + 1) * n ≤ T * n := Nat.mul_le_mul_right _ ht have h2 : (t.val + 1) * n = t.val * n + n := by simp [Nat.succ_mul] omega⟩ /-- Reshape a flat `T*n`-bit word into a `T×n` matrix. -/ def uncurryGrid {T n : Nat} (f : Fin (T * n) → Bool) : AuthMatrix T n := fun t i => f (pairIdx t i) /-- **THE RESHAPE IS INJECTIVE.** Every flat index `j < T*n` is `pairIdx ⟨j/n⟩ ⟨j%n⟩`, so two words that agree on every cell of the grid agree everywhere. (When `n = 0` the domain `Fin 0` is empty and the statement is vacuous, which `omega` discharges through `Fin.elim0`'s absurdity.) -/ theorem uncurryGrid_injective (T n : Nat) : Function.Injective (uncurryGrid (T := T) (n := n)) := by intro f g h funext j have hn : 0 < n := by rcases Nat.eq_zero_or_pos n with hz | hp · exact absurd j.isLt (by simp [hz]) · exact hp have hjlt : j.val < T * n := j.isLt -- NOT `Nat.lt_of_mul_lt_mul_right`: that core lemma carries `Classical.choice`, and this -- corpus's axiom gate admits only {propext, Quot.sound}. Decidable case split instead. have hq : j.val / n < T := by rcases Nat.lt_or_ge (j.val / n) T with h | h · exact h · exfalso have h1 : T * n ≤ (j.val / n) * n := Nat.mul_le_mul_right _ h have h2 : (j.val / n) * n ≤ j.val := Nat.div_mul_le_self j.val n omega have hr : j.val % n < n := Nat.mod_lt _ hn have hidx : pairIdx (T := T) (n := n) ⟨j.val / n, hq⟩ ⟨j.val % n, hr⟩ = j := by apply Fin.ext show (j.val / n) * n + j.val % n = j.val have hdm := Nat.div_add_mod j.val n have hc : (j.val / n) * n = n * (j.val / n) := Nat.mul_comm _ _ omega have := congrFun (congrFun h ⟨j.val / n, hq⟩) ⟨j.val % n, hr⟩ simpa [uncurryGrid, hidx] using this /-- **THE BRIDGE.** The `2^(T*n)` packed words give `2^(T*n)` genuinely distinct authorization matrices, for EVERY T and n. `bitWorld_injective` is `TTEInjectivityFloor`'s ∀-n bit decode (`Nat.eq_of_testBit_eq` + `Nat.testBit_lt_two_pow`, Lean core); the reshape is § 2 above. This is precisely the embedding `InjectivityFloor.state_floor` asks its caller to supply and that no caller in this estate had ever supplied beyond T·n = 2. -/ def denseWorld (T n : Nat) : Fin (2 ^ (T * n)) → AuthMatrix T n := fun m => uncurryGrid (TTEInjectivityFloor.bitWorld (T * n) m) theorem denseWorld_injective (T n : Nat) : Function.Injective (denseWorld T n) := (uncurryGrid_injective T n).comp (TTEInjectivityFloor.bitWorld_injective (T * n)) /-! ## § 3 — THE COMPOSED THEOREM: spec ⇒ 2^(T*n) ≤ s ⇒ T*n bits, ∀ T,n -/ /-- **THE ESSENTIALITY THEOREM, COMPOSED AND GENERAL.** Hypothesis: a deterministic pooled-KV policy that summarizes the authorization matrix into a state (`σ`) and answers every fetch from that state alone (`ans`), and that is simultaneously ZERO-LEAK and FULL-REUSE — both directions of `ans (σ M) c = memA M c`. Conclusion: it carries at least `2^(T*n)` states, for EVERY T and n. Nothing is assumed about the representation: `authMatrix_ext` and `denseWorld_injective` are proved above rather than hypothesised, so this statement has no side conditions left. -/ theorem kv_pool_state_floor (T n s : Nat) (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool) (hspec : ∀ M c, ans (σ M) c = memA M c) : 2 ^ (T * n) ≤ s := by have hinj : Function.Injective σ := fun A B hAB => IsolationBound.spec_forces_injective memA σ ans authMatrix_ext hspec A B hAB exact IsolationBound.essential_state_count T n s (σ ∘ denseWorld T n) (hinj.comp (denseWorld_injective T n)) /-- The state space is nonempty: a spec-satisfying policy over `Fin s` maps a matrix into it, so `s ≠ 0`. Needed to take a logarithm. -/ theorem kv_pool_states_pos (T n s : Nat) (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool) (_hspec : ∀ M c, ans (σ M) c = memA M c) : s ≠ 0 := by intro h0 have := (σ (fun _ _ => false)).isLt omega /-- **THE BIT COUNT — the headline sentence, as a Lean statement.** A zero-leak + full-reuse pooled-KV policy over `T` tenants and `n` pooled blocks needs at least `T*n` BITS to index its states: `T*n ≤ ⌊log₂ s⌋`. Until now every "T·n bits" in this estate was prose over a `2^k ≤ s`; this is the logarithm, mathlib-free, ∀ T,n. -/ theorem kv_pool_bits_floor (T n s : Nat) (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool) (hspec : ∀ M c, ans (σ M) c = memA M c) : T * n ≤ Nat.log2 s := le_log2_of_pow_le (kv_pool_states_pos T n s σ ans hspec) (kv_pool_state_floor T n s σ ans hspec) /-- **THE DEPLOYABLE FORM.** `T*n` bits held as `⌈T*n/8⌉` bytes: the authorization store cannot be provisioned smaller. Stated as the ceiling-division identity a sizing gate would compute. -/ theorem kv_pool_bytes_floor (T n s : Nat) (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool) (hspec : ∀ M c, ans (σ M) c = memA M c) : (T * n + 7) / 8 ≤ (Nat.log2 s + 7) / 8 := Nat.div_le_div_right (Nat.add_le_add_right (kv_pool_bits_floor T n s σ ans hspec) 7) /-- **THE IMPOSSIBILITY.** Below the floor no policy is correct — the ∀-(T,n) generalization of `no_three_state_policy`, which was a `decide` at T=1, n=2. -/ theorem no_policy_below_floor (T n s : Nat) (hs : s < 2 ^ (T * n)) (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool) : ¬ (∀ M c, ans (σ M) c = memA M c) := by intro hspec exact absurd (kv_pool_state_floor T n s σ ans hspec) (by omega) /-! ### Non-vacuity — the spec IS satisfiable, and exactly at the floor Without this every impossibility above would be uninformative: a spec nothing satisfies makes "no implementation below the floor" trivially true. -/ /-- **TIGHTNESS, construction-tied.** The tag-table policy — state := the matrix itself, answer := membership — satisfies the spec, ∀ T,n. Unlike the `⟨id, injective_id⟩` attainment form this estate's own `InjectivityFloor.identity_attainment_mentions_no_spec` calls out as vacuous, this one MENTIONS THE SPEC and discharges it. -/ theorem tag_table_attains (T n : Nat) : ∀ (M : AuthMatrix T n) (c : Cell T n), memA (id M) c = memA M c := by intro M c; rfl /-- **THE Θ.** The floor is necessary AND attained — both conjuncts mention the spec. -/ theorem kv_pool_theta (T n s : Nat) : (∀ (σ : AuthMatrix T n → Fin s) (ans : Fin s → Cell T n → Bool), (∀ M c, ans (σ M) c = memA M c) → 2 ^ (T * n) ≤ s) ∧ (∀ (M : AuthMatrix T n) (c : Cell T n), memA (id M) c = memA M c) := ⟨fun σ ans h => kv_pool_state_floor T n s σ ans h, tag_table_attains T n⟩ /-! ## § 4 — THE KV-CACHE INSTANTIATION, named Nothing in `IsolationBound.lean` mentions a KV cache. The model below is the one the measured work in this estate exercises: a paged prefix cache (vLLM-style APC) holding `n` blocks that may be served across `T` tenants, where the engine's per-fetch decision is a function of its stored authorization state and the fetch alone. -/ /-- The KV-cache pooling world: `T` tenants × `n` pooled prefix blocks in a shared paged cache. `KVAuth T n t b = true` means tenant `t` may be served pooled block `b`. -/ abbrev KVAuth (T n : Nat) := AuthMatrix T n /-- A KV fetch: tenant `t` asking for pooled prefix block `b`. -/ abbrev KVFetch (T n : Nat) := Cell T n /-- **THE KV-CACHE AUTHORIZATION-STATE FLOOR, IN BITS.** Any cross-tenant KV-cache pool that never serves an unauthorized block (zero leak) and always serves an authorized cached block (full reuse), and whose serve/deny decision is a function of its stored state and the fetch, must hold at least `T*n` bits of authorization state for `T` tenants over `n` pooled blocks. This is the statement the estate's headline makes. It is now one theorem, general in T and n, in bits. WHAT IT DOES NOT SAY (both foils preserved in `IsolationBound.lean`): zero leak ALONE is 0 bits (`deny_all_starves` — deny everything, never leak, starve); full reuse ALONE is 0 bits (`serve_all_leaks`). And it is the DENSE rights model — see § 5. -/ theorem kv_cache_pool_bits_floor (T n s : Nat) (state : KVAuth T n → Fin s) (serve : Fin s → KVFetch T n → Bool) (hspec : ∀ (A : KVAuth T n) (f : KVFetch T n), serve (state A) f = memA A f) : T * n ≤ Nat.log2 s := kv_pool_bits_floor T n s state serve hspec /-- A concrete deployment witness: 64 tenants over 1024 pooled blocks forces 65,536 bits = 8,192 bytes of authorization state. Arithmetic only — the theorem above supplies the content. -/ theorem kv_cache_witness_64x1024 : 64 * 1024 = 65536 ∧ (64 * 1024 + 7) / 8 = 8192 := by decide /-! ## § 5 — THE SHIPPING MODEL, and exactly when the dense floor binds The dense model gives every (tenant, block) right independently: `2^(T*n)` worlds. A deployment that gives each block EXACTLY ONE owner has only `T^n` worlds. `StructuredIsolation` proves both halves of that model separately and — like `IsolationBound` — never composes them: its `structured_forces_injective` is over `Fin n → Fin T` while `structured_state_floor` is over `Fin (T^n)`, with no bridge. § 5 supplies the bridge and the composition, so the model that actually ships carries a proved floor too, and then states the separation as a theorem. -/ /-- Single-owner rights: each of `n` pooled blocks has exactly one owning tenant. -/ abbrev OwnerMap (T n : Nat) := Fin n → Fin T /-- Base-`T` digit decode: the `i`-th digit of a packed index below `T^n`. -/ def digitWorld (T n : Nat) (hT : 0 < T) (m : Fin (T ^ n)) : OwnerMap T n := fun i => ⟨m.val / T ^ i.val % T, Nat.mod_lt _ hT⟩ /-- Uniqueness of base-`T` representation, mathlib-free: two naturals below `T^n` agreeing on every digit `i < n` are equal. Induction on `n`; the step peels digit 0 via `Nat.div_add_mod`. (No `0 < T` needed: at `T = 0` the hypothesis `a < 0 ^ n` is vacuous for `n ≥ 1` and forces `a = b = 0` at `n = 0`. `digitWorld` still needs `0 < T` — for the `Fin T` bound, not for this.) -/ theorem base_digits_unique (T : Nat) : ∀ (n a b : Nat), a < T ^ n → b < T ^ n → (∀ i, i < n → a / T ^ i % T = b / T ^ i % T) → a = b := by intro n induction n with | zero => intro a b ha hb _; simp at ha hb; omega | succ n ih => intro a b ha hb h have h0 : a % T = b % T := by simpa using h 0 (Nat.zero_lt_succ n) -- NOT `Nat.div_lt_of_lt_mul`: that core lemma carries `Classical.choice`. have shrink : ∀ x : Nat, x < T ^ (n + 1) → x / T < T ^ n := by intro x hx rcases Nat.lt_or_ge (x / T) (T ^ n) with h | h · exact h · exfalso have h1 : T ^ n * T ≤ (x / T) * T := Nat.mul_le_mul_right _ h have h2 : (x / T) * T ≤ x := Nat.div_mul_le_self x T have h3 : x < T ^ n * T := by simpa [Nat.pow_succ] using hx omega have hdiv : a / T = b / T := by apply ih · exact shrink a ha · exact shrink b hb · intro i hi have := h (i + 1) (Nat.succ_lt_succ hi) simpa [Nat.pow_succ, Nat.mul_comm, Nat.div_div_eq_div_mul] using this have ea := Nat.div_add_mod a T have eb := Nat.div_add_mod b T rw [hdiv, h0] at ea omega theorem digitWorld_injective (T n : Nat) (hT : 0 < T) : Function.Injective (digitWorld T n hT) := by intro a b h apply Fin.ext apply base_digits_unique T n a.val b.val a.isLt b.isLt intro i hi have := congrArg Fin.val (congrFun h ⟨i, hi⟩) simpa [digitWorld] using this /-- **THE SINGLE-OWNER FLOOR, COMPOSED.** A pool that reads back each block's owning tenant — the minimum a correct single-owner pool must do, since it cannot serve a block to its owner without knowing the owner — needs at least `T^n` states, for every `T ≥ 1` and every `n`. -/ theorem single_owner_state_floor (T n s : Nat) (hT : 0 < T) (rep : OwnerMap T n → Fin s) (owner : Fin s → Fin n → Fin T) (hspec : ∀ (o : OwnerMap T n) (i : Fin n), owner (rep o) i = o i) : T ^ n ≤ s := by have hinj : Function.Injective rep := fun o1 o2 hr => StructuredIsolation.structured_forces_injective rep owner hspec o1 o2 hr exact StructuredIsolation.structured_state_floor T n s (rep ∘ digitWorld T n hT) (hinj.comp (digitWorld_injective T n hT)) /-- **THE SINGLE-OWNER BIT COUNT.** With `T = 2^b` tenants the floor is exactly `n·b = n·log₂T` bits — the number `README.md` states in prose, now a theorem. -/ theorem single_owner_bits_floor (b n s : Nat) (rep : OwnerMap (2 ^ b) n → Fin s) (owner : Fin s → Fin n → Fin (2 ^ b)) (hspec : ∀ (o : OwnerMap (2 ^ b) n) (i : Fin n), owner (rep o) i = o i) : n * b ≤ Nat.log2 s := by have hT : 0 < 2 ^ b := Nat.two_pow_pos b have hfloor : (2 ^ b) ^ n ≤ s := single_owner_state_floor (2 ^ b) n s hT rep owner hspec have hpow : 2 ^ (n * b) ≤ s := by have : (2 ^ b) ^ n = 2 ^ (n * b) := by rw [← Nat.pow_mul, Nat.mul_comm] omega have hs : s ≠ 0 := by intro h0 have := (rep (fun _ => ⟨0, hT⟩)).isLt omega exact le_log2_of_pow_le hs hpow /-! ### WHEN THE DENSE FLOOR BINDS — the separation, machine-checked `StructuredIsolation.structured_below_dense` proves `T^n ≤ 2^(T*n)` (non-strict). The operative question is not whether the single-owner floor is smaller but whether a store PROVISIONED for it can serve the dense spec. It cannot, and that is the precise statement of when `T·n` bites. -/ /-- The separation is STRICT for every `T` and every `n ≥ 1`: a single-owner store is strictly smaller than the dense floor, so it cannot be sized for both. (An earlier draft carried `2 ≤ T ∧ 2 ≤ n`; the proof never used them, so they were decoration and are removed rather than left in to make the statement look guarded. The interesting regime is still `T, n ≥ 2` — see `separation_witness_4x4` — but the theorem does not need it.) -/ theorem single_owner_below_dense_strict (T n : Nat) (hn : 0 < n) : T ^ n < 2 ^ (T * n) := by have hstep : T ^ n < (2 ^ T) ^ n := Nat.pow_lt_pow_left (Nat.lt_two_pow_self (n := T)) (by omega) calc T ^ n < (2 ^ T) ^ n := hstep _ = 2 ^ (T * n) := (Nat.pow_mul 2 T n).symm /-- **THE ANSWER TO "WHEN DOES THE T·n FLOOR BITE".** A pool whose authorization store is provisioned for the single-owner model (`T^n` states) provably CANNOT satisfy the dense zero-leak + full-reuse spec, for every `T` and every `n ≥ 1`. So the dense `T·n`-bit floor is not an alternative accounting of the same deployment — it is the floor of a STRICTLY MORE PERMISSIVE one, and a design that ships single-owner rights has not escaped it, it has declined to offer what it bounds. The dense model is the one where a block may be authorized to an arbitrary SUBSET of tenants (group / shared-read ACLs); the single-owner model is the one where it may not. -/ theorem single_owner_store_cannot_serve_dense (T n : Nat) (hn : 0 < n) (σ : AuthMatrix T n → Fin (T ^ n)) (ans : Fin (T ^ n) → Cell T n → Bool) : ¬ (∀ M c, ans (σ M) c = memA M c) := no_policy_below_floor T n (T ^ n) (single_owner_below_dense_strict T n hn) σ ans /-- Concrete witness of the gap at T=4, n=4: the single-owner store holds 256 states (8 bits), the dense floor is 2^16 = 65,536 states (16 bits) — a factor of 256 in states, 2× in bits. -/ theorem separation_witness_4x4 : (4 : Nat) ^ 4 = 256 ∧ 2 ^ (4 * 4) = 65536 ∧ (4 : Nat) ^ 4 < 2 ^ (4 * 4) := by decide /-! ## § 6 — the foils are still load-bearing, restated at this file's surface These re-export `IsolationBound`'s foils so a reader of the composed theorem cannot miss the two hypotheses without which the whole bound is 0 bits. They are NOT weakened here. -/ /-- ZERO-LEAK ALONE IS 0 BITS. The stateless deny-all policy never leaks and holds no state — and starves, forfeiting pooling entirely. Any citation of the `T·n` floor that drops "full reuse" is citing a bound this foil refutes. -/ theorem zero_leak_alone_is_free : IsolationBound.mem4 3 0 = true ∧ (fun (_ : Fin 2) => false) 0 = false := IsolationBound.deny_all_starves /-- FULL-REUSE ALONE IS 0 BITS. The stateless serve-all policy reuses everything and holds no state — and leaks. -/ theorem full_reuse_alone_is_free : IsolationBound.mem4 0 0 = false ∧ (fun (_ : Fin 2) => true) 0 = true := IsolationBound.serve_all_leaks end EssentialBits