I find this provides a visualization that is likely to be significantly more
intuitive for others. It even holds when the matrix is not
rectangular (yes, I know, it's not really a matrix then), so long as all
matrices share the same respective K_j.
This uses the same variable subscript on \equiv itself to define the symbol,
rather than the previous symbol which looked like equiv rotated, but also
looked too much like a turnstile used for "infer", a metalanguage construct
that is not appropriate here. It kept bothering me.
This represents the old cmatch system (which is in use today, but the
classification system has since been rewritten, though it has not yet been
merged). It was my attempt over a decade ago to reason about how this
system ought to work.
I think it's fair to say that this is absolute insanity and that the new
formulation is significantly better.
I removed this when I added concmath, thinking that it would include it for
me, and apparently I never re-added it after realizing that it didn't.
I'm a big fan of the typography of Concrete Mathematics.
The subscript of the matrix family adds too much vertical space. This
offsets that to restore it to about what it otherwise would be, since the
second subscript does not get in the way.
This was originally going to be used to define @yields for the classifier,
but I took a very different approach which doesn't require reasoning about
the system in terms of recursion.
This defines @as and @yields, but does not yet define matches formally.
It's also missing index entries, which I'll take the time to add after I'm
sure things are staying as they are.
This was quite a bit of work, and the approach I took is different than I
originally expected, so Section 0 can use some cleanup.
There is more to come from here.
This is going to evolve a great deal, and note that the yield definition is
completely absent.
It may be time to switch to natural deduction (Gentzen-style).
That macro previously expanded into \Classify, but that was undone before
committing to make it clear when one is referring to a variable vs. a
classification as a definition.
This will be used as an IR of sorts to eliminate the XML, which will be far
too verbose to use in proofs. It also allows us to attach behavior to the
operator, which will end up defining two values for @as and @yields.
The previously-existing notation for this has been removed. These will be
updated soon to account for vectors and matrices, but until then, this is
simply nonsense.
Mike Gerwitz