IndisputableMonolith.Cryptography.BalancedJSubsetSum

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# 8-Balanced J-Subset Sum
   7
   8This module defines the first RS-native cryptography candidate in a deliberately
   9boring form. It makes no security claim.
  10
  11An instance has integer weights, residues in `ZMod 8`, phi-rungs, a target, and
  12a J-cost bound. A witness is a finite subset satisfying the target equation,
  138-neutrality, and the cost bound.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Cryptography
  18namespace BalancedJSubsetSum
  19
  20open Constants
  21
  22noncomputable section
  23
  24/-- Phi-rung value, represented by `exp(k log phi)` to avoid integer-power API
  25details in the first definition module. -/
  26def rungValue (k : ℤ) : ℝ := Real.exp ((k : ℝ) * Real.log phi)
  27
  28theorem rungValue_pos (k : ℤ) : 0 < rungValue k := by
  29  unfold rungValue
  30  exact Real.exp_pos _
  31
  32@[simp] theorem rungValue_zero : rungValue 0 = 1 := by
  33  unfold rungValue
  34  norm_num
  35
  36/-- One finite 8-Balanced J-Subset Sum instance. -/
  37structure BJSSInstance where
  38  n : ℕ
  39  weight : Fin n → ℤ
  40  residue : Fin n → ZMod 8
  41  rung : Fin n → ℤ
  42  target : ℤ
  43  bound : ℝ
  44
  45/-- A candidate witness is just a selected support. -/
  46structure BJSSWitness (inst : BJSSInstance) where
  47  support : Finset (Fin inst.n)
  48
  49/-- Integer target sum. -/
  50def weightSum (inst : BJSSInstance) (w : BJSSWitness inst) : ℤ :=
  51  ∑ i ∈ w.support, inst.weight i
  52
  53/-- Mod-8 residue sum. -/
  54def residueSum (inst : BJSSInstance) (w : BJSSWitness inst) : ZMod 8 :=
  55  ∑ i ∈ w.support, inst.residue i
  56
  57/-- J-cost contribution of a selected item. -/
  58def rungCost (inst : BJSSInstance) (i : Fin inst.n) : ℝ :=
  59  Cost.Jcost (rungValue (inst.rung i))
  60
  61/-- Total J-cost of a witness support. -/
  62def totalJCost (inst : BJSSInstance) (w : BJSSWitness inst) : ℝ :=
  63  ∑ i ∈ w.support, rungCost inst i
  64
  65def weightTarget (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  66  weightSum inst w = inst.target
  67
  68def residueNeutral (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  69  residueSum inst w = 0
  70
  71def jCostBound (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  72  totalJCost inst w ≤ inst.bound
  73
  74/-- Full solution predicate for the finite BJSS problem. -/
  75def isSolution (inst : BJSSInstance) (w : BJSSWitness inst) : Prop :=
  76  weightTarget inst w ∧ residueNeutral inst w ∧ jCostBound inst w
  77
  78theorem rungCost_nonneg (inst : BJSSInstance) (i : Fin inst.n) :
  79    0 ≤ rungCost inst i := by
  80  unfold rungCost
  81  exact Cost.Jcost_nonneg (rungValue_pos (inst.rung i))
  82
  83theorem totalJCost_nonneg (inst : BJSSInstance) (w : BJSSWitness inst) :
  84    0 ≤ totalJCost inst w := by
  85  unfold totalJCost
  86  exact Finset.sum_nonneg (fun i _hi => rungCost_nonneg inst i)
  87
  88/-- Classical decidability of the finite solution predicate. This is only a
  89finite search statement, not an efficiency claim. -/
  90noncomputable def solutionDecidable (inst : BJSSInstance) (w : BJSSWitness inst) :
  91    Decidable (isSolution inst w) := by
  92  classical
  93  exact inferInstance
  94
  95/-- Ordinary subset-sum embeds by using zero residues, zero rungs, and zero
  96cost bound. -/
  97def fromSubsetSum {n : ℕ} (weight : Fin n → ℤ) (target : ℤ) : BJSSInstance where
  98  n := n
  99  weight := weight
 100  residue := fun _ => 0
 101  rung := fun _ => 0
 102  target := target
 103  bound := 0
 104
 105theorem fromSubsetSum_totalJCost_zero {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 106    (S : Finset (Fin n)) :
 107    totalJCost (fromSubsetSum weight target) ⟨S⟩ = 0 := by
 108  simp [totalJCost, rungCost, fromSubsetSum, Cost.Jcost_unit0]
 109
 110/-- Any ordinary subset-sum solution gives a degenerate BJSS solution. -/
 111theorem fromSubsetSum_isSolution {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 112    (S : Finset (Fin n)) (h : (∑ i ∈ S, weight i) = target) :
 113    isSolution (fromSubsetSum weight target) ⟨S⟩ := by
 114  constructor
 115  · simpa [weightTarget, weightSum, fromSubsetSum] using h
 116  constructor
 117  · simp [residueNeutral, residueSum, fromSubsetSum]
 118  · have hcost := fromSubsetSum_totalJCost_zero weight target S
 119    change totalJCost (fromSubsetSum weight target) ⟨S⟩ ≤ 0
 120    exact le_of_eq hcost
 121
 122end
 123
 124end BalancedJSubsetSum
 125end Cryptography
 126end IndisputableMonolith
 127