Extend affine finite-symbol sufficiency to degree boxes - #301

Merged

PerAlexandersson merged 83 commits into

mainfrom

codex-degreebox297

Aug 5, 2026

Commits on Aug 3, 2026

feat: prove polarization diagonal reconstruction
PerAlexandersson
committed
db5d5be
Package polarization in degree box
PerAlexandersson
committed
d6b6b20
Define diagonal polarization projection
PerAlexandersson
committed
1289666
Bound degree of diagonal projection
PerAlexandersson
committed
5e8c505
Restrict diagonal projection to degree boxes
PerAlexandersson
committed
003c6bb
Deduplicate unique equivalence degree proof
PerAlexandersson
committed
0226016
Define linear source polarization map
PerAlexandersson
committed
734df98
Define source-polarized degree-box operator
PerAlexandersson
committed
d9eb16d
Hide polarization linearity helpers
PerAlexandersson
committed
6fdc02b
Specialize polarization degree equivalence
PerAlexandersson
committed
5c8391c
Normalize multiaffine symbol coefficients
PerAlexandersson
committed
33d0be6
Evaluate diagonal projection on basis monomials
PerAlexandersson
committed
aaee7e3
Inline diagonal monomial calculation
PerAlexandersson
committed
b016190
Lift polarized operators on basis monomials
PerAlexandersson
committed
68cfa13
Reindex multiaffine exponents by support
PerAlexandersson
committed
ba13770
Golf zero-one exponent normalization
PerAlexandersson
committed
0b5c6b7
Group multiaffine terms by total degree
PerAlexandersson
committed
8589704
Diagonalize complementary symbol monomials
PerAlexandersson
committed
ca03f25
Place complement degree lemma in Finsupp
PerAlexandersson
committed
e1e0ac4
Prepare source symbol reindexing
PerAlexandersson
committed
3086ae9
Prove source polarized symbol identity
PerAlexandersson
committed
4f93fa7
Prove symmetry of polarization
PerAlexandersson
committed
554e81a
Add full polynomial symmetrization
PerAlexandersson
committed
c4b2609
Generalize symmetrization API
PerAlexandersson
committed
eb4150c
Add partial polynomial symmetrization
PerAlexandersson
committed
b418259
Prove partial symmetrization V-form identities
PerAlexandersson
committed
91e54b8
add degree-box modules to root imports
PerAlexandersson
committed
d8ab820
add bivariate quotient boundary identities
PerAlexandersson
committed
1278c75
add bivariate quotient positivity bridge
PerAlexandersson
committed
b6a3790
deduplicate symmetric bivariate proofs
PerAlexandersson
committed
6a3b329
formalize bivariate solve-for-variable step
PerAlexandersson
committed
8dba4c6
derive bivariate nonvanishing from quotient positivity
PerAlexandersson
committed
c3d8a0b
define second bivariate form by symmetry
PerAlexandersson
committed
24ed20a
bridge bivariate quotient criterion to stability
PerAlexandersson
committed
b08fdf1
derive weak quotient positivity from stability
PerAlexandersson
committed
68bfea4
golf bivariate weak converse proof
PerAlexandersson
committed
3397998
formalize constant bivariate quotient branch
PerAlexandersson
committed
1c34dec
add nonconstant bivariate quotient witness
PerAlexandersson
committed
f9a9215
deduplicate quotient denominator proofs
PerAlexandersson
committed
8862136
add analytic upper-half-plane strictness lemma
PerAlexandersson
committed
a3e25db
Merge remote-tracking branch 'origin/main' into codex-degreebox297
PerAlexandersson
committed
5936067
import upstream iterated derivative tactic modules
PerAlexandersson
committed
ae59cde
add bivariate quotient local nonconstancy
PerAlexandersson
committed
aace948
Repair degree-box comparator blockers
PerAlexandersson
committed
782d918
Repair finite-symbol dependency imports
PerAlexandersson
committed
6e2df3d
fix: repair degree-box comparator build
PerAlexandersson
committed
e1e161d
fix: use owning stability and index APIs
PerAlexandersson
committed
1ba62e1
chore: update finite-symbol vars API
PerAlexandersson
committed
78b55b9
feat: define source-block polarization
PerAlexandersson
committed
3ee82f6
feat: extract source-block coefficients
PerAlexandersson
committed
d4b6344
golf: use canonical degree-box equivalence
PerAlexandersson
committed
7d83d94
feat: isolate normalized source coefficient
PerAlexandersson
committed
c4a9708
feat: compute finite-symbol source coefficient
PerAlexandersson
committed
0651a2b
Document source polarization definition
PerAlexandersson
committed
4a48e77
Expand lifted algebraic symbol before diagonalization
PerAlexandersson
committed
0ad2c9d
Identify multiaffine complementary supports
PerAlexandersson
committed
51f2223
Repair degree-box polarization infrastructure
PerAlexandersson
committed
ca95ee9
Prove source-polarized symbol identity
PerAlexandersson
committed
69f33bd
Clean up degree-box proof scaffolding
PerAlexandersson
committed
bb092a5
Bound polar derivative degree
PerAlexandersson
committed
8fc0d73
Generalize polar derivative root containment
PerAlexandersson
committed
c958eb8
Generalize Grace lower-half degree bound
PerAlexandersson
committed
a843543
Golf bounded Grace proof plumbing
PerAlexandersson
committed
2367643
Generalize polarization stability to bounded degree
PerAlexandersson
committed
ff4c824
Commute source polarization with specialization
PerAlexandersson
committed
6607b5b
Golf specialization bridge plumbing
PerAlexandersson
committed
72615fb
Bound source degree after specialization
PerAlexandersson
committed
717ad29
Fix specialization degree proof arguments
PerAlexandersson
committed
096a3f3
Golf specialization degree bound
PerAlexandersson
committed
52e4093
Preserve stability under source polarization
PerAlexandersson
committed
8e60f2e
Bound algebraic symbol source degree
PerAlexandersson
committed
5b7fd6a
Deduplicate algebraic symbol degree bounds
PerAlexandersson
committed
9b5367f
Transfer finite symbol stability through polarization
PerAlexandersson
committed
f9e539f
Document Jensen backend obstruction
PerAlexandersson
committed
fe13bc2
Clean up finite symbol documentation
PerAlexandersson
committed
643e4aa
Document PF-specific Jensen source gap
PerAlexandersson
committed
f18c2fe
Fix degree-box polarization elaboration
PerAlexandersson
committed
647cf8a
Close source specialization homomorphism goals
PerAlexandersson
committed
f8d2c81

Commits on Aug 4, 2026

Commits on Aug 5, 2026

Merge remote-tracking branch 'origin/main' into codex-degreebox297
PerAlexandersson
committed
11b7867