Reference · Signed rationals

rainbow.math.rational.signed.one-hot-attained

Signed rationalssrc/rainbow/math/rational/signed/one_hot_attained.clj0 definitions, 2 theorems

THE ONE-HOT SELECTOR / ATTAINMENT LEMMA, the shared Level-3 reading of every checker that certifies a minimum or maximum with a 0/1 witness (the max/min-type checks). Such a checker proves each candidate's GAP is nonnegative (the certified value is a bound of every candidate), the witness weights are 0/1 and sum to 1, and the witness-weighted gaps sum to 0. The reading is that the witnessed candidate is ATTAINED: signed/one-hot-attained : forall W G k, (forall i < k, 0 <= W i) -> (forall i < k, W i ~ 0 \/ W i ~ 1) -> (forall i < k, 0 <= G i) -> expr-sum-value W k ~ 1 -> expr-sum-value (fun i. W i * G i) k ~ 0 -> exists i, i < k /\ W i ~ 1 /\ G i ~ 0 `0 <= W i` follows from the 0/1 disjunction and is taken as a hypothesis for brevity. `0 <= G i` is NOT needed for the statement to be true: 0/1 weights summing to 1 select exactly one candidate, and the weighted sum is that candidate's gap. This proof's induction uses it, and every one-hot checker supplies it (its bound groups), so the hypothesis costs no consumer anything. Dropping it would need a counting argument instead. Proof, by induction on k with a strengthened claim: the weighted sum S_k is >= 0, and if S_k ~ 0 then either the weights so far sum to ~ 0 or a selected candidate below k is attained. A step splits S_{k+1} = S_k + W_k G_k ~ 0 into two zero parts (both are nonnegative). If the earlier weights sum to 0, either W_k ~ 0 (the total stays 0) or W_k ~ 1 (then G_k ~ W_k G_k ~ 0, attained at k). At the end the weights sum to 1, not 0, which leaves attainment. The sum facts used here are proved inside this induction; the general expr-sum-value algebra is a separate lane.

Depends onmath.checksmath.nat.strict-below-moremath.rational.signed.add-zero-reflectionmath.rational.signed.multiply-ordermath.rational.signed.multiply-ringmath.rational.signed.unit-lawsmath.rational.signed.no-zero-divisorsmath.rational.signed.order-monotonemath.rational.signed.limit-uniquenessmath.rational.signed.map-sum-algebra

signed/one-hot-attained-strengthened :
  (W G : ℕ → ℚ) (k : ℕ)
  (hw : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ W i)
  (h01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (W i = 0) (W i = 1))
  (hg : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ G i)
  → proposition/conjunction (signed/nonnegative (value)) (value = 0 → disjunction)
  where disjunction := proposition/disjunction (signed/expr-sum-value W k = 0) (proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i k) (proposition/conjunction (W i = 1) (G i = 0))))
  where value := signed/expr-sum-value (fun i => W i · G i) k

signed/one-hot-attained :
  (W G : ℕ → ℚ) (k : ℕ)
  (hw : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ W i)
  (h01 : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), proposition/disjunction (W i = 0) (W i = 1))
  (hg : ∀ (i : ℕ), ∀ (hi : nat/strict-below i k), 0 ≤ G i)
  (hsum : signed/expr-sum-value W k = 1)
  (hzero : signed/expr-sum-value (fun i => W i · G i) k = 0)
  → proposition/existence ℕ (fun i => proposition/conjunction (nat/strict-below i k) (proposition/conjunction (W i = 1) (G i = 0)))