Prove Liu cross-owned gaps by bounded continuity - #295

Draft

PerAlexandersson wants to merge 76 commits into

mainfrom

codex-liu64-resume

Commits on Aug 2, 2026

Add reflected half-line root count transport
PerAlexandersson
committed
3130373
Add reflected root endpoint transport
PerAlexandersson
committed
dc5ea25
Transport bounded root counts through degree drops
PerAlexandersson
committed
7be5d9f
Translate bounded root count constancy
PerAlexandersson
committed
2547bf0
Prove Liu cross-owned gaps by bounded continuity
PerAlexandersson
committed
a64e2cb
Deduplicate Liu bounded-continuity proof
PerAlexandersson
committed
e0cea04
Centralize bounded interval degree plumbing
PerAlexandersson
committed
c1591c9
Connect Liu bounded continuity to finite descent
PerAlexandersson
committed
1ba0438
Preserve compatibility under derivative regularization
PerAlexandersson
committed
a1f92d9
Centralize derivative regularizer linearity
PerAlexandersson
committed
a33ab40
Match roots under small derivative shifts
PerAlexandersson
committed
e968692
Preserve no-common roots under small shifts
PerAlexandersson
committed
8907f1c
Centralize multiset matching eliminators
PerAlexandersson
committed
5e00cea
Add finite derivative shift sequences
PerAlexandersson
committed
7ed5364
Regularize Liu endpoints by bounded shifts
PerAlexandersson
committed
f4be700
Golf derivative shift root matching
PerAlexandersson
committed
439c036
Track roots through bounded Liu regularization
PerAlexandersson
committed
fe74125
Stabilize Liu root counts under matching
PerAlexandersson
committed
8ae49d8
Golf multiset relation diagonal
PerAlexandersson
committed
2fa6bde
Match sorted roots through multiset relations
PerAlexandersson
committed
3c480d7
Match roots after deleting largest factors
PerAlexandersson
committed
7c91070
Golf sorted root matching wrapper
PerAlexandersson
committed
4305d9a
Close ordered inequalities under root matching
PerAlexandersson
committed
3a1615a
Close same-degree Liu root counts
PerAlexandersson
committed
9bfa6fb
Golf root count closure length bounds
PerAlexandersson
committed
fd2cbf5
Add successor root crossing converse
PerAlexandersson
committed
a7f16c4
Close successor root count compatibility
PerAlexandersson
committed
c7ea7e4
Golf successor root count wrapper
PerAlexandersson
committed
6efa1a6
Bridge descending root sequence to sorted roots
PerAlexandersson
committed
04c609d
Close compatible root approximants
PerAlexandersson
committed
2f08dc2
Golf compatible approximant closure
PerAlexandersson
committed
514266d
Close equal-degree left root-count branches
PerAlexandersson
committed
2158cb6
Close successor-degree left root-count branches
PerAlexandersson
committed
a9ecb09
Golf fixed left branch closure
PerAlexandersson
committed
4aaf4f0
Close two-step-degree left root-count branches
PerAlexandersson
committed
2e32688
Dispatch fixed left branch closure by degree
PerAlexandersson
committed
9c96321
Golf fixed left branch dispatcher
PerAlexandersson
committed
4bbcb1f
Close fixed right root-count branches
PerAlexandersson
committed
7e8863a
Close disjunctive Liu root-count branches
PerAlexandersson
committed
8a2b5d0
Deduplicate Liu root relation widening
PerAlexandersson
committed
fa72364
Prove Liu nonconstant forward implication
PerAlexandersson
committed
8ca681d
Assemble Liu no-common nonconstant equivalence
PerAlexandersson
committed
15e5818
Golf Liu regularization assembly
PerAlexandersson
committed
2e0240e
Prove corrected Liu common-root equivalences
PerAlexandersson
committed
e93c453
Refute false Liu nonconstant branch statement
PerAlexandersson
committed
1a3cba5
Reuse low-degree compatibility in Liu counterexample
PerAlexandersson
committed
6c25cf7
Prove Liu no-common degree gap
PerAlexandersson
committed
dbe2e41
Prove odd-degree downward shift obstruction
PerAlexandersson
committed
732b3a1
Golf odd-degree shift nonzeroness
PerAlexandersson
committed
cfb8590
Prove nonnegative penultimate critical value
PerAlexandersson
committed
790605f
Prove downward shift obstruction
PerAlexandersson
committed
af30c16
Golf downward shift positivity proof
PerAlexandersson
committed
e16919d
Prove constant endpoint degree bound
PerAlexandersson
committed
a558145
Package constant degree endpoints
PerAlexandersson
committed
ac1b9ae
Deduplicate constant endpoint bound
PerAlexandersson
committed
872eb8a
Prove Liu Corollary 2.2
PerAlexandersson
committed
18b674e
Remove duplicate multiset relation helpers
PerAlexandersson
committed
b9b6b9a
Restore multiset relation infrastructure
PerAlexandersson
committed
67a654a

Commits on Aug 3, 2026

Merge remote-tracking branch 'origin/main' into codex-liu64-resume
PerAlexandersson
committed
0a593be
Repair Liu constant-shift proof block
PerAlexandersson
committed
c07bfc1
chore: remove redundant derivative-shift simp argument
PerAlexandersson
committed
c2702d6
fix: import multiset strong induction
PerAlexandersson
committed
f2b58f3
fix: avoid root-order reverse-index timeout
PerAlexandersson
committed
e90d393
refactor: simplify root-order length facts
PerAlexandersson
committed
2f263fc
fix: expose derivative-shift declarations
PerAlexandersson
committed
b8f3246
fix: normalize derivative-shift root transport
PerAlexandersson
committed
7da47c4
refactor: simplify derivative-shift tail positivity
PerAlexandersson
committed
0a49c23
Repair multiset relation eliminators
PerAlexandersson
committed
b053688
Golf multiset relation composition
PerAlexandersson
committed
9808264
Repair Liu comparator dependencies
PerAlexandersson
committed
198878a
Repair Liu comparator regressions
PerAlexandersson
committed
bcb80a8
fix multiset sorted relation induction
PerAlexandersson
committed
4cd3e0c
repair multiset sorted-tail reconstruction
PerAlexandersson
committed
93b0bb8
Repair Liu root matching CI failures
PerAlexandersson
committed
3b416cb
Qualify Liu sorted-root helper
PerAlexandersson
committed
b1e9e07
Repair Liu root-count closure APIs
PerAlexandersson
committed
faaf41e