9.2. 5. A direct positive scalar certificate🔗

9.2.1. 5.1 The priced profile🔗

Put

\beta=\frac{23}{250},\quad\gamma=\frac7{60},\quad\alpha=\frac{103}{1000},\quad\kappa=\frac{23}{1000},\qquad G(s)=\gamma-\alpha s-\kappa s^2.

Theorem9.2.1.1

Group: The pair charge. (8)

Group member previews

Preview

Theorem 9.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma PC5.1 (the price). For 0\le s\le2, b(s)>0 and

b(s)[\beta\Psi'(s)-\alpha-2\kappa s]=\frac{1071}{64000}\left(s-\frac{170}{1071}\right)^2+\frac{1343}{17136000} +\frac{69}{32000}s^2(2-s)>0, \qquad \text{(PC-PRICE)}

\beta\Psi(s)\ge\alpha s+\kappa s^2. \qquad \text{(PC-PRICE-INTEGRAL)}

Lean code for Theorem9.2.1.1●1 theorem

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_price {t : ℝ} (ht : 0 ≤ t)
  (ht2 : t ≤ 2) :
  103 * t / 1000 + 23 * t ^ 2 / 1000 ≤
    23 / 250 * NaturalLatents.General.separationPrice t

theorem NaturalLatents.General.pairCharge_price
  {t : ℝ} (ht : 0 ≤ t) (ht2 : t ≤ 2) :
  103 * t / 1000 + 23 * t ^ 2 / 1000 ≤
    23 / 250 *
      NaturalLatents.General.separationPrice
        t

C8, (PRICE) and (PRICE-INTEGRAL): `(103/1000) t + (23/1000) t^2 ≤ (23/250) separationPrice t` on `[0, 2]`.
The derivative of `(23/250) separationPrice - 103 t/1000 - 23 t^2/1000` is
`((1071/64000)(t - 170/1071)^2 + 1343/17136000 + (69/32000) t^2 (2 - t)) / affinityPoly t ≥ 0`.

Proof for Theorem 9.2.1.1

uses 0

Lean proves: (23/250)\Psi(s)\ge(103/1000)s+(23/1000)s^2 for 0\le s\le2, the inequality (PC-PRICE-INTEGRAL).

Complete squares in the price derivative and integrate the positive derivative from the zero endpoint. See the page section.

Lean: pairCharge_price (NaturalLatents/General/PairCharge/Certificate.lean) states (PC-PRICE-INTEGRAL) only, for 0\le t\le2; the identity (PC-PRICE) and b>0 enter its proof but not its statement.

9.2.2. 5.2 Three positive quartics🔗

The proof uses explicitly given constants: the shift s/5 in W, the slope \lambda, the weight k, the profile coefficients \alpha,\kappa, the polynomials M_l,M_m,M_h and the fifteen numerator coefficients below. Nothing depends on how they were found: every identity below is checked by exact rational arithmetic.

For 0\le s\le1 and 1/16\le j\le1/2 put q=(16j-1)/7, so 0\le q\le1, and define

\begin{aligned} F(s,j)&=3(1-s+sj)^2-G(s)\mathrm{Den}(s,j),\qquad F_l(s)=F(s,1/16),\qquad F_h(s)=F(s,1/2),\\ F_m(s)&=\frac{F_l(s)+F_h(s)}2-\frac{49}{512}[3+G(s)]s^2. \end{aligned}

Theorem9.2.2.1

Group: The pair charge. (8)

Group member previews

Preview

Theorem 9.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma PC5.2 (the scalar certificate). For 0\le s\le1 and 1/16\le j\le1/2,

F(s,j)=(1-q)^2F_l(s)+2q(1-q)F_m(s)+q^2F_h(s), \qquad \text{(PC-INTERPOLATION)}

3(1-s+sj)^2-G(s)\mathrm{Den}(s,j)>0. \qquad \text{(PC-SCALAR)}

Lean code for Theorem9.2.2.1●4 theorems

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_quartic_low {s : ℝ} (hs : 0 ≤ s) :
  0 < NaturalLatents.General.pairChargeScalar s (1 / 16)

theorem NaturalLatents.General.pairCharge_quartic_low
  {s : ℝ} (hs : 0 ≤ s) :
  0 <
    NaturalLatents.General.pairChargeScalar
      s (1 / 16)

C9, edge `j = 1/16`: `F_l = M_l + (2907750 + 6796995 s + 137267 s^2 + 6234675 s^3 + 528825 s^4)/2880000000`.

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_quartic_mid {s : ℝ} (hs : 0 ≤ s) :
  0 <
    (NaturalLatents.General.pairChargeScalar s (1 / 16) +
          NaturalLatents.General.pairChargeScalar s (1 / 2)) /
        2 -
      49 / 512 * (3 + NaturalLatents.General.pairChargeProfile s) *
        s ^ 2

theorem NaturalLatents.General.pairCharge_quartic_mid
  {s : ℝ} (hs : 0 ≤ s) :
  0 <
    (NaturalLatents.General.pairChargeScalar
            s (1 / 16) +
          NaturalLatents.General.pairChargeScalar
            s (1 / 2)) /
        2 -
      49 / 512 *
          (3 +
            NaturalLatents.General.pairChargeProfile
              s) *
        s ^ 2

C9, the Bernstein middle coefficient
`F_m = (F_l + F_h)/2 - (49/512)(3 + G(s)) s^2 = M_m + (77550 + 106007463 s + 57708163 s^2 + 5565 s^3 + 469995 s^4)/1152000000`.

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_quartic_high {s : ℝ} (hs : 0 ≤ s)
  (hs1 : s ≤ 1) : 0 < NaturalLatents.General.pairChargeScalar s (1 / 2)

theorem NaturalLatents.General.pairCharge_quartic_high
  {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) :
  0 <
    NaturalLatents.General.pairChargeScalar
      s (1 / 2)

C9, edge `j = 1/2`: `F_h = M_h + (8000 + 10005 s + 116424 s^2 + 612 s^3 + 828 s^4)/3600000`.

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_scalar_certificate {s j : ℝ}
  (hs : 0 ≤ s) (hs1 : s ≤ 1) (hjlo : 1 / 16 ≤ j) (hjhi : j ≤ 1 / 2) :
  NaturalLatents.General.pairChargeProfile s *
      NaturalLatents.General.pairChargeDenominator s j <
    3 * (1 - s + s * j) ^ 2

theorem NaturalLatents.General.pairCharge_scalar_certificate
  {s j : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1)
  (hjlo : 1 / 16 ≤ j) (hjhi : j ≤ 1 / 2) :
  NaturalLatents.General.pairChargeProfile
        s *
      NaturalLatents.General.pairChargeDenominator
        s j <
    3 * (1 - s + s * j) ^ 2

C9, (INTERPOLATION) and (SCALAR): `G(s) B(s, j) < 3 (1 - s + s j)^2` on `[0,1] × [1/16, 1/2]`.
With `q = (16 j - 1)/7`, `F(s, j) = (1-q)^2 F_l + 2 q (1-q) F_m + q^2 F_h` exactly.

Proof for Theorem 9.2.2.1

uses 0

Lean proves: F_l>0, F_m>0 and F_h>0 on their stated scalar domains, and 3(1-s+sj)^2-G(s)\mathrm{Den}(s,j)>0 for 0\le s\le1 and 1/16\le j\le1/2.

Interpolate quadratically in the normalized quartic ratio and certify each edge quartic by exact rational positive decompositions. See the page section.

Lean: pairCharge_quartic_low, pairCharge_quartic_mid and pairCharge_quartic_high (NaturalLatents/General/PairCharge/Certificate.lean) state the positivity consequences of (PC-CERTIFICATE), F_l>0, F_m>0 and F_h>0, the first two for s\ge0 and the third for 0\le s\le1; the certificate identities appear only in their proofs. pairCharge_scalar_certificate (same file) states (PC-SCALAR), with (PC-INTERPOLATION) used only in its proof. The scalar functions G, \lambda, k, \mathrm{Den}(s,j) and F are pairChargeProfile, pairChargeSlope, pairChargeWeight, pairChargeDenominator and pairChargeScalar (same file).

Theorem9.2.2.2

Group: The pair charge. (8)

Group member previews

Preview

Theorem 9.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 4

Statement dependency previews

Preview

Theorem 9.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagspartly kernel-verified

Theorem PC5.3 (the pair charge C). For every finite nonempty X,Y, every nonempty S with all rows and columns used, every feasible w>0 on S, and every pair of distinct positive contacts P,R of w,

\frac{I(P)+I(R)}2+\frac{23}{250}\Psi(s)>\frac7{60}.

Lean code for Theorem9.2.2.2●7 theorems

theoremdefined in NaturalLatents/General/PairCharge.lean

complete

theorem NaturalLatents.General.pairCharge_C {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y] :
  NaturalLatents.General.HasPairCharge
    NaturalLatents.General.CommonSupportPair (23 / 250) (7 / 60)

theorem NaturalLatents.General.pairCharge_C
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y] :
  NaturalLatents.General.HasPairCharge
    NaturalLatents.General.CommonSupportPair
    (23 / 250) (7 / 60)

