The super-Gram identity

The closing display of the proof of RS21's Theorem 6, in the form the converse consumes: the composition's mixed partition function is the superform pairing of the two fragments' tensors. The base sum the composition's own total equals is EdgeSubset.baseSumBitsOf_all of ConverseFamily.lean, read with the bits each subset itself determines, and the tensor side of that sum is EdgeSubset.base_sum_eq_superForm_pairing_bitsOf.

@[reducible]

def RS.EdgeSubset.idBaseOrder (n : ℕ) : LinearOrder (Fin (0 + n) ⊕ Fin (n + 0))

The order the base's labels carry.

Equations

• RS.EdgeSubset.idBaseOrder n = RS.sumLexLinearOrder (Fin (0 + n)) (Fin (n + 0))

@[reducible]

def RS.EdgeSubset.idTopOrder : LinearOrder (Fin 0 ⊕ Fin 0)

The order the composition's own label type carries.

Equations

• RS.EdgeSubset.idTopOrder = RS.sumLexLinearOrder (Fin 0) (Fin 0)

def RS.EdgeSubset.BaseSumIsClosure : Prop

The closure, read on the base with each subset's own bits. The composition's own value is the sum, over the base's subsets, of the ledger-weighted term the pair family gives — each subset read with the bits it itself determines, which is the reading at which a closing cut's two lifts are each other's.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.EdgeSubset.baseSumIsClosure_of_baseSumBitsOf (H : ∀ {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)), BaseSumBitsOf h t (closeBase F G) (pairFamily h t F G) 0) : BaseSumIsClosure

The base sum from the bit-varying sum. The composition's own total is the base sum read with each subset's own bits, once that sum is known; the round trip then replaces the pushed lift by the pair family itself.

theorem RS.EdgeSubset.mixedPartition_pairClose_eq_superForm_of_baseSum (H : BaseSumIsClosure) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) : mixedPartition h (pairClose F G) = (↑k - 2 * ↑ℓ) ^ (closeBase F G).circles * ∑ x : GenBoundaryState k ℓ (Fin t), ∑ y : GenBoundaryState k ℓ (Fin t), (superForm t x y * ∑ s₁ : Finset F.Flag, tensorTermAt F h s₁ x) * ∑ s₂ : Finset G.Flag, tensorTermAt G h s₂ y

The closing identity of RS21's Theorem 6, from the base sum. The closure's value is the superform pairing of the two fragment tensors, at every interface.

theorem RS.EdgeSubset.superGramIdentity_of_baseSum (H : BaseSumIsClosure) : SuperGramIdentity

THE SUPER-GRAM IDENTITY FROM THE BASE SUM. With the base sum, the closing identity of RS21's Theorem 6 holds at every interface, and with it the converse: the closure's value is the superform pairing of the two fragments' tensors.

theorem RS.EdgeSubset.baseSumIsClosure_all : BaseSumIsClosure

THE BASE SUM IS THE CLOSURE. The composition's own value is the base sum read with each subset's own bits — the reading at which a closing cut's two lifts are each other's. Nothing is assumed: the summand does not read the lift's bits at all (summandSum_bits_indep).

theorem RS.EdgeSubset.superGramIdentity : SuperGramIdentity

THE SUPER-GRAM IDENTITY. The closing display of the proof of RS21's Theorem 6: the closure of two fragments, evaluated by the mixed partition function, is the super form of their two tensors — at every interface, closing cuts included.

theorem RS.EdgeSubset.regtsSevensterConverse : RegtsSevensterConverseStatement

THE REGTS–SEVENSTER CONVERSE. Every mixed partition function is an edge-rank-bounded parameter.