PROOF THAT (P1) IS EQUIVALENT TO GIRARD'S `TECHNICAL CONDITION'
===============================================================

Recall Girard's technical condition (G), and condition (P1) from the
LICS paper:

 (G)  if v is a weight generated by the weights occurring in \Theta,
      and x is a &-vertex, then v.~w(x) does not depend on p_x, where
      w(x) is the weight of x and p_x is the eigenvariable of x.

 (P1) for any &-resolution R of \Theta, exactly one linking of \Theta
      is on R.

Here \Theta is a collection of slices \Theta(\phi), one for each
valuation \phi, such that \Theta(\phi) resolves &'s consistently with \phi,
ie, the additive resolution underlying \Theta(\phi) is a subgraph of
the &-resolution R(\phi) determined by \phi.  (Recall that a valuation
is an assignment of 0 or 1 to each eigenvariable, ie, a choice of
right or left for each &.)

To prove (G) <=> (P1) we shall use the following stepping-stone
conditions.  The first is the relaxation of (G) obtained by
restricting to weights of axiom links.

 (G-AX) 
      if v the a weight of an axiom link of \Theta, and x is a &-vertex,
      then v.~w(x) does not depend on p_x.

 (SELF-INDEP) 
      no & depends on itself, ie, for all &-vertices x of \Theta,
      w(x) does not depend on p_x.

 (PRESENCE) 
      an axiom link z depends on a &-vertex x in a slice S only if
      x is in S.
     
(Recall that z depends on x in \Theta(\phi) iff z is in \Theta(\phi)
but not in \Theta(\phi^x), where \phi^x is the valuation obtained from
\phi by toggling the 0/1 value of \phi(x).)
 

PROPOSITION 
===========

  (G)  <=>  (G-AX) and (SELF-INDEP)  <=>  (PRESENCE)  <=>  (P1)
    

Proof of  (G)  <=>  (G-AX) and (SELF-INDEP)
-----------------------------------------

(G)=>(SELF-INDEP) follows by taking v=~w(L) in (G), and the fact that a
weight x depends on p iff ~x depends on p;  (G)=>(G-AX) is trivial.

Conversely,  (G-AX) and (SELF-INDEP) => (G)  because, for any weight u not
depending on p, and any weights w and w',

  (1) [w.u indep of p] and [w'.u indep of p] => (w|w').u indep of p
  (2) [w.u indep of p] and [w'.u indep of p] => (w.w').u indep of p
  (3) w.u indep of p => ~w.u indep of p

(NB x|y = "x or y", and ~w.u=(~w).u) In turn, (1) and (2) follow from

  (a) [x indep p] and [y indep p]  =>  x|y indep p
  (b) [x indep p] and [y indep p]  =>  x.y indep p

respectively, since (w.w').u = (w.u).(w'.u) and (w|w').u = (w.u)|(w'.u).
Finally, for (3), if ~w.u depends on p, then (w.u)|(~w.u) = (w|~w).u = u
depends on p, a contradiction.


Proof of  (G-AX) and (SELF-INDEP)  <=>  (PRESENCE)
------------------------------------------------

We begin with an auxilary Lemma:

Lemma 1.  If x is in \Theta(\phi) but not in \Theta(\phi^x), then some 
          axiom link depends on x in \Theta(\phi^x).

Proof of Lemma 1: 
         let y be the first vertex below x which is in both \Theta(\phi)
         and \Theta(\phi^x); pick an axiom link above y.

Proof of (PRESENCE) => (SELF-INDEP): 
  x self-dependent 
  => x in \Theta(\phi) but not \Theta(\phi^x) 
  => (by Lemma 1) an axiom link depends on x in \Theta(\phi^x) 
  => (by (PRESENCE)) x in \Theta(\phi^x), contradiction.
 
Proof of (G-AX) <=> (PRESENCE), given (SELF-INDEP).  
Below is z an axiom link with weight v.

  (G-AX)  
  <=>
  v.~w(x) indep of p_x   
  <=>
  all \phi. \phi(v.~w(x)) = \phi^x(v.~w(x))   
  <=>
  all \phi. [z in \Theta(\phi) and x not in \Theta(\phi)] iff 
            [z in \Theta(\phi^x) and x not in \Theta(\phi^x)]   
  <=>
  all \phi. x not in \Theta(\phi) implies 
            [z in \Theta(\phi) iff z \in \Theta(\phi^x)]   
  <=> (by (SELF-INDEP))
  all \phi. x not in \Theta(\phi) implies z indep of x in \Theta(\phi)  
  <=> (contrapositive)
  all \phi. z dep on x in \Theta(\phi) implies x in \Theta(\phi)  
  <=>
  (PRESENCE)


Proof of (PRESENCE) <=> (P1)
----------------------------

(PRESENCE) => (P1).  Existence follows immediately by definition of
\Theta as a set of slices \Theta(\phi)\subseteq R(\phi), one for each
valuation \phi.  For uniqueness: suppose \lambda and \lambda' are
distinct linkings of \Theta, say from slices \Theta(\phi) and
\Theta(\phi'), with both \lambda and \lambda' on the same &-resolution R.

Claim: there exists a &-vertex x with \phi(x) not= \phi'(x), and x is
not in at least one of \Theta(\phi) or \Theta(\phi').  Proof of Claim:
pick any x such that \phi(x) not= \phi'(x) [exists, since \phi not=
\phi']; if x is not in R, then it is not in \Theta(\phi)\subseteq R,
as sought; if x is in R, then it cannot be in both \Theta(\phi) and
\Theta(\phi'), since R chooses (say) left for x, and one of
\Theta(\phi) and \Theta(\phi') chooses right (since \phi(x) not=
\phi'(x); QED Claim.

Without loss of generality, x is not in \Theta(\phi).  Thus by
(PRESENCE), \Theta(\phi^x)=\Theta(\phi).  Repeating this argument
for the remaining &-vertices on which \phi and \phi' differ,
we obtain \Theta(\phi')=\Theta(\phi), a contradiction.

(P1) => (PRESENCE).  Suppose the axiom link z depends on x in
\Theta(\phi), and x is not in \Theta(\phi).  Let \lambda be the
linking of \Theta(\phi), and let \lambda' be the linking of
\Theta(\phi^x) (distinct from \lambda, since z depended on x).  Since
\Theta(\phi)\subset R(\phi) [by definition], and x is absent from
\Theta(\phi), we have also \Theta(\phi)\subseteq R(\phi'); thus both
\lambda and \lambda' fit on R(\phi'), contradicting (P1).


DJDH 2003/07/16