Ternary scale theorems: Difference between revisions

Inthar (talk | contribs)
Inthar (talk | contribs)
 
(13 intermediate revisions by the same user not shown)
Line 84: Line 84:
By part (2), we have that ''s'' has step signature {{nowrap|''a'''''X''' ''b'''''Y''' ''b'''''Z'''}}, ''a'' odd. By part (4), we have that {{nowrap|''T''('''X''', '''W''') {{=}} ''s''('''X''', '''W''', '''W''')}} is a MOS scale ''a'''''X'''2''b'''''W'''. If {{nowrap|''b'' {{=}} 1}}, there's nothing to prove, so assume {{nowrap|''b'' > 1}}.
By part (2), we have that ''s'' has step signature {{nowrap|''a'''''X''' ''b'''''Y''' ''b'''''Z'''}}, ''a'' odd. By part (4), we have that {{nowrap|''T''('''X''', '''W''') {{=}} ''s''('''X''', '''W''', '''W''')}} is a MOS scale ''a'''''X'''2''b'''''W'''. If {{nowrap|''b'' {{=}} 1}}, there's nothing to prove, so assume {{nowrap|''b'' > 1}}.


Consider the two generators in the GS of ''s'', which are lifts of the generator {{nowrap|''i'''''X''' + ''j'''''W'''}} of ''T''('''X''', '''W'''), where {{nowrap|gcd(''j'', 2''k'') {{=}} 1}}. Assume, possibly after inverting the generator, that the imperfect generator of ''T'' has {{nowrap|''j'' − 1}} '''W'''s and the perfect generator has ''j'' '''W'''s.
Consider the two generators in the GS of ''s'', which are lifts of the generator {{nowrap|''i'''''X''' + ''j'''''W'''}} of ''T''('''X''', '''W'''), where {{nowrap|gcd(''j'', 2''b'') {{=}} 1}}. Assume, possibly after inverting the generator, that the imperfect generator of ''T'' has {{nowrap|''j'' − 1}} '''W'''s and the perfect generator has ''j'' '''W'''s.


