The two-wing cone from the flow's own factorisation #
Category: 3-Local (CV; the causal shape of the two-wing experiment, second route). BACKLOG #139, taken the way CSD's own foundations prefer.
TwoWingCone.lean gets the wings' causal separation from a supplied coupling
graph: twoWingGraph has no A–B edge, so the cones never meet. That left #131 with one arena and
two dynamics — the cone came from graphInteractingU, while the Born weights, the record history
and the CHSH value come from LF6.localDeisolationFlow, and nothing related them.
CSD does not want two. specs/CSD-CHARTER.md is explicit that "there is one flow and one
microstate", and the corpus gives the same discharge condition for Posit 1 and Posit 10 — derive it
from the de-isolation dynamics. The fully principled route is therefore one Hamiltonian generating
both, which is the H_int frontier (R-016) and has no cheap brick. This file takes the reachable
form of the same idea: drop the second interaction and read the separation off the measurement flow
itself.
The point #
LF6.localFlowUnitary is reindex … (vnUnitary 2 ⊗ₖ vnUnitary 2) and
LF6.localDeisolation_factorises says the dilation is V_A ⊗ V_B. The measurement interaction is
already a product of per-wing unitaries. A product unitary has disjoint per-wing support, and
disjoint supports commute — so the separation is a property of the measurement, with no graph and
no period count:
- ★★
leftModes_two_twoandrightModes_two_two—CompositeArena's mode blocks atK₁ = K₂ = 2areTwoWingCone's wing mode sets, so that file's machinery and this one's are about the same regions (by decide); - ★★★
supportedOn_heisenberg_pow_of_factorised— the evolved A-observable stays A-local at every power of a factorised flow. This is what replaces the cone: there is no ball to grow, because the B-factor acts trivially on an A-supported observable (heisenberg_eq_of_disjoint) and the A-factor cannot leave A's modes; - ★★★
arenaObs_kick_of_factorisedand ★★★recordStroke_comm_kick_of_factorised— a B-wing intervention cannot steer A's reading or A's record write, after any number of applications of the measurement interaction, exactly; - ★
supportedOn_wingAModes_leftOpand ★supportedOn_wingBModes_rightOp— non-vacuity: every pair of per-wing operators gives the two factors, throughCompositeArena'sleftOp/rightOp.
What this changes for #131, and what it does not #
It changes what is assumed. #131's standing caveat is that adjacency is supplied through E.
Here there is no E: the separation follows from the measurement interaction being a product over
the wings. The assumption moves from "the graph has no A–B edge" to "the apparatus couples each wing
to its own pointer", which is a statement about the experiment rather than about an auxiliary graph.
⚠️ It is still an assumption. localDeisolation_factorises holds by construction — LF6-A.3
chose a product dilation. So locality is still put in, just somewhere more physical. Deriving it is
R-016, and nothing here touches that.
⚠️ Weaker than a cone, and deliberately. A product unitary gives static locality — disjoint
supports commute — not a propagating bound with a velocity. That is the right statement for one
measurement: the question is whether the two wings' records can influence each other, and disjoint
support answers it exactly. A propagating cone matters only for a dynamics that is not a product,
i.e. if the wings were coupled, which this experiment says they are not.
TwoWingCone.lean keeps the graded version for that case; neither file
supersedes the other.
⚠️ The index alignment with LF6 is checked but not formalised. LF6.jointDilEquiv regroups
((sᴀ,pᴀ),(s_b,p_b)) ↦ ((sᴀ,s_b),(pᴀ,p_b)), so the dilated space is four Fin 2 factors grouped per
wing, and FieldConfig 4 2 = Fin 4 → Fin 2 is four Fin 2 factors indexed by mode; under
modes 0,1 = (sysA, ptrA) and modes 2,3 = (sysB, ptrB) the de-isolation's tensor split is the
wing mode split, which is why wingAModes = {0,1} was the right choice. Carrying
localFlowUnitary itself across that alignment is bookkeeping this file does not do: the theorems
below are stated for any wing-factorised flow and instantiated at leftOp/rightOp, not at
localFlowUnitary. Until that is done, "the de-isolation flow satisfies the hypothesis" is a
checked claim about index conventions, not a theorem.
References: TwoWingCone.lean (wingAModes, wingBModes, and the graph route
this is the alternative to), CompositeArena.lean (leftModes,
rightModes, leftOp, rightOp, leftOp_supportedOn, composite_no_signalling — the static
version of the same idea), SupportSpreading.lean
(heisenberg_eq_of_disjoint, heisenberg_supportedOn_union),
ArenaBridge.lean (arenaObs_kick_of_disjointSupport),
LF6/LocalDeisolationFlow.lean (localFlowUnitary, localDeisolation_factorises, jointDilEquiv
— the flow this is about, not imported); specs/CSD-CHARTER.md ("one flow and one microstate");
specs/BACKLOG.md #139, #131, R-016.
The two files' mode regions agree #
★★ CompositeArena's left block is A's wing. So the composite machinery and
TwoWingCone.lean are about the same modes, and nothing has been re-indexed
between them.
★★ And the right block is B's wing.
The cone, from factorisation #
★★★ A wing-factorised flow cannot spread an A-local observable. At every power of
U_A * U_B, the Heisenberg-evolved observable is still supported on A's modes: the B-factor acts
trivially on it (heisenberg_eq_of_disjoint) and the A-factor cannot take it outside A.
This is what replaces a light cone. There is no ball to grow — not because the propagation is slow, but because the interaction does not couple the wings at all.
★★★ A B-wing intervention cannot steer A's reading, exactly, after any number of applications of a wing-factorised flow. No graph, no period budget, no error term.
★★★ And it cannot steer A's record write. The fibred form, which is the statement #131's obligation (3) asks for — here with the separation read off the measurement interaction rather than off a supplied graph.
Non-vacuity: every pair of per-wing unitaries gives such a flow #
★ The A-wing factor of a product flow, as an operator on the four-mode configuration space:
CompositeArena's leftOp, whose support is A's modes by leftOp_supportedOn.
★ The B-wing factor.