addedConfig_eq_addedConfig_iff_left
plain-language theorem explainer
The theorem states that for any natural number N and coupled-core configurations a, a', s the map addedConfig is injective in its first argument when the second argument is held fixed. Researchers modeling finite ququart arrays in recognition frameworks cite it to recover unique displacement labels from observed configurations. The term-mode proof splits the biconditional, applies functional extensionality plus the core add4 injectivity lemma pointwise on the forward direction, and closes the reverse direction by substitution and reflexivity.
Claim. For any natural number $N$ and configurations $a,a',s : Fin N → Fin 4$, the equality $addedConfig(a,s) = addedConfig(a',s)$ holds if and only if $a = a'$, where $addedConfig(a,s)$ is the pointwise four-state addition $(addedConfig(a,s))_x = add4(a_x, s_x)$.
background
CoupledCoreIndex N is the finite-site configuration space of coupled ququart cores, defined as the function type Fin N → Fin 4. The operation addedConfig a s is the pointwise lift of the four-state addition: (addedConfig a s) x := add4 (a x) (s x). The present lemma is the direct functional lift of the sibling result add4_eq_add4_iff_left_core, which establishes the same injectivity on the single-site set Fin 4 by exhaustive case analysis. The local setting is the foundation layer for coupled recognition cores, which supplies concrete finite-N carriers compatible with upstream phi-ladder and Recognition Composition Law structures.
proof idea
The proof is a term-mode construction. It first applies constructor to split the biconditional. The forward direction invokes funext, then extracts the value at each site x via congrArg and feeds the resulting equality into the core lemma add4_eq_add4_iff_left_core. The reverse direction substitutes the hypothesis and concludes by reflexivity.
why it matters
This injectivity supplies the unique-recovery step required by the downstream theorem tensorWeylMonomial_basis_image_orthogonal, which shows that distinct tensor-Weyl displacement labels map coupled basis states to orthogonal outputs. It therefore closes a prerequisite for orthogonality arguments inside the CoupledRecognitionCores module. The result sits inside the foundation layer that realizes finite-N models of the eight-tick octave and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.