Documentation

Anderson4D.Continuum.OpenEdgeOccupiedLabels

Reindexing an open cell word by its occupied labels #

An R-324 cell word has values in the infinite lattice Z4; it is never appropriate to demand surjectivity onto that lattice. Instead, one first fixes its finite support and regards the word as taking values in the subtype of labels that actually occur. An admissible Hepp realization identifies that finite support with the leaves of its tree.

This file proves that the resulting leaf word is surjective and transports raw occurrence counts, selected endpoint labels, the unmarked pairing constraint, and the adjacent-chain weight. It is the exact bridge from the physical cell decomposition to OpenEdgeRawCountFiber.

Surjectivity onto the occupied finite support #

source
theorem Anderson4D.tupleWord_surjective {m : ℕ} (y : Fin m → Z4) :
Function.Surjective (tupleWord y)

A tuple word is tautologically surjective onto its own support.

source
theorem Anderson4D.reindex_tupleWord_surjective {t : PlaneTree} {m : ℕ} (y : Fin m → Z4) (e : HeppLeaf t ≃ ↥(tupleSupport y)) :
Function.Surjective (reindexSupportWord e (tupleWord y))

Transporting the tuple word along any leaf/support equivalence gives a surjective leaf word.

source
def Anderson4D.reindexTupleWordAt {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {y : Fin m → Z4} (hZ : tupleSupport y = Z) :
Fin m → HeppLeaf t

Reindex a tuple whose support has been identified with a fixed finite set Z.

Equations
Instances For
    source
    theorem Anderson4D.reindexTupleWordAt_surjective {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {y : Fin m → Z4} (hZ : tupleSupport y = Z) :
    Function.Surjective (reindexTupleWordAt e hZ)

    A word reindexed over exactly its occupied fixed support is surjective onto the Hepp leaves.

    Exact transport of labels and counts #

    source
    theorem Anderson4D.reindexTupleWordAt_embedding_apply {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {y : Fin m → Z4} (hZ : tupleSupport y = Z) (i : Fin m) :
    ↑(e (reindexTupleWordAt e hZ i)) = y i

    Forgetting the leaf reindexing recovers the original lattice label.

    source
    theorem Anderson4D.wordFiberCount_reindexTupleWordAt {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {y : Fin m → Z4} (hZ : tupleSupport y = Z) (l : HeppLeaf t) :
    wordFiberCount (reindexTupleWordAt e hZ) l = wordFiberCount y ↑(e l)

    Occurrence counts after leaf reindexing are exactly the original lattice-label counts.

    source
    theorem Anderson4D.wordFiberCount_reindexTupleWordAt_eq {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {reference w : Fin m → Z4} (hrefZ : tupleSupport reference = Z) (hwZ : tupleSupport w = Z) (hcount : ∀ (x : ↥Z), wordFiberCount w ↑x = wordFiberCount reference ↑x) (l : HeppLeaf t) :
    wordFiberCount (reindexTupleWordAt e hwZ) l = wordFiberCount (reindexTupleWordAt e hrefZ) l

    Equality of raw counts on the occupied support transports to equality of leaf-word raw profiles.

    source
    theorem Anderson4D.reindexTupleWordAt_apply_eq_of_apply_eq {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {reference w : Fin m → Z4} (hrefZ : tupleSupport reference = Z) (hwZ : tupleSupport w = Z) (i : Fin m) (hi : w i = reference i) :
    reindexTupleWordAt e hwZ i = reindexTupleWordAt e hrefZ i

    Equality at one physical endpoint transports to equality of the corresponding leaf labels.

    Pairing and raw-fibre transport #

    source
    theorem Anderson4D.reindexTupleWordAt_respectsExcept {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (κ : PartialPairing (Fin m)) (a b : Fin m) {y : Fin m → Z4} (hZ : tupleSupport y = Z) (hy : RespectsPairingExcept κ a b y) (i : Fin m) :
    i ≠ a → i ≠ b → reindexTupleWordAt e hZ i = reindexTupleWordAt e hZ (κ i)

    The equality on every unmarked physical pairing edge survives the occupied-label leaf reindexing.

    source
    theorem Anderson4D.reindexTupleWordAt_mem_openEdgeRawCountFixedEndpointFiber {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) (κ : PartialPairing (Fin m)) (a b : Fin m) (reference w : Fin m → Z4) (hrefZ : tupleSupport reference = Z) (hwZ : tupleSupport w = Z) (hcount : ∀ (x : ↥Z), wordFiberCount w ↑x = wordFiberCount reference ↑x) (ha : w a = reference a) (hb : w b = reference b) (hwRespect : RespectsPairingExcept κ a b w) :
    reindexTupleWordAt e hwZ ∈ openEdgeRawCountFixedEndpointFiber κ a b (reindexTupleWordAt e hrefZ)

    A physical word with the same occupied support, raw profile, and selected endpoint labels as a reference maps into the exact raw-count leaf fibre used by Proposition 5.7.

    Adjacent-chain weight #

    source
    theorem Anderson4D.supportChainWeight_tupleWordAt_eq_heppChainWeight {t : PlaneTree} {m : ℕ} {Z : Finset Z4} (e : HeppLeaf t ≃ ↥Z) {y : Fin m → Z4} (hZ : tupleSupport y = Z) :
    supportChainWeight (tupleWordAt hZ) = heppChainWeight (fun (l : HeppLeaf t) => ↑(e l)) (reindexTupleWordAt e hZ)

    The support chain weight is exactly the Hepp chain weight after occupied-label reindexing.