κ-improvement development, part 18: item-language primitives

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs17

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.KFU2Cover
/-!
# KFU2 §1: coverage of the `Φ`-addresses and whole-array denotations

Hypotheses (`RCRT` side): `1 ≤ s_j`, pairwise coprime `s_j` (`j < d`), `μ_j P_j ≡ 1 (mod s_j)`.

* `cover`: every valid `S_r`-address `b` is `phiAddr (kOf b) (b_d)` with `kOf b < P_d`
  (CRT via `RCRT.PhiEquiv`).
* `phiAddr_eq_Phi`: the first `d` coordinates of `phiAddr k c` are the `RCRT.Phi` residues of `k`.
* **`PhiD_eq`**: `PhiD xs` at padded address `b` is `xs[2·kOf b + b_d]` if `b` is a source
  address, `0` otherwise (`RCRT` `Φ` on whole arrays, zero padded).
* **`PhiInvD_eq`**: `(PhiInvD ys)[m] = ys[enc_{T_r} (phiAddr (m/2) (m%2))]` (`Φ⁻¹` on whole arrays).
* **`PhiInvD_PhiD`**: `Φ⁻¹ ∘ Φ = id`; **`PhiD_PhiInvD`**: `Φ ∘ Φ⁻¹ = id` on arrays vanishing on the padding.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KFU

open IntMul KFC AModel AModelL12

section Cover

variable {d : ℕ} {sF μ : ℕ → ℕ}

/-- The CRT hypotheses. -/
structure CrtOK (d : ℕ) (sF μ : ℕ → ℕ) : Prop where
  pos : ∀ j < d, 1 ≤ sF j
  cop : ∀ i j, i < d → j < d → i ≠ j → Nat.Coprime (sF i) (sF j)
  inv : ∀ j < d, ((μ j * OpenAI.RCRT.Ppre sF j : ℕ) : ZMod (sF j)) = 1

open Classical in
/-- The `k` whose `Φ`-address is `b` (`0` if none). -/
noncomputable def kOf (d : ℕ) (sF μ : ℕ → ℕ) (b : List ℕ) : ℕ :=
  if h : ∃ k < OpenAI.RCRT.Ppre sF d, (List.range d).map (fun j => μ j * k % sF j) = b.take d
  then Classical.choose h else 0

end Cover

end NLogN.KFU

end