Register: the terracing realization of [raised]

The syntagmatic reading of [raised] ([snider-1999], [lionnet-2025]): each [-raised] node lowers the register for everything that follows and each [+raised] node raises it, so a node sequence is realized as the running sum of its shifts from a baseline — terracing, as in the register-only systems of Drubea and Numèè and in the catathesis of Japanese and English intonation ([BP86]).

Main definitions

• TRN.pitchEffect — the shift a node contributes.
• realizePitch — the pitch levels of a sequence from a baseline, the running sums (List.scanl); pitchDeltas, the same from 0.

Main results

• realizePitch_eq_pitchDeltas_shift — a baseline only shifts the deltas.
• realizePitch_mono — realization is monotone in the baseline and, pointwise, in the shifts: the basis of catathesis blocking.

def Tone.TRN.pitchEffect (t : TRN) : ℤ

The register shift a node contributes: [-raised] lowers, [+raised] raises, an unspecified [raised] is inert.

Equations

• t.pitchEffect = match t.raised with | none => 0 | some false => -1 | some true => 1

def Tone.realizePitch (level : ℤ) (ts : List TRN) : List ℤ

Terracing: the pitch levels of a node sequence from a baseline, each shift cumulative — the running sums of the shifts.

Equations

• Tone.realizePitch level ts = (List.scanl (fun (x1 x2 : ℤ) => x1 + x2) level (List.map Tone.TRN.pitchEffect ts)).tail

@[simp]

theorem Tone.realizePitch_nil (level : ℤ) : realizePitch level [] = []

@[simp]

theorem Tone.realizePitch_cons (level : ℤ) (t : TRN) (rest : List TRN) : realizePitch level (t :: rest) = (level + t.pitchEffect) :: realizePitch (level + t.pitchEffect) rest

@[simp]

theorem Tone.length_realizePitch (level : ℤ) (ts : List TRN) : (realizePitch level ts).length = ts.length

theorem Tone.realizePitch_append (level : ℤ) (ts us : List TRN) : realizePitch level (ts ++ us) = realizePitch level ts ++ realizePitch (level + (List.map TRN.pitchEffect ts).sum) us

A sequence realizes piecewise: the second part continues from the register the first part leaves.

def Tone.pitchDeltas (ts : List TRN) : List ℤ

The register shifts from the start: no privileged pitch, only the differences.

Equations

• Tone.pitchDeltas ts = Tone.realizePitch 0 ts

theorem Tone.realizePitch_eq_pitchDeltas_shift (level : ℤ) (ts : List TRN) : realizePitch level ts = List.map (fun (x : ℤ) => x + level) (pitchDeltas ts)

A baseline only shifts the deltas.

theorem Tone.realizePitch_mono {ts₁ ts₂ : List TRN} (hts : List.Forall₂ (Function.onFun (fun (x1 x2 : ℤ) => x1 ≤ x2) TRN.pitchEffect) ts₁ ts₂) {n m : ℤ} (hnm : n ≤ m) : List.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (realizePitch n ts₁) (realizePitch m ts₂)

Monotonicity: pointwise lower shifts and a lower baseline give pointwise lower pitch. Structural basis of catathesis blocking ([BP86]): a register reset at a phrase boundary leaves everything after it higher than continued compression would.

theorem Tone.realizePitch_baseline_mono (ts : List TRN) {n m : ℤ} (h : n ≤ m) : List.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (realizePitch n ts) (realizePitch m ts)

A higher baseline gives pointwise higher pitch for a fixed sequence.