The pair charge C on common finite supports, including supports with holes.

theoremdefined in NaturalLatents/General/Contact.lean

complete

theorem NaturalLatents.General.contact_moments {X Y : Type} [Fintype X]
  [Fintype Y] [DecidableEq X] [DecidableEq Y] {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  NaturalLatents.General.ContactMoments S P R

theorem NaturalLatents.General.contact_moments
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  NaturalLatents.General.ContactMoments S
    P R

Two distinct positive contacts `P`, `R` of a common feasible kernel satisfy the moment relations of
`ContactMoments`, in particular `quarticMoment P R ≤ separation P R ^ 2 / 2`.

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_price {t : ℝ} (ht : 0 ≤ t)
  (ht2 : t ≤ 2) :
  103 * t / 1000 + 23 * t ^ 2 / 1000 ≤
    23 / 250 * NaturalLatents.General.separationPrice t

theorem NaturalLatents.General.pairCharge_price
  {t : ℝ} (ht : 0 ≤ t) (ht2 : t ≤ 2) :
  103 * t / 1000 + 23 * t ^ 2 / 1000 ≤
    23 / 250 *
      NaturalLatents.General.separationPrice
        t

C8, (PRICE) and (PRICE-INTEGRAL): `(103/1000) t + (23/1000) t^2 ≤ (23/250) separationPrice t` on `[0, 2]`.
The derivative of `(23/250) separationPrice - 103 t/1000 - 23 t^2/1000` is
`((1071/64000)(t - 170/1071)^2 + 1343/17136000 + (69/32000) t^2 (2 - t)) / affinityPoly t ≥ 0`.

theoremdefined in NaturalLatents/General/PairCharge.lean

complete

theorem NaturalLatents.General.pairCharge_information_floor {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R)
  (hs1 : NaturalLatents.General.separation P R ≤ 1) :
  0 <
      NaturalLatents.General.pairChargeDenominator
        (NaturalLatents.General.separation P R)
        (NaturalLatents.General.quarticRatio P R) ∧
    3 *
          (1 - NaturalLatents.General.separation P R +
              NaturalLatents.General.separation P R *
                NaturalLatents.General.quarticRatio P R) ^
            2 /
        NaturalLatents.General.pairChargeDenominator
          (NaturalLatents.General.separation P R)
          (NaturalLatents.General.quarticRatio P R) ≤
      (stoch_to_det.Knat P + stoch_to_det.Knat R) / 2

theorem NaturalLatents.General.pairCharge_information_floor
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R)
  (hs1 :
    NaturalLatents.General.separation P
        R ≤
      1) :
  0 <
      NaturalLatents.General.pairChargeDenominator
        (NaturalLatents.General.separation
          P R)
        (NaturalLatents.General.quarticRatio
          P R) ∧
    3 *
          (1 -
                NaturalLatents.General.separation
                  P R +
              NaturalLatents.General.separation
                  P R *
                NaturalLatents.General.quarticRatio
                  P R) ^
            2 /
        NaturalLatents.General.pairChargeDenominator
          (NaturalLatents.General.separation
            P R)
          (NaturalLatents.General.quarticRatio
            P R) ≤
      (stoch_to_det.Knat P +
          stoch_to_det.Knat R) /
        2

The positive scalar denominator gives the averaged information floor.

theoremdefined in NaturalLatents/General/PairCharge/MomentBounds.lean

complete

theorem NaturalLatents.General.pairCharge_quarticRatio_bounds {X Y : Type}
  [Fintype X] [Fintype Y] [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)} {w P R : NaturalLatents.General.Law X Y}
  (hpair : NaturalLatents.General.CommonSupportPair S w P R) :
  1 / 16 ≤ NaturalLatents.General.quarticRatio P R ∧
    NaturalLatents.General.quarticRatio P R ≤ 1 / 2

theorem NaturalLatents.General.pairCharge_quarticRatio_bounds
  {X Y : Type} [Fintype X] [Fintype Y]
  [DecidableEq X] [DecidableEq Y]
  {S : Finset (X × Y)}
  {w P R : NaturalLatents.General.Law X Y}
  (hpair :
    NaturalLatents.General.CommonSupportPair
      S w P R) :
  1 / 16 ≤
      NaturalLatents.General.quarticRatio
        P R ∧
    NaturalLatents.General.quarticRatio P
        R ≤
      1 / 2

theoremdefined in NaturalLatents/General/PairCharge/Certificate.lean

complete

theorem NaturalLatents.General.pairCharge_scalar_certificate {s j : ℝ}
  (hs : 0 ≤ s) (hs1 : s ≤ 1) (hjlo : 1 / 16 ≤ j) (hjhi : j ≤ 1 / 2) :
  NaturalLatents.General.pairChargeProfile s *
      NaturalLatents.General.pairChargeDenominator s j <
    3 * (1 - s + s * j) ^ 2

theorem NaturalLatents.General.pairCharge_scalar_certificate
  {s j : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1)
  (hjlo : 1 / 16 ≤ j) (hjhi : j ≤ 1 / 2) :
  NaturalLatents.General.pairChargeProfile
        s *
      NaturalLatents.General.pairChargeDenominator
        s j <
    3 * (1 - s + s * j) ^ 2

C9, (INTERPOLATION) and (SCALAR): `G(s) B(s, j) < 3 (1 - s + s j)^2` on `[0,1] × [1/16, 1/2]`.
With `q = (16 j - 1)/7`, `F(s, j) = (1-q)^2 F_l + 2 q (1-q) F_m + q^2 F_h` exactly.

theoremdefined in NaturalLatents/Upstream/ContactInformation.lean

complete

theorem stoch_to_det.Knat_nonneg.{u_1, u_2} {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β]
  {q : α × β → ℝ} (hq : stoch_to_det.IsPMF q) : 0 ≤ stoch_to_det.Knat q

theorem stoch_to_det.Knat_nonneg.{u_1, u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype α] [Fintype β] [DecidableEq α]
  [DecidableEq β] {q : α × β → ℝ}
  (hq : stoch_to_det.IsPMF q) :
  0 ≤ stoch_to_det.Knat q

Nonnegativity of the natural mutual-information budget.

Proof for Theorem 9.2.2.2

uses 0

Lean proves: (I(P)+I(R))/2+(23/250)\Psi(s)\ge7/60 for distinct positive contacts of a common feasible kernel, the non-strict charge HasPairCharge CommonSupportPair (23/250) (7/60).

For separation at most one, combine the information floor, positive scalar certificate, and price; above one, the price and nonnegative information suffice. See the page section.

Lean: pairCharge_C (NaturalLatents/General/PairCharge.lean), stating HasPairCharge CommonSupportPair (23/250) (7/60). It uses contact_moments for 0<s<2 and pairCharge_price; for s\le1, pairCharge_information_floor, pairCharge_quarticRatio_bounds and pairCharge_scalar_certificate; and for s>1, stoch_to_det.Knat_nonneg (NaturalLatents/Upstream/ContactInformation.lean) for nonnegative information. Lean splits the cases at s\le1 and s>1. Lean's HasPairCharge is the non-strict inequality; the strict form is proved on the page.