Commit e7aa241
WIP vcl-ut PR-1: Composition diagnostic — mutual-wrap + structural fixes
Composition.idr forward-ref noise cleared (mutual wrap 242-727) +
faithful fixes: appendNilRight/mapFstAppend binders, joinWhere moved,
allFieldsBoundSubset relevant implicits, elemAppendSplit binders.
Exposed the IRREDUCIBLE debt (18 errs, NOT mechanical): composeJoin/
joinLinear non-covering (real definitional gap → cascades to l6-l10);
fst ambiguity (global); compositionPreservation still MkL4 ...
AllParameterised (#20 deleted that ctor — L4 never integrated in
corpus); noRawUserInputCompose fails in situ. These = the L1/L6-L10
composition theorems #20's VERIFICATION-STANCE already lists OWED.
NOT a mechanical tail — needs proof reconstruction or honest OWED scoping.
Refs hyperpolymath/standards#124.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent df1231c commit e7aa241
1 file changed
Lines changed: 487 additions & 483 deletions
0 commit comments