Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Global EJM action and score orbit

Abstract

The actual source and outcome actions form score-constant event orbits.

The source component is the subgroup of node equivalences generated by the 192 original source-copy permutations, and the outcome component is the full permutation group on the four outcomes. The action applies the inverse source equivalence followed by the outcome bijection. The centered score is invariant under each generator and therefore under the generated subgroup, so every event in the resulting group orbit has the same exact integer score.

Theorem 1.1 (The combined global action preserves the actual score).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.actual_score_invariant

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.actual_score_invariant (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actual coefficient functions retain their source-coordinate and common-outcome symmetries. Closure under identity, multiplication and inverse transports the source symmetry to the generated subgroup; composing it with any outcome permutation gives exact score equality.

Theorem 1.2 (Every event in one global orbit has the base score).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.orbit_score_constant

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.orbit_score_constant (✓ std3). ∎

Source. Repository-derived.

Commentary.

Membership in the group orbit is witnessed by one concrete generated source equivalence and outcome permutation, so the combined invariance transports the score from the base event to that orbit member.

Theorem 1.3 (The score is pairwise constant on each global orbit).

Lean statement: D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.orbit_score_pairwise

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/EJM/EJMGlobalScoreInvariant.orbit_score_pairwise (✓ std3). ∎

Source. Repository-derived.

Commentary.

Any two events witnessed in the same generated group orbit have equal scores by comparison through the common base event. This is the reusable orbit-level consequence for later symmetry-reduced certificate arguments.

References