'''Claim 1''': Deleting '''X'''s from the generator subwords of ''s'' gives every ''j''-step subword in the scale ''E''<sub>X</sub>(''s'')('''Y''',&nbsp;'''Z'''), the scale word obtained by deleting all '''X''''s from ''s''. These ''j''-step subwords are adjacent and alternating under the ordering induced by the AGS stack.
'''Claim 1''': Deleting '''X'''s from the generator subwords of ''s'' gives every ''j''-step subword in the scale ''E''<sub>X</sub>(''s'')('''Y''',&nbsp;'''Z'''), the scale word obtained by deleting all '''X''''s from ''s''. These ''j''-step subwords are adjacent and alternating under the ordering induced by the AGS stack.
Line 103: Line 103:
* C.1. Importantly, deleting '''X''''s gives windows of length ''j'', such that when you project adjacent lifted generators (by deleting '''X''''s) to the binary necklace {{nowrap|''U'' :{{=}} ''E''<sub>'''X'''</sub>(''s'')('''Y''', '''Z''')}}, the resulting ''j''-step windows in ''U'' are adjacent and do not overlap.
* C.1. Importantly, deleting '''X''''s gives windows of length ''j'', such that when you project adjacent lifted generators (by deleting '''X''''s) to the binary necklace {{nowrap|''U'' :{{=}} ''E''<sub>'''X'''</sub>(''s'')('''Y''', '''Z''')}}, the resulting ''j''-step windows in ''U'' are adjacent and do not overlap.
* C.2. Moreover, for every ''j''-step window {{nowrap|''U''[''q'' : ''q'' + ''j'']}}, there exists an {{nowrap|(''i'' + ''j'')-step}} window {{nowrap|''s''[''r'' : ''r'' + ''i'' + ''j'']}} such that {{nowrap|''s''[''r'']}} is the non-'''X''' that corresponds to {{nowrap|''U''[''q'']}} under step deletion. Since by subclaim A, the unique imperfect {{nowrap|(''i'' + ''j'')-step}} window in ''s'' begins in an '''X''', we know that {{nowrap|''s''[''r'' : ''r'' + ''i'' + ''j'']}} is perfect.
* C.2. Moreover, for every ''j''-step window {{nowrap|''U''[''q'' : ''q'' + ''j'']}}, there exists an {{nowrap|(''i'' + ''j'')-step}} window {{nowrap|''s''[''r'' : ''r'' + ''i'' + ''j'']}} such that {{nowrap|''s''[''r'']}} is the non-'''X''' that corresponds to {{nowrap|''U''[''q'']}} under step deletion. Since by subclaim A, the unique imperfect {{nowrap|(''i'' + ''j'')-step}} window in ''s'' begins in an '''X''', we know that {{nowrap|''s''[''r'' : ''r'' + ''i'' + ''j'']}} is perfect.
* C.3. We need only stack {{nowrap|2''b'' &le; ''n'' &minus; 1}} generators (to get {{nowrap|2''b''-many}} ''j''-step windows downstairs) to witness the alternation. Under the ordering induced by this stacking, the 1st ''j''-step subword of ''U'' and the {{nowrap|2''b''-th}} ''j''-step window differ due to parity. Since {{nowrap|gcd(''j'', 2''b'') {{=}} 1}}, this visits every note of ''U''.
* C.3. We need only stack {{nowrap|2''b'' &le; ''n'' &minus; 1}} generators (to get {{nowrap|2''b''-many}} ''j''-step windows downstairs) to witness the alternation. Under the ordering induced by this stacking, the 1st ''j''-step subword of ''U'' and the last ({{nowrap|2''b''-th}}) ''j''-step window differ due to parity. Since {{nowrap|gcd(''j'', 2''b'') {{=}} 1}}, this visits every note of ''U''.


'''Claim 2''': If a binary necklace ''U'' has ''b'' '''Y'''s and ''b'' '''Z'''s, {{nowrap|gcd(''j'', 2''b'') {{=}} 1}}, and consecutively stacked ''j''-steps in ''U'' occur in 2 alternating sizes, then {{nowrap|''U'' {{=}} ('''YZ''')<sup>''b''</sup>}}.
'''Claim 2''': If a binary necklace ''U'' has ''b'' '''Y'''s and ''b'' '''Z'''s, {{nowrap|gcd(''j'', 2''b'') {{=}} 1}}, and consecutively stacked ''j''-steps in ''U'' occur in 2 alternating sizes, then {{nowrap|''U'' {{=}} ('''YZ''')<sup>''b''</sup>}}.
Line 171: Line 171:
# the stack has only copies of '''Q''' and '''R'''; or
# the stack has only copies of '''Q''' and '''R'''; or
# the stack has one '''T''' and does not contain any '''R''' (since it's more than {{nowrap|''f'' − 1}} generators away).
# the stack has one '''T''' and does not contain any '''R''' (since it's more than {{nowrap|''f'' − 1}} generators away).
These give exactly three distinct sizes for every interval class. Hence ''s'' is SV3.
These give exactly three distinct sizes for every interval class. Hence ''s'' is SV3. In this case a window stacking argument shows that the second type of ''fk''-step {{nowrap|((''f'' &minus; 1)''Q'' + ''T'')}} alternates with the first type {{nowrap|((''f'' &minus; 1)''Q'' + ''R'')}}, and ''fQ'' occurs only once, so ''s'' has generator sequence {{nowrap|GS((''f'' &minus; 1)''Q'' + ''T'', (''f'' &minus; 1)''Q'' + ''R'')}}. Since ''n'' is odd, ''s'' is odd-regular.
 
In this case ''s'' has two chains of '''Q''', one with {{floor|''n''/2}} notes and one offset by {{nowrap|'''Q'''<sup>(''f'' − 1)</sup>R}} with {{ceil|''n''/2}} notes. Every instance of Q must be a ''k''-step, since by ℤ-linear independence {{nowrap|'''Q''' {{=}} α'''a''' + β'''b''' + γ'''c'''}} is the only way to write '''Q''' in the basis {{nowrap|('''a''', '''b''', '''c''')}}; so ''s'' is well-formed with respect to '''Q'''. Thus ''s'' also satisfies the generator-offset property with generator '''Q'''.


'''Case 2:''' {{nowrap|μ &ge; {{ceil|''n''/2}}}}, i.e. Λ<sub>2</sub> has fewer β than β′.
'''Case 2:''' {{nowrap|μ &ge; {{ceil|''n''/2}}}}, i.e. Λ<sub>2</sub> has fewer β than β′.


Since Λ<sub>3</sub> has more β than β′, Λ<sub>2</sub> is {{floor|''n''/2}}β&nbsp;{{ceil|''n''/2}}β′, and Λ<sub>3</sub> is {{ceil|''n''/2}}γ&nbsp;{{floor|''n''/2}}γ′. There is a unique mode of {{ceil|''n''/2}}γ&nbsp;{{floor|''n''/2}}γ′ that both begins and ends with γ, namely γγ′γγ′…γγ′γ. Thus Λ<sub>2</sub> is ββ′ββ′…ββ′β′. It is now easy to see that if the number of ''k''-steps stacked is odd, then there are two sizes that do not contain '''T''' and one size that contains '''T'''; if the number of ''k''-steps stacked is even, then there is one size that does not contain '''T''' and two sizes that contain T. Hence ''s'' is SV3.
Since Λ<sub>3</sub> has more β than β′, Λ<sub>2</sub> is {{floor|''n''/2}}β&nbsp;{{ceil|''n''/2}}β′, and Λ<sub>3</sub> is {{ceil|''n''/2}}γ&nbsp;{{floor|''n''/2}}γ′. There is a unique mode of {{ceil|''n''/2}}γ&nbsp;{{floor|''n''/2}}γ′ that both begins and ends with γ, namely γγ′γγ′…γγ′γ. Thus Λ<sub>2</sub> is ββ′ββ′…ββ′β′. It is now easy to see that if the number of ''k''-steps stacked is odd, then there are two sizes that do not contain '''T''' and one size that contains '''T'''; if the number of ''k''-steps stacked is even, then there is one size that does not contain '''T''' and two sizes that contain ''T''. Hence ''s'' is SV3.


In this case we have {{nowrap|Σ {{=}} '''QRQR'''…'''QRT'''}}, and ''s'' is well-formed with respect to the generator {{nowrap|'''Q''' + '''R'''}}, thus ''s'' satisfies the generator-offset property. By Proposition 1, ''s'' is SV3.
In this case we have Σ = ''QRQR…QRT'', and ''s'' has generator sequence {{nowrap|GS(''Q'', ''R'').}} We thus have that ''s'' is odd-regular.


'''Case 3:''' {{nowrap|3 &le; μ &le; {{floor|''n''/2}}}}.
'''Case 3:''' {{nowrap|3 &le; μ &le; {{floor|''n''/2}}}}.
Line 253: Line 251:


=== Theorem 5.1 (Classification of ternary balanced scales) ===
=== Theorem 5.1 (Classification of ternary balanced scales) ===
# A primitive [[balanced]] ternary scale ''s'' is pairwise-MOS, and satisfies one of the following:
# A primitive [[balanced]] ternary scale ''s'' is pairwise-MOS; conversely, pairwise-MOS scales are balanced. Such a scale satisfies one of the following:
## '''sporadic balanced''': ''s'' is equivalent to '''XYXZXYX''', the ternary [[Fraenkel word]], with step signature 4'''X'''2'''Y'''1'''Z'''.
## '''sporadic balanced''': ''s'' is equivalent to '''XYXZXYX''', the ternary [[Fraenkel word]], with step signature 4'''X'''2'''Y'''1'''Z'''.
## '''odd-regular''': len(''s'') is odd, and ''s'' is equivalent to a word constructed from taking the brightest mode of the MOS ''c'''''X'''''b'''''Z''' with ''c'' even and {{nowrap|gcd(''c'', ''b'') {{=}} 1}}, and replacing every other '''X''' with '''Y'''. We assume {{nowrap|'''X''' &gt; '''Z'''}} when constructing the MOS. In particular, ''s'' has [[step signature]] ''a'''''X'''''a'''''Y'''''b'''''Z''' where ''b'' is odd (with {{nowrap|''a'' {{=}} ''c''/2}}).
## '''odd-regular''': len(''s'') is odd, and ''s'' is equivalent to a word constructed from taking the brightest mode of the MOS ''c'''''X'''''b'''''Z''' with ''c'' even and {{nowrap|gcd(''c'', ''b'') {{=}} 1}}, and replacing every other '''X''' with '''Y'''. We assume {{nowrap|'''X''' &gt; '''Z'''}} when constructing the MOS. In particular, ''s'' has [[step signature]] ''a'''''X'''''a'''''Y'''''b'''''Z''' where ''b'' is odd (with {{nowrap|''a'' {{=}} ''c''/2}}).
Line 264: Line 262:


==== Proof ====
==== Proof ====
For 5.1.1: We showed previously that the Fraenkel, odd-regular, and even-regular circular words are balanced. Thus it remains to show that (a) ternary balanced words are pairwise-MOS (b) if ''a'' > ''b'' > ''c'', then ''s'' is equivalent to the Fraenkel word (c) assuming ''a'' != ''b'' = ''c'' any ''s'' that is not odd-regular or even-regular is not balanced.
For 5.1.1: We showed previously that the Fraenkel, odd-regular, and even-regular circular words are balanced.
 
We will first prove that a balanced circular word is primitive iff the gcd of the step signature is 1. Proof sketch: let ''d'' be the gcd of the step signature. (''n''/''d'')-step multisets come in 1 size, namely the equave divided by ''d'', because if some letter count differs, then we get 3 values for this letter count for (''n''/''d'')-step multisets by the discrete IVT.
 
It remains to show that (a) ternary balanced words are pairwise-MOS (b) if ''a'' > ''b'' > ''c'', then ''s'' is equivalent to the Fraenkel word (c) assuming ''a'' != ''b'' = ''c'' any ''s'' that is not odd-regular or even-regular is not balanced.


(a) Let ''s'' be a ternary balanced word; then for any given letter '''y''' the number of '''y'''s in a subword of any given length ''L'' varies by at most 1. Thus the same is true when we count all non-'''y''' letters in any subword of length ''L''; thus when we equate '''x''' and '''z''', the count of the resulting letter in any subword of length ''L'' differs by 1. Being a binary balanced word is one characterization of the MOS property.
(a) Let ''s'' be a ternary balanced word; then for any given letter '''y''' the number of '''y'''s in a subword of any given length ''L'' varies by at most 1. Thus the same is true when we count all non-'''y''' letters in any subword of length ''L''; thus when we equate '''x''' and '''z''', the count of the resulting letter in any subword of length ''L'' differs by 1. Being a binary balanced word is one characterization of the MOS property.
Line 327: Line 329:
Write ''s''<sub>1</sub> for the scale word made from stacked 2-steps from the 0-degree, and let ''s''<sub>2</sub> be as follows:
Write ''s''<sub>1</sub> for the scale word made from stacked 2-steps from the 0-degree, and let ''s''<sub>2</sub> be as follows:
* In the singly even case, let ''s''<sub>2</sub> be the circular word of 2-steps starting at the (''n''/2)-degree. We know that they differ only by interchanging '''y''' and '''z''', hence that they have the same period. Hence both ''s''<sub>1</sub> and ''s''<sub>2</sub> are primitive.
* In the singly even case, let ''s''<sub>2</sub> be the circular word of 2-steps starting at the (''n''/2)-degree. We know that they differ only by interchanging '''y''' and '''z''', hence that they have the same period. Hence both ''s''<sub>1</sub> and ''s''<sub>2</sub> are primitive.
* In the doubly even case, start from the mode of ''s'' whose template MOS is the brightest mode. Let ''s''<sub>2</sub> be offset at a generator of the even-regular scale, which by Theorem 6 we choose to have the same interval class as a bright generator of the MOS ''a'''''x''' 2''k'''''X'''. This is what induces the equality of ''s''<sub>1</sub> and ''s''<sub>2</sub> (in particular, the two scales have the same period, thus they are both primitive): Let ''s''<sub>''t''</sub> be the period of the brightest mode of the template MOS, and let ''g'' be its bright generator class. Then the slice {{nowrap|''s''<sub>''t''</sub>[-''g'' +1 : 1]}} is the imperfect generator of the MOS. Now when we "darken" the mode by one generator, which is the difference between the template MOSes of ''s''<sub>1</sub> and ''s''<sub>2</sub>, we turn that slice into the bright generator, hence swapping ''s''<sub>''t''</sub>[-''g''] and ''s''<sub>''t''</sub>[-''g'' + 1]. Note that ''g'' must be odd since it generates a 2-period MOS. So (under 0-indexing) the first letter's index is even and the second letter's index is odd, which is what we want since the letters are within a stacked 2-step. While the generator might have to be higher by an (''n''/2)-step, that doesn't affect the parity since ''n''/2 is even.
* In the doubly even case, start from the mode of ''s'' whose template MOS is the brightest mode. Let ''s''<sub>2</sub> be offset at a generator of the even-regular scale, which we choose to have the same interval class as a bright generator of the MOS ''a'''''x''' 2''k'''''X'''. This is what induces the equality of ''s''<sub>1</sub> and ''s''<sub>2</sub> (in particular, the two scales have the same period, thus they are both primitive): Let ''s''<sub>''t''</sub> be the period of the brightest mode of the template MOS, and let ''g'' be its bright generator class. Then the slice {{nowrap|''s''<sub>''t''</sub>[-''g'' +1 : 1]}} is the imperfect generator of the MOS. Now when we "darken" the mode by one generator, which is the difference between the template MOSes of ''s''<sub>1</sub> and ''s''<sub>2</sub>, we turn that slice into the bright generator, hence swapping ''s''<sub>''t''</sub>[-''g''] and ''s''<sub>''t''</sub>[-''g'' + 1]. Note that ''g'' must be odd since it generates a 2-period MOS. So (under 0-indexing) the first letter's index is even and the second letter's index is odd, which is what we want since the letters are within a stacked 2-step. While the generator might have to be higher by an (''n''/2)-step, that doesn't affect the parity since ''n''/2 is even.


We prove that ''s''<sub>1</sub> and ''s''<sub>2</sub> are MOS substitution scales with a filling MOS of period 2. The number the 2-step (1) occurs must be the same in both ''s''<sub>1</sub> and ''s''<sub>2</sub>. The word of stacked 2-steps of the template MOS (which is of the form {{nowrap|''w''('''x''', '''X''', '''X''')''w''('''x''', '''X''', '''X''')}}), which is itself a MOS word, consists of letters (1) '''x''' + '''X''' and (2) 2'''X''' if more '''X''''s than '''x''''s, 2'''x''' if more '''x''''s than '''X''''s. The word of stacked 2-steps from our chosen offset is also this same MOS word. Thus it remains to handle the cases (1) and (2) above. IWhenever the letter '''x''' + '''X''' is encountered, the number of the last letters that are equated to '''X''' that are consumed is 1, which is odd. Whenever the other letter is encountered, that number is even (0 or 2). Hence (since ''n'' > 4) the letter 2'''X''' resp. 2'''x''' serves as the non-slot letter, and the letters ('''x''' + '''X''') serve as the slot letters where a 2-period filling MOS word (a repetition of {{nowrap|('''x'''+'''y''')('''x'''+'''z''')}}) is substituted.
We prove that ''s''<sub>1</sub> and ''s''<sub>2</sub> are MOS substitution scales with a filling MOS of period 2. The number the 2-step (1) occurs must be the same in both ''s''<sub>1</sub> and ''s''<sub>2</sub>. The word of stacked 2-steps of the template MOS (which is of the form {{nowrap|''w''('''x''', '''X''', '''X''')''w''('''x''', '''X''', '''X''')}}), which is itself a MOS word, consists of letters (1) '''x''' + '''X''' and (2) 2'''X''' if more '''X''''s than '''x''''s, 2'''x''' if more '''x''''s than '''X''''s. The word of stacked 2-steps from our chosen offset is also this same MOS word. Thus it remains to handle the cases (1) and (2) above. Whenever the letter '''x''' + '''X''' is encountered, the number of the last letters that are equated to '''X''' that are consumed is 1, which is odd. Whenever the other letter is encountered, that number is even (0 or 2). Hence (since ''n'' > 4) the letter 2'''X''' resp. 2'''x''' serves as the non-slot letter, and the letters ('''x''' + '''X''') serve as the slot letters where a 2-period filling MOS word (a repetition of {{nowrap|('''x'''+'''y''')('''x'''+'''z''')}}) is substituted.


Now we count the letters that occur in these MOS substitution words of 2-steps. Consider the chunk boundaries of the template MOS. For every boundary between chunks, there is one slot letter in the template MOS for ''s''<sub>1</sub> and one in the template MOS ''s''<sub>2</sub>, due to index parity. So it suffices that we have evenly many boundaries between (nonempty) chunks. Equivalently, we have to prove that there are evenly many steps of the step size that occurs less frequently in the template MOS ''a'''''x''' 2''k'''''X''', which is true by assumption (''a'' and 2''k'' are both even).
Now we count the letters that occur in these MOS substitution words of 2-steps. Consider the chunk boundaries of the template MOS. For every boundary between chunks, there is one slot letter in the template MOS for ''s''<sub>1</sub> and one in the template MOS ''s''<sub>2</sub>, due to index parity. So it suffices that we have evenly many boundaries between (nonempty) chunks. Equivalently, we have to prove that there are evenly many steps of the step size that occurs less frequently in the template MOS ''a'''''x''' 2''k'''''X''', which is true by assumption (''a'' and 2''k'' are both even).
* In the singly even case, since there are evenly many slot letters in both ''s''<sub>1</sub> and ''s''<sub>2</sub>, there are oddly many non-slot letters in both. Since ''s''<sub>1</sub> and ''s''<sub>2</sub> differ by interchanging '''y''' and '''z''', they have "opposite" filling letters, '''x''' + '''y''' being the opposite of '''x''' + '''z'''. This makes ''s''<sub>1</sub> and ''s''<sub>2</sub> opposite chiralities of an odd-regular MV3 scale.
* In the singly even case, since there are evenly many slot letters in both ''s''<sub>1</sub> and ''s''<sub>2</sub>, there are oddly many non-slot letters in both. Since ''s''<sub>1</sub> and ''s''<sub>2</sub> differ by interchanging '''y''' and '''z''', they have "opposite" filling letters, '''x''' + '''y''' being the opposite of '''x''' + '''z'''. This makes ''s''<sub>1</sub> and ''s''<sub>2</sub> opposite chiralities of an odd-regular MV3 scale.
* In the doubly even case, the number of non-slot letters in ''s''<sub>1</sub> and ''s''<sub>2</sub> is even, and we have a filling MOS of period 2. Since ''s''<sub>1</sub> and ''s''<sub>2</sub> are both primitive, they are both even-regular scales. {{Qed}}
* In the doubly even case, the number of non-slot letters in ''s''<sub>1</sub> and ''s''<sub>2</sub> is even, and we have a filling MOS of period 2. Since ''s''<sub>1</sub> and ''s''<sub>2</sub> are both primitive, they are both even-regular scales. {{Qed}}
== Theorem 7 (Ternary parallelogram scales are MOS substitution) ==
:''Main article: [[Ternary parallelogram scales are MOS substitution]]''
Ternary parallelogram scale words are [[MOS substitution]] scale words, where the period count of the template MOS is the number of rows of the parallelogram parallel to the unique step size parallel to a side of the parallelogram.


== Open problems ==
== Open problems ==
Line 353: Line 360:
# In the theory of MOS, there is a second [[MOS Scale Family Tree|scale tree]] that is less frequently talked about, which Erv Wilson calls the "Rabbit Sequence" ([http://www.anaphoria.com/RabbitSequence.pdf Erv Wilson's original version], [https://mikebattagliamusic.com/MOSTree/MOSTreeab.html interactive version 1], [https://mikebattagliamusic.com/MOSTree/MOSTreeLs.html interactive version 2]). This is a tree for which each MOS word has two children, depending on if the MOS is "soft" (with {{nowrap|L/s &lt; 2}}) or "hard" (with {{nowrap|L/s &gt; 2}}). For instance, LsLss has the two children LLsLLLs and ssLsssL. Does a similar scale plane exist for these generator-offset-MV3 scales?
# In the theory of MOS, there is a second [[MOS Scale Family Tree|scale tree]] that is less frequently talked about, which Erv Wilson calls the "Rabbit Sequence" ([http://www.anaphoria.com/RabbitSequence.pdf Erv Wilson's original version], [https://mikebattagliamusic.com/MOSTree/MOSTreeab.html interactive version 1], [https://mikebattagliamusic.com/MOSTree/MOSTreeLs.html interactive version 2]). This is a tree for which each MOS word has two children, depending on if the MOS is "soft" (with {{nowrap|L/s &lt; 2}}) or "hard" (with {{nowrap|L/s &gt; 2}}). For instance, LsLss has the two children LLsLLLs and ssLsssL. Does a similar scale plane exist for these generator-offset-MV3 scales?


== External links ==
* [https://github.com/turbofishcrow/scale-word-theorems Scale word theorems formalized in Lean 4 (WIP)]
[[Category:Math]]
[[Category:Math]]
[[Category:Rank-3 scales| ]]
[[Category:Rank-3 scales| ]]