Multi-block endpoint fibres for R-322

This file continues the all-order closure after the partition and terminal primitive identities. A member of a fixed endpoint-signature fibre is recorded by its increasingly ordered primitive restriction on every concrete Definition 3.1 extraction block. The first result below is the exact faithfulness statement: those block coordinates determine the ambient pairing with no quotient and no multiplicity.

The complete primitive coordinate family

@[reducible, inline]

abbrev Anderson4D.ExtractionBlockIndex {m : ℕ} (κ : PartialPairing (Fin m)) : Type

The concrete blocks in the Definition 3.1 schedule, retaining their membership proofs so that dependent primitive orders can be used.

Equations

• Anderson4D.ExtractionBlockIndex κ = { B : Finset (Fin m) // B ∈ Anderson4D.extractionBlocks κ }

@[reducible, inline]

abbrev Anderson4D.ExtractionPrimitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) : Type

One standard primitive pairing coordinate on every concrete extraction block.

Equations

• Anderson4D.ExtractionPrimitiveCoordinates κ = ((B : Anderson4D.ExtractionBlockIndex κ) → ↥(Anderson4D.primitiveFullPairings (Anderson4D.residualBlockOrder ↑B)))

theorem Anderson4D.endpointFiber_isFullyPairedOn_extractionBlock {m : ℕ} (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) (B : ExtractionBlockIndex κ) : IsFullyPairedOn ↑τ ↑B

A signature-fibre member is fully paired on every reference extraction block.

theorem Anderson4D.endpointFiber_isRelPrimitiveOn_extractionBlock {m : ℕ} (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) (B : ExtractionBlockIndex κ) : IsRelPrimitiveOn ↑τ ↑B

A signature-fibre member is relatively primitive on every reference extraction block.

def Anderson4D.endpointFiberPrimitiveCoordinate {m : ℕ} (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) (B : ExtractionBlockIndex κ) : ↥(primitiveFullPairings (residualBlockOrder ↑B))

Increasing standardization of one reference block of a signature-fibre member.

Equations

• Anderson4D.endpointFiberPrimitiveCoordinate κ τ B = ⟨Anderson4D.orderedBlockPairing ↑τ ↑B ⋯ (Anderson4D.residualPrimitiveBlockOrderIso κ ↑B ⋯), ⋯⟩

def Anderson4D.endpointFiberPrimitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) : ExtractionPrimitiveCoordinates κ

All primitive block coordinates of one endpoint-fibre member.

Equations

• Anderson4D.endpointFiberPrimitiveCoordinates κ τ B = Anderson4D.endpointFiberPrimitiveCoordinate κ τ B

theorem Anderson4D.endpointFiberPrimitiveCoordinate_apply {m : ℕ} (κ : PartialPairing (Fin m)) (τ : ReductionEndpointFiberAt κ) (B : ExtractionBlockIndex κ) (j : Fin (2 * residualBlockOrder ↑B)) : ↑((residualPrimitiveBlockOrderIso κ ↑B ⋯) (↑(endpointFiberPrimitiveCoordinate κ τ B) j)) = ↑τ ↑((residualPrimitiveBlockOrderIso κ ↑B ⋯) j)

Evaluation of a standardized block coordinate recovers the ambient pairing on that block.

theorem Anderson4D.endpointFiberPrimitiveCoordinates_injective {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) : Function.Injective (endpointFiberPrimitiveCoordinates κ)

The complete family of primitive block coordinates is faithful. This is the multiplicity-free component of the multi-block product equivalence.

Reassembling a coordinate family

theorem Anderson4D.eq_of_mem_of_mem_of_pairwise_disjoint {α : Type u_1} [DecidableEq α] {blocks : List (Finset α)} (hpairwise : List.Pairwise Disjoint blocks) {B C : Finset α} (hB : B ∈ blocks) (hC : C ∈ blocks) {i : α} (hiB : i ∈ B) (hiC : i ∈ C) : B = C

In a pairwise-disjoint list, two members which meet are equal.

noncomputable def Anderson4D.extractionBlockAt {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (i : Fin m) : ExtractionBlockIndex κ

The unique concrete extraction block containing an index of a full pairing.

Equations

• Anderson4D.extractionBlockAt κ hκ i = ⟨Classical.choose ⋯, ⋯⟩

theorem Anderson4D.extractionBlockAt_contains {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (i : Fin m) : i ∈ ↑(extractionBlockAt κ hκ i)

theorem Anderson4D.extractionBlockAt_eq {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (i : Fin m) (B : ExtractionBlockIndex κ) (hiB : i ∈ ↑B) : extractionBlockAt κ hκ i = B

Characterization of the chosen block by membership.

noncomputable def Anderson4D.extractionPrimitiveCoordinatesApply {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) : Fin m

Apply a complete coordinate family on the unique extraction block containing the input index.

Equations

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

theorem Anderson4D.extractionPrimitiveCoordinatesApply_eq {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) : extractionPrimitiveCoordinatesApply κ hκ coordinates i = let B := extractionBlockAt κ hκ i; have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, ⋯⟩)))

Controlled unfolding equation for blockwise coordinate application.

theorem Anderson4D.extractionPrimitiveCoordinatesApply_mem {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) : extractionPrimitiveCoordinatesApply κ hκ coordinates i ∈ ↑(extractionBlockAt κ hκ i)

Applying a coordinate stays in the same concrete extraction block.

theorem Anderson4D.extractionBlockAt_apply {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) : extractionBlockAt κ hκ (extractionPrimitiveCoordinatesApply κ hκ coordinates i) = extractionBlockAt κ hκ i

The block lookup is stable under coordinate application.

theorem Anderson4D.extractionPrimitiveCoordinatesApply_of_mem {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) (B : ExtractionBlockIndex κ) (hiB : i ∈ ↑B) : extractionPrimitiveCoordinatesApply κ hκ coordinates i = have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, hiB⟩)))

Coordinate application written using any certified block containing the input, rather than the noncomputable block lookup.

theorem Anderson4D.extractionPrimitiveCoordinatesApply_involutive {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) : Function.Involutive (extractionPrimitiveCoordinatesApply κ hκ coordinates)

The blockwise application is an involution because every primitive coordinate is an involution and its image stays in the same block.

noncomputable def Anderson4D.partialPairingOfExtractionPrimitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) : PartialPairing (Fin m)

Ambient pairing obtained by independently installing every primitive coordinate on the complete extraction-block partition.

Equations

• Anderson4D.partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates = { toFun := Anderson4D.extractionPrimitiveCoordinatesApply κ hκ coordinates, involutive := ⋯ }

theorem Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_apply_of_mem {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (i : Fin m) (B : ExtractionBlockIndex κ) (hiB : i ∈ ↑B) : (partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates) i = have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, hiB⟩)))

theorem Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_closedOn {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (B : ExtractionBlockIndex κ) (i : Fin m) : i ∈ ↑B → (partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates) i ∈ ↑B

The assembled ambient pairing is closed on every reference block.

theorem Anderson4D.orderedBlockPairing_partialPairingOfExtractionPrimitiveCoordinates {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (B : ExtractionBlockIndex κ) : orderedClosedBlockPairing (↑B) (residualPrimitiveBlockOrderIso κ ↑B ⋯) ⟨partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates, ⋯⟩ = ↑(coordinates B)

Increasing restriction of the assembled pairing is the prescribed primitive coordinate.

noncomputable def Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_primitiveClosedOn {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (B : ExtractionBlockIndex κ) : PrimitiveClosedOn (residualBlockOrder ↑B) (↑B) (residualPrimitiveBlockOrderIso κ ↑B ⋯)

The assembled ambient pairing, certified as primitive on one concrete reference block.

Equations

• Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_primitiveClosedOn κ hκ coordinates B = ⟨⟨Anderson4D.partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates, ⋯⟩, ⋯⟩

theorem Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_isFullyPairedOn {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (B : ExtractionBlockIndex κ) : IsFullyPairedOn (partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates) ↑B

theorem Anderson4D.partialPairingOfExtractionPrimitiveCoordinates_isRelPrimitiveOn {m : ℕ} (κ : PartialPairing (Fin m)) (hκ : κ.IsFull) (coordinates : ExtractionPrimitiveCoordinates κ) (B : ExtractionBlockIndex κ) : IsRelPrimitiveOn (partialPairingOfExtractionPrimitiveCoordinates κ hκ coordinates) ↑B

Carrier-generic primitive-partition product equivalence

@[reducible, inline]

abbrev Anderson4D.PrimitivePartitionBlockIndex {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : Type

Blocks of an arbitrary complete primitive partition.

Equations

• Anderson4D.PrimitivePartitionBlockIndex P = { B : Finset (Fin n) // B ∈ P.blocks }

@[reducible, inline]

abbrev Anderson4D.PrimitivePartitionCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : Type

Independent standard primitive pairing coordinates on all blocks of an arbitrary complete primitive partition.

Equations

• Anderson4D.PrimitivePartitionCoordinates P = ((B : Anderson4D.PrimitivePartitionBlockIndex P) → ↥(Anderson4D.primitiveFullPairings (Anderson4D.residualBlockOrder ↑B)))

@[reducible, inline]

abbrev Anderson4D.PrimitivePartitionFiber {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : Type

Ambient pairings which are closed, full, and relatively primitive on every block of a fixed complete primitive partition.

Equations

• Anderson4D.PrimitivePartitionFiber P = { τ : Anderson4D.PartialPairing (Fin n) // ∀ B ∈ P.blocks, Anderson4D.IsFullyPairedOn τ B ∧ Anderson4D.IsRelPrimitiveOn τ B }

def Anderson4D.primitivePartitionFiberCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (τ : PrimitivePartitionFiber P) : PrimitivePartitionCoordinates P

Standard primitive coordinates of a generic fixed-block fibre member.

Equations

• Anderson4D.primitivePartitionFiberCoordinates P τ B = ⟨Anderson4D.orderedBlockPairing ↑τ ↑B ⋯ (Anderson4D.residualPrimitiveBlockOrderIso κ ↑B ⋯), ⋯⟩

noncomputable def Anderson4D.primitivePartitionBlockAt {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (i : Fin n) : PrimitivePartitionBlockIndex P

The unique block of a complete primitive partition containing an ambient index.

Equations

• Anderson4D.primitivePartitionBlockAt P i = ⟨Classical.choose ⋯, ⋯⟩

theorem Anderson4D.primitivePartitionBlockAt_contains {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (i : Fin n) : i ∈ ↑(primitivePartitionBlockAt P i)

theorem Anderson4D.primitivePartitionBlockAt_eq {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (i : Fin n) (B : PrimitivePartitionBlockIndex P) (hiB : i ∈ ↑B) : primitivePartitionBlockAt P i = B

noncomputable def Anderson4D.primitivePartitionCoordinatesApply {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (i : Fin n) : Fin n

Blockwise application for a generic primitive partition.

Equations

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

theorem Anderson4D.primitivePartitionCoordinatesApply_eq {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (i : Fin n) : primitivePartitionCoordinatesApply P coordinates i = let B := primitivePartitionBlockAt P i; have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, ⋯⟩)))

theorem Anderson4D.primitivePartitionCoordinatesApply_of_mem {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (i : Fin n) (B : PrimitivePartitionBlockIndex P) (hiB : i ∈ ↑B) : primitivePartitionCoordinatesApply P coordinates i = have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, hiB⟩)))

theorem Anderson4D.primitivePartitionCoordinatesApply_mem {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (i : Fin n) : primitivePartitionCoordinatesApply P coordinates i ∈ ↑(primitivePartitionBlockAt P i)

theorem Anderson4D.primitivePartitionCoordinatesApply_involutive {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) : Function.Involutive (primitivePartitionCoordinatesApply P coordinates)

noncomputable def Anderson4D.partialPairingOfPrimitivePartitionCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) : PartialPairing (Fin n)

Reassemble independent primitive coordinates on a generic complete partition.

Equations

• Anderson4D.partialPairingOfPrimitivePartitionCoordinates P coordinates = { toFun := Anderson4D.primitivePartitionCoordinatesApply P coordinates, involutive := ⋯ }

theorem Anderson4D.partialPairingOfPrimitivePartitionCoordinates_apply_of_mem {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (i : Fin n) (B : PrimitivePartitionBlockIndex P) (hiB : i ∈ ↑B) : (partialPairingOfPrimitivePartitionCoordinates P coordinates) i = have e := residualPrimitiveBlockOrderIso κ ↑B ⋯; ↑(e (↑(coordinates B) (e.symm ⟨i, hiB⟩)))

theorem Anderson4D.partialPairingOfPrimitivePartitionCoordinates_closedOn {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (B : PrimitivePartitionBlockIndex P) (i : Fin n) : i ∈ ↑B → (partialPairingOfPrimitivePartitionCoordinates P coordinates) i ∈ ↑B

theorem Anderson4D.orderedBlockPairing_partialPairingOfPrimitivePartitionCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) (B : PrimitivePartitionBlockIndex P) : orderedClosedBlockPairing (↑B) (residualPrimitiveBlockOrderIso κ ↑B ⋯) ⟨partialPairingOfPrimitivePartitionCoordinates P coordinates, ⋯⟩ = ↑(coordinates B)

noncomputable def Anderson4D.primitivePartitionFiberOfCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) (coordinates : PrimitivePartitionCoordinates P) : PrimitivePartitionFiber P

Generic reassembly belongs to the fixed primitive-block fibre.

Equations

• Anderson4D.primitivePartitionFiberOfCoordinates P coordinates = ⟨Anderson4D.partialPairingOfPrimitivePartitionCoordinates P coordinates, ⋯⟩

noncomputable def Anderson4D.primitivePartitionFiberEquivCoordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : PrimitivePartitionFiber P ≃ PrimitivePartitionCoordinates P

Exact carrier-generic product equivalence: a fixed primitive-block fibre has one independent complete primitive pairing coordinate per block, with no quotient and no multiplicity.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.instFintypePrimitivePartitionFiber {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) : Fintype (PrimitivePartitionFiber P)

Equations

• Anderson4D.instFintypePrimitivePartitionFiber P = Fintype.ofEquiv (Anderson4D.PrimitivePartitionCoordinates P) (Anderson4D.primitivePartitionFiberEquivCoordinates P).symm

theorem Anderson4D.sum_primitivePartitionFiber_eq_sum_coordinates {n : ℕ} {κ : PartialPairing (Fin n)} (P : PrimitiveBlockPartition κ) {M : Type u_1} [AddCommMonoid M] (F : PrimitivePartitionFiber P → M) : ∑ τ : PrimitivePartitionFiber P, F τ = ∑ coordinates : PrimitivePartitionCoordinates P, F ((primitivePartitionFiberEquivCoordinates P).symm coordinates)

Reindex any finite sum over a fixed primitive-block fibre as the exact dependent product of primitive coordinates.