Proof of the tJ-property

Pensieve header: Proof of the $tJ$ property.

SetDirectory["C:\\drorbn\\AcademicPensieve\\2013-04"];
<< CheatSheetJ-Verification.m;
$SeriesCompareDegree = 6;

The tJ equation

Congruent[
γ // tm[u,v,w] // (Subscript[J, w]),
Plus[
γ // (Subscript[J, u]) // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

The radial variation of the tJ equation

The radial variation of the LHS

Congruent[
((((1+ϵ)γ // tm[u,v,w] // (Subscript[J, w]))-(γ // tm[u,v,w] // (Subscript[J, w])))/ϵ),
γ // tm[u,v,w] // (Subscript[RC, w])[γ//tm[u,v,w]] // (Subscript[div, w]) // (Subscript[CC, w])[-γ//tm[u,v,w]]]

The radial variation of the RHS, part 1

Congruent[
((((1+ϵ)γ // (Subscript[J, u]) // tm[u,v,w])-(γ // (Subscript[J, u]) // tm[u,v,w]))/ϵ),
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ] // tm[u,v,w]]

The radial variation of the RHS, part 2a

Congruent[
((((1+ϵ)γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w])-(γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w]))/ϵ),
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w]]

The radial variation of the RHS, part 2b

Congruent[
(((γ // (Subscript[RC, u])[(1+ϵ)γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w])-(γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w]))/ϵ),
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]]  // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w]
]

The radial variation of the RHS, part 2

Congruent[
((((1+ϵ)γ // (Subscript[RC, u])[(1+ϵ)γ] // (Subscript[J, v]) // (Subscript[CC, u])[-(1+ϵ)γ] // tm[u,v,w])-(γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[CC, u])[-γ] // tm[u,v,w]))/ϵ),
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

Congruent[
γ // tm[u,v,w] // (Subscript[RC, w])[γ//tm[u,v,w]] // (Subscript[div, w]) // (Subscript[CC, w])[-γ//tm[u,v,w]],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

Use RC equation t on first term

Congruent[
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]]//tm[u,v,w] // (Subscript[div, w]) // (Subscript[CC, w])[-γ//tm[u,v,w]],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

Use div property t on first term

Congruent[
Plus[
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, u]) //tm[u,v,w]// (Subscript[CC, w])[-γ//tm[u,v,w]],
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) //tm[u,v,w]// (Subscript[CC, w])[-γ//tm[u,v,w]]
],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

Use CC equation t on first two term

Congruent[
Plus[
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, u]) //(Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) //(Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w]
],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ] // tm[u,v,w],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ] // tm[u,v,w]
]]

Cancel all tm[u,v,w]’s, cancel term 2 with term 4

Congruent[
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, u]) //(Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]) // (Subscript[CC, u])[-γ],
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]]// (Subscript[CC, u])[-γ],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]] // (Subscript[CC, u])[-γ]
]]

Cancel (Subscript[CC, u])[-γ] on the right

Congruent[
γ //(Subscript[RC, u])[γ] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, u]) //(Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]],
Plus[
γ // (Subscript[RC, u])[γ] // (Subscript[div, u]),
γ // (Subscript[RC, u])[γ] // (Subscript[ad, u])[γ//(Subscript[RC, u])[γ]] // adSeries[((1-(E^(-ad)))/ad),γ//(Subscript[RC, u])[γ]] // (Subscript[RC, v])[γ//(Subscript[RC, u])[γ]] // (Subscript[div, v]) // (Subscript[CC, v])[-γ//(Subscript[RC, u])[γ]],
γ // (Subscript[RC, u])[γ] // (Subscript[J, v]) // (Subscript[ad, u])[-γ//(Subscript[RC, u])[γ]]
]]

Replace γ //(Subscript[RC, u])[γ]->γ

Congruent[
γ // (Subscript[RC, v])[γ] // (Subscript[div, u]) //(Subscript[CC, v])[-γ],
Plus[
γ // (Subscript[div, u]),
γ // (Subscript[ad, u])[γ] // adSeries[((1-(E^(-ad)))/ad),γ] // (Subscript[RC, v])[γ] // (Subscript[div, v]) // (Subscript[CC, v])[-γ],
γ // (Subscript[J, v]) // (Subscript[ad, u])[-γ]
]]

The above is “Equation Jad” of Juv.nb!