Stability of record macrostates under motion of the base

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #104, out of #103.

MacrostateStability.lean (#103) proved the stability of #102's record string under motion of the fibre: the macroscopic law exactly invariant, the pointwise string unchanged outside a set of epistemic measure k·N·δ. That is the only channel a record write opens. A flow of Σ also moves the base, and then the arcs themselves move, because globalBasin c i is cut out by the rate field at the microstate's own base point. This file carries the margin argument over that motion.

What the hypothesis is, and what it is not

The displacement of the arcs is a hypothesis, stated directly on the endpoints:

• arcLo, arcHi — the two endpoints of a context's arc, as functions of the base point;
• ArcShift c ε p q — every arc of c moves by at most ε between the base points p and q. ⚠️ This needs no metric on the base, and so no continuity of the rate field either. #104's row text proposed a LipschitzWith hypothesis; the endpoint form is strictly weaker, available at the pin, and is what the margin argument actually consumes;
• ★ arcShift_of_rate_close — if the rates move by at most η coordinatewise then ArcShift c ((N+1)·η), since each endpoint is a sum of at most N + 1 rates. A modulus of continuity on the rate field enters here and nowhere else.

What is proved

• sigmaMove f g — a move of Σ: a measurable motion f of the base together with a base-dependent record write g. sigmaMove id (fun _ => δ) is #103's sigmaShift;
• ★ ae_fst_eq — the epistemic measure lives on the fibre over its own preparation, and hence ★★★ map_sigmaMove: the epistemic law is carried exactly to the law at the moved base, (epistemicMeasure p).map (sigmaMove f g) = epistemicMeasure (f p). This is the right form of #103's exact half once the base moves: the macroscopic law is not invariant — the Born weights are those of the moved base point — and the transport is still exact, with no error term. The f = id case ★★ map_sigmaMove_id discharges a caveat of #103: a base-dependent write, the recordStroke of CV/RecordInfluence.lean, preserves the epistemic law exactly;
• robustBasin₂ c δ ε i — the two-sided robust interior: margin ε at the lower endpoint and δ + ε at the upper one. Two-sided because a base motion can move the lower endpoint up, which a record write alone never does (robustBasin₂_zero recovers #103's one-sided set at ε = 0);
• ★★ sigmaMove_mem_globalBasin — the margin lemma with the base in motion, and hence ★★ outcomeCode_sigmaMove, ★★★ recordString_sigmaMove and ★★ recordMacro_sigmaMove;
• ★★★ measure_recordString_ne_sigmaMove_le — the microstates a move relabels have epistemic measure at most k·N·(δ + 2ε), and ★★ measure_recordString_ne_sigmaMove_rate_le gives the same in terms of the rate displacement, k·N·(δ + 2(N+1)η);
• ★★ measure_robustBasin₂_ge — robustness is still controlled by the Born weight: rate p i − (δ + 2ε) bounds the two-sided robust interior below;
• ★★★ measure_exists_recordString_ne_flow_le — one exceptional set serves a whole flow. For a one-parameter family of moves whose write stays in [0, δ] and whose arc displacement stays below ε over [0, T], the record string survives the entire horizon outside that same k·N·(δ + 2ε). This is what #103's drift corollary becomes once the base is allowed to move, and it needs no new argument: the robust set does not depend on the parameter.

Honest scope

⚠️ The arc displacement is assumed, not derived. Nothing here shows that any particular flow of Σ — least of all a Hamiltonian one — moves the arcs by a bounded amount, and ContextField still carries no regularity beyond measurability. What arcShift_of_rate_close buys is the reduction of the hypothesis to a modulus of continuity on the rate field; supplying that for the canonical momentContext is not done here, and LF4.momentMap has no recorded modulus.

⚠️ The motion of the base is an arbitrary measurable map, not a flow. f is not assumed invertible, measure-preserving, continuous, or part of a one-parameter group, and no generator is constructed. measure_exists_recordString_ne_flow_le quantifies over a family of such maps; calling it a flow is a convenience of the name, not a claim about its structure.

⚠️ Still not invariance, and still no mixing. As in #103, no cell is shown to be an invariant set and not_hasCorrelationDecay_blockPop_of_unitary is untouched. Note the exact half is weaker here than in #103 and deliberately so: the law moves to epistemicMeasure (f p), so a base motion changes the macroscopic statistics, which is what it should do.

⚠️ The bound degrades as k·N, and in N again through the rates. δ + 2(N+1)η carries a second factor of N, so the rate field has to be uniformly close for a large alphabet. No better constant is claimed, and records of Born weight below δ + 2ε are granted no robustness at all.

⚠️ The typicality half is untouched. As in #103, "overwhelmingly many microstates share it" is conditional on concentration of the weights and is BACKLOG #105; nothing here supplies it, and fs_chebyshev_concentration is still a statement about base statistics.

References: records-to-spacetime-scoping.md ST-3; future-work.md; MacrostateStability.lean (#103), RecordMacrostate.lean (#102), MacroProjection.lean (#99), GlobalBasin.lean, CV/RecordInfluence.lean (fibreShift, recordStroke); specs/BACKLOG.md #104, #103, #105, #100.

The arc endpoints as functions of the base point

noncomputable def CSD.RecordLayer.arcLo {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) : ℝ

The lower endpoint of the arc a context assigns to outcome i, as a function of the base point. globalBasin reads the rate field at the microstate's own base, so moving the base moves this endpoint — which is what #103 did not have to consider.

Equations

• CSD.RecordLayer.arcLo c i p = CSD.RecordLayer.loSum (c.rate p) i

noncomputable def CSD.RecordLayer.arcHi {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) : ℝ

The upper endpoint of the arc, as a function of the base point. Agrees with #103's cellTop read at x.1.

Equations

• CSD.RecordLayer.arcHi c i p = CSD.RecordLayer.loSum (c.rate p) i + c.rate p i

theorem CSD.RecordLayer.cellTop_eq_arcHi {N : ℕ} (c : ContextField N) (i : Fin N) (x : LF4.KSigma N) : cellTop c i x = arcHi c i x.1

theorem CSD.RecordLayer.arcHi_le_one {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) : arcHi c i p ≤ 1

theorem CSD.RecordLayer.arcLo_nonneg {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) : 0 ≤ arcLo c i p

theorem CSD.RecordLayer.measurable_arcLo {N : ℕ} (c : ContextField N) (i : Fin N) : Measurable (arcLo c i)

theorem CSD.RecordLayer.measurable_arcHi {N : ℕ} (c : ContextField N) (i : Fin N) : Measurable (arcHi c i)

theorem CSD.RecordLayer.mem_globalBasin_iff_arc {N : ℕ} (c : ContextField N) (i : Fin N) (x : LF4.KSigma N) : x ∈ globalBasin c i ↔ arcLo c i x.1 < rep x.2.1 ∧ rep x.2.1 ≤ arcHi c i x.1

The basin, written in the endpoint functions — the form the base-motion argument consumes.

The displacement of the arcs

def CSD.RecordLayer.ArcShift {N : ℕ} (c : ContextField N) (ε : ℝ) (p q : LF4.CPN N) : Prop

The arcs of c move by at most ε between the base points p and q. This is the whole hypothesis the base-motion bound needs: it mentions no metric on the base, hence no continuity of the rate field, only that the endpoints do not travel far.

Equations

• CSD.RecordLayer.ArcShift c ε p q = ∀ (i : Fin N), |CSD.RecordLayer.arcLo c i q - CSD.RecordLayer.arcLo c i p| ≤ ε ∧ |CSD.RecordLayer.arcHi c i q - CSD.RecordLayer.arcHi c i p| ≤ ε

theorem CSD.RecordLayer.arcShift_refl {N : ℕ} (c : ContextField N) {ε : ℝ} (hε : 0 ≤ ε) (p : LF4.CPN N) : ArcShift c ε p p

theorem CSD.RecordLayer.ArcShift.mono {N : ℕ} {c : ContextField N} {ε ε' : ℝ} {p q : LF4.CPN N} (h : ArcShift c ε p q) (hle : ε ≤ ε') : ArcShift c ε' p q

theorem CSD.RecordLayer.abs_loSum_sub_le {n : ℕ} (r r' : Fin n → ℝ) {η : ℝ} (hη : 0 ≤ η) (h : ∀ (j : Fin n), |r' j - r j| ≤ η) (i : Fin n) : |loSum r' i - loSum r i| ≤ ↑n * η

A partial sum of rates moves by at most n · η when each rate does. The arithmetic behind arcShift_of_rate_close.

theorem CSD.RecordLayer.arcShift_of_rate_close {N : ℕ} (c : ContextField N) {η : ℝ} (hη : 0 ≤ η) {p q : LF4.CPN N} (h : ∀ (j : Fin N), |c.rate q j - c.rate p j| ≤ η) : ArcShift c ((↑N + 1) * η) p q

★ A modulus of continuity on the rate field bounds the arc displacement. Each endpoint is a sum of at most N + 1 rates, so rates within η put the arcs within (N+1)·η. This is the only place a regularity assumption on ContextField would enter, and #104's row proposed it as a LipschitzWith hypothesis; the endpoint form ArcShift is weaker and is what the margin lemma uses.

A move of Σ: the base travels and a record is written

def CSD.RecordLayer.sigmaMove {N : ℕ} (f : LF4.CPN N → LF4.CPN N) (g : LF4.CPN N → ℝ) (x : LF4.KSigma N) : LF4.KSigma N

A move of Σ: a motion f of the ontic base point together with a base-dependent record write g, the amount written into the record coordinate at each base point. sigmaMove id (fun _ => δ) is #103's sigmaShift, and sigmaMove id g is the base-dependent write of CV/RecordInfluence.lean's recordStroke.

Equations

• CSD.RecordLayer.sigmaMove f g x = (f x.1, x.2.1 + ↑(g x.1), x.2.2)

@[simp]

theorem CSD.RecordLayer.sigmaMove_fst {N : ℕ} (f : LF4.CPN N → LF4.CPN N) (g : LF4.CPN N → ℝ) (x : LF4.KSigma N) : (sigmaMove f g x).1 = f x.1

@[simp]

theorem CSD.RecordLayer.sigmaMove_record {N : ℕ} (f : LF4.CPN N → LF4.CPN N) (g : LF4.CPN N → ℝ) (x : LF4.KSigma N) : (sigmaMove f g x).2.1 = x.2.1 + ↑(g x.1)

@[simp]

theorem CSD.RecordLayer.sigmaMove_partner {N : ℕ} (f : LF4.CPN N → LF4.CPN N) (g : LF4.CPN N → ℝ) (x : LF4.KSigma N) : (sigmaMove f g x).2.2 = x.2.2

theorem CSD.RecordLayer.sigmaMove_id_const {N : ℕ} (δ : ℝ) : (sigmaMove id fun (x : LF4.CPN N) => δ) = sigmaShift δ

theorem CSD.RecordLayer.measurable_sigmaMove {N : ℕ} {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} (hf : Measurable f) (hg : Measurable g) : Measurable (sigmaMove f g)

The epistemic law transports exactly

theorem CSD.RecordLayer.ae_fst_eq {N : ℕ} (p : LF4.CPN N) : ∀ᵐ (x : LF4.KSigma N) ∂epistemicMeasure p, x.1 = p

★ The epistemic measure lives on the fibre over its own preparation. Available because LF4.CPN N has measurable singletons, which is what lets a base-dependent write be replaced by a constant one almost everywhere.

theorem CSD.RecordLayer.map_sigmaMove {N : ℕ} {f : LF4.CPN N → LF4.CPN N} (hf : Measurable f) (g : LF4.CPN N → ℝ) (p : LF4.CPN N) : MeasureTheory.Measure.map (sigmaMove f g) (epistemicMeasure p) = epistemicMeasure (f p)

★★★ The epistemic law is carried exactly to the law at the moved base. The write translates the record coordinate, which Haar measure absorbs; the base map carries the Dirac factor to the Dirac factor at f p. So the macroscopic law after a move is the macroscopic law of the moved preparation — not the same law, and the transport is nevertheless exact, with no error term and no margin hypothesis. This is #103's exact half in the form it takes once the base is allowed to move.

theorem CSD.RecordLayer.map_sigmaMove_id {N : ℕ} (g : LF4.CPN N → ℝ) (p : LF4.CPN N) : MeasureTheory.Measure.map (sigmaMove id g) (epistemicMeasure p) = epistemicMeasure p

★★ A base-dependent record write preserves the epistemic law exactly. The f = id case, and the discharge of #103's caveat: CV/RecordInfluence.lean's recordStroke translates the fibre by an amount read off the base, and that is covered.

The two-sided robust interior

noncomputable def CSD.RecordLayer.robustBasin₂ {N : ℕ} (c : ContextField N) (δ ε : ℝ) (i : Fin N) : Set (LF4.KSigma N)

The (δ, ε)-robust interior of a basin: margin ε at the lower endpoint and δ + ε at the upper one. Two-sided, because a base motion can move the lower endpoint up, which a record write alone never does.

Equations

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

noncomputable def CSD.RecordLayer.lowerBand {N : ℕ} (c : ContextField N) (ε : ℝ) (i : Fin N) : Set (LF4.KSigma N)

The ε-boundary band at the lower endpoint: the first ε of the arc, the part a base motion can push out from below.

Equations

• CSD.RecordLayer.lowerBand c ε i = {x : CSD.LF4.KSigma N | CSD.RecordLayer.arcLo c i x.1 < CSD.RecordLayer.rep x.2.1 ∧ CSD.RecordLayer.rep x.2.1 ≤ CSD.RecordLayer.arcLo c i x.1 + ε}

theorem CSD.RecordLayer.robustBasin₂_zero {N : ℕ} (c : ContextField N) (δ : ℝ) (i : Fin N) : robustBasin₂ c δ 0 i = robustBasin c δ i

theorem CSD.RecordLayer.measurableSet_robustBasin₂ {N : ℕ} (c : ContextField N) (δ ε : ℝ) (i : Fin N) : MeasurableSet (robustBasin₂ c δ ε i)

theorem CSD.RecordLayer.measurableSet_lowerBand {N : ℕ} (c : ContextField N) (ε : ℝ) (i : Fin N) : MeasurableSet (lowerBand c ε i)

theorem CSD.RecordLayer.robustBasin₂_subset_globalBasin {N : ℕ} (c : ContextField N) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (i : Fin N) : robustBasin₂ c δ ε i ⊆ globalBasin c i

theorem CSD.RecordLayer.robustBasin₂_mono {N : ℕ} (c : ContextField N) {δ δ' ε ε' : ℝ} (hδ : δ' ≤ δ) (hε : ε' ≤ ε) (i : Fin N) : robustBasin₂ c δ ε i ⊆ robustBasin₂ c δ' ε' i

theorem CSD.RecordLayer.globalBasin_subset_robustBasin₂_union {N : ℕ} (c : ContextField N) (δ ε : ℝ) (i : Fin N) : globalBasin c i ⊆ robustBasin₂ c δ ε i ∪ lowerBand c ε i ∪ edgeBand c (δ + ε) i

★ Every basin splits into its two-sided robust interior and its two boundary bands.

The margin lemma with the base in motion

theorem CSD.RecordLayer.sigmaMove_mem_globalBasin {N : ℕ} (c : ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ ε : ℝ} (i : Fin N) {x : LF4.KSigma N} (hg0 : 0 ≤ g x.1) (hgδ : g x.1 ≤ δ) (harc : ArcShift c ε x.1 (f x.1)) (hx : x ∈ robustBasin₂ c δ ε i) : sigmaMove f g x ∈ globalBasin c i

★★ The margin lemma under a move of Σ. A move whose write is at most δ and whose arcs travel at most ε cannot take a microstate out of a basin it is (δ, ε)-robustly inside. Both endpoints are in play: the lower one is cleared by the margin ε, the upper one by δ + ε.

theorem CSD.RecordLayer.outcomeCode_sigmaMove {N : ℕ} (c : ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) {i : Fin N} {x : LF4.KSigma N} (hg0 : 0 ≤ g x.1) (hgδ : g x.1 ≤ δ) (harc : ArcShift c ε x.1 (f x.1)) (hx : x ∈ robustBasin₂ c δ ε i) : outcomeCode c (sigmaMove f g x) = outcomeCode c x

★★ A move does not change the outcome a context assigns to a microstate robustly inside one of its basins.

theorem CSD.RecordLayer.recordString_sigmaMove {N k : ℕ} (c : Fin k → ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) {x : LF4.KSigma N} (hg0 : 0 ≤ g x.1) (hgδ : g x.1 ≤ δ) (harc : ∀ (j : Fin k), ArcShift (c j) ε x.1 (f x.1)) (hx : ∀ (j : Fin k), ∃ (i : Fin N), x ∈ robustBasin₂ (c j) δ ε i) : recordString c (sigmaMove f g x) = recordString c x

★★★ A move of Σ leaves the whole record string intact on a microstate robustly inside a basin of every context of the family.

theorem CSD.RecordLayer.recordMacro_sigmaMove {N k : ℕ} (c : Fin k → ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) {x : LF4.KSigma N} (hg0 : 0 ≤ g x.1) (hgδ : g x.1 ≤ δ) (harc : ∀ (j : Fin k), ArcShift (c j) ε x.1 (f x.1)) (hx : ∀ (j : Fin k), ∃ (i : Fin N), x ∈ robustBasin₂ (c j) δ ε i) : (recordMacro c).toFun (sigmaMove f g x) = (recordMacro c).toFun x

★★ The macrostate of #102 is preserved under a move of Σ, stated on recordMacro.

The measure of the two bands

theorem CSD.RecordLayer.measure_lowerBand_le {N : ℕ} (c : ContextField N) (ε : ℝ) (i : Fin N) (p : LF4.CPN N) : (epistemicMeasure p) (lowerBand c ε i) ≤ ENNReal.ofReal ε

The lower band is small: its slice over the preparation is the first ε of one arc.

theorem CSD.RecordLayer.measure_robustBasin₂_ge {N : ℕ} (c : ContextField N) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (i : Fin N) (p : LF4.CPN N) : ENNReal.ofReal (c.rate p i - (δ + 2 * ε)) ≤ (epistemicMeasure p) (robustBasin₂ c δ ε i)

★★ Robustness is still controlled by the Born weight. The two-sided robust interior of the basin of i has epistemic measure at least rate p i − (δ + 2ε): a record of large Born weight survives a move whose write and whose arc displacement are both small compared with its weight, and a cell of weight below δ + 2ε is granted nothing.

The microstates a move can relabel

noncomputable def CSD.RecordLayer.unstableSet₂ {N : ℕ} (c : ContextField N) (δ ε : ℝ) : Set (LF4.KSigma N)

The microstates a move of size (δ, ε) can relabel, for one context: those outside every basin (a null set) and those in either boundary band.

Equations

• CSD.RecordLayer.unstableSet₂ c δ ε = ((⋃ (i : Fin N), CSD.RecordLayer.globalBasin c i)ᶜ ∪ ⋃ (i : Fin N), CSD.RecordLayer.lowerBand c ε i) ∪ ⋃ (i : Fin N), CSD.RecordLayer.edgeBand c (δ + ε) i

theorem CSD.RecordLayer.exists_robustBasin₂_of_notMem_unstableSet₂ {N : ℕ} (c : ContextField N) (δ ε : ℝ) {x : LF4.KSigma N} (hx : x ∉ unstableSet₂ c δ ε) : ∃ (i : Fin N), x ∈ robustBasin₂ c δ ε i

theorem CSD.RecordLayer.measure_unstableSet₂_le {N : ℕ} (c : ContextField N) {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (p : LF4.CPN N) : (epistemicMeasure p) (unstableSet₂ c δ ε) ≤ ↑N * ENNReal.ofReal (δ + 2 * ε)

One context's unstable set has measure at most N · (δ + 2ε): two bands per outcome, plus the null set where no basin contains the microstate.

Quantitative stability under a move of Σ

theorem CSD.RecordLayer.measure_recordString_ne_sigmaMove_le {N k : ℕ} (c : Fin k → ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hg : ∀ (q : LF4.CPN N), g q ∈ Set.Icc 0 δ) (harc : ∀ (j : Fin k) (q : LF4.CPN N), ArcShift (c j) ε q (f q)) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | recordString c (sigmaMove f g x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal (δ + 2 * ε))

★★★ Quantitative stability of record macrostates under a move of Σ. The microstates whose record string a move changes have epistemic measure at most k · N · (δ + 2ε), where δ bounds the record write and ε bounds the travel of the arcs. At ε = 0 this is #103's bound; the extra 2ε is the price of letting the base move, and it is two-sided because both endpoints travel.

theorem CSD.RecordLayer.measure_recordString_ne_sigmaMove_rate_le {N k : ℕ} (c : Fin k → ContextField N) {f : LF4.CPN N → LF4.CPN N} {g : LF4.CPN N → ℝ} {δ η : ℝ} (hδ : 0 ≤ δ) (hη : 0 ≤ η) (hg : ∀ (q : LF4.CPN N), g q ∈ Set.Icc 0 δ) (hrate : ∀ (j : Fin k) (q : LF4.CPN N) (i : Fin N), |(c j).rate (f q) i - (c j).rate q i| ≤ η) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | recordString c (sigmaMove f g x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal (δ + 2 * ((↑N + 1) * η)))

★★ The same bound in terms of a modulus of continuity on the rate field. Rates within η coordinatewise put the arcs within (N+1)·η, so the relabelled set has measure at most k · N · (δ + 2(N+1)η). ⚠️ Note the second factor of N: for a large alphabet the rate field has to be uniformly close, not merely close.

theorem CSD.RecordLayer.measure_exists_recordString_ne_flow_le {N k : ℕ} (c : Fin k → ContextField N) (F : ℝ → LF4.CPN N → LF4.CPN N) (G : ℝ → LF4.CPN N → ℝ) {T δ ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hG : ∀ s ∈ Set.Icc 0 T, ∀ (q : LF4.CPN N), G s q ∈ Set.Icc 0 δ) (harc : ∀ s ∈ Set.Icc 0 T, ∀ (j : Fin k) (q : LF4.CPN N), ArcShift (c j) ε q (F s q)) (p : LF4.CPN N) : (epistemicMeasure p) {x : LF4.KSigma N | ∃ s ∈ Set.Icc 0 T, recordString c (sigmaMove (F s) (G s) x) ≠ recordString c x} ≤ ↑k * (↑N * ENNReal.ofReal (δ + 2 * ε))

★★★ One exceptional set serves a whole flow. For a one-parameter family of moves whose write stays in [0, δ] and whose arcs stay within ε over the horizon [0, T], the record string survives the entire horizon outside a set of measure k · N · (δ + 2ε) — the same set, because the robust interior does not depend on the parameter. This is #103's drift corollary once the base is allowed to move, and it needs no new argument. ⚠️ F s is an arbitrary measurable motion of the base: no group law, no invertibility and no generator is assumed, so "flow" names the shape, not a structure.