Basic theory of segments #
This file develops the theory of the segments defined in
Phonology/Segmental/Defs.lean. Natural-class membership is just the bundle order
— a pattern p matches s exactly when p ≤ s ([Shi86]; [Car92])
— so the results here are about the feature-change operations and the injectivity
of the Parker sonority ranking.
Main results #
Segment.setFeature_hasValue&c. — the feature-change operations act as specified.Sonority.Class.parkerRank_injective— the Parker scale ranks classes distinctly.
Effect on the modified feature #
@[simp]
theorem
Phonology.Segment.setFeature_hasValue
(s : Segment)
(f : Feature)
(v : Bool)
:
(s.setFeature f v).HasValue f v
theorem
Phonology.Segment.fillFromContext_apply_self_of_unspecified
(s : Segment)
{f : Feature}
(h : s.Unspecified f)
(ctx : Segment)
:
s.fillFromContext f ctx f = ctx f
theorem
Phonology.Segment.fillFromContext_apply_self_of_specified
(s : Segment)
{f : Feature}
{w : Bool}
(h : s.HasValue f w)
(ctx : Segment)
:
s.fillFromContext f ctx f = some w
Value preserved on other features #
@[simp]
theorem
Phonology.Segment.setFeature_apply_of_ne
(s : Segment)
{f g : Feature}
(h : f ≠ g)
(v : Bool)
:
s.setFeature f v g = s g
@[simp]
theorem
Phonology.Segment.fillFromContext_apply_of_ne
(s : Segment)
{f g : Feature}
(h : f ≠ g)
(ctx : Segment)
:
s.fillFromContext f ctx g = s g
Sonority #
The eight Parker classes receive distinct ranks: parkerRank is injective
([Par02]). The ranking is Parker's reversible default, so this is the
faithful invariant — no fixed order on Sonority.Class is implied.