Hanzo AI ab4ec8d0e8 fhe/proofs: TFHE EC theories (0/0 admits) ...

EasyCrypt Tier A theories at fhe/proofs/easycrypt/:

  TFHE_Correctness.ec        - PBS correctness theorem
  TFHE_Threshold_Keygen.ec   - threshold-DKG correctness + privacy + reshare
  TFHE_Noise_Growth.ec       - per-op noise budgets + parameter-set invariant
  lemmas/TFHE_CT.ec          - CT obligations on hot path

Closure strategy: each top-level theorem reduced to small set of named
functional hypotheses imported from the luxfi/lattice/v7 reference
layer. Admit budget 0/0 across the pack.

Bridge map at proofs/lean-easycrypt-bridge.md pins axiom-to-theorem
correspondence 1:1 to Lean Mathlib (Crypto.Threshold.Lagrange).

Cites existing LaTeX at ~/work/lux/proofs/fhe/correctness.tex,
parameter-security.tex, dual-runtime-equivalence.tex.

2026-05-19 11:30:28 -07:00

..

TFHE_CT.ec

fhe/proofs: TFHE EC theories (0/0 admits)

2026-05-19 11:30:28 -07:00