Release v0.7.0

.agents/PLAN.md

@@ -8,16 +8,17 @@ Plancherel, relative Hamming distance, balancedness, restrictions, ANF, algebrai
 functions, and derivatives needed by CryptBoolean. FABL is the canonical owner of those shared APIs;
 this project imports them directly and adds only source-facing or cross-representation laws.
 
-The current Blueprint baseline contains 294 source-facing statement nodes: 291 formalized nodes
-associated with 1882 proved Lean declarations and 3 visibly open nodes, connected by 713 reviewed
+The current Blueprint baseline contains 317 source-facing statement nodes: 314 formalized nodes
+associated with 2158 proved Lean declarations and 3 visibly open nodes, connected by 772 reviewed
 dependency edges. Chapter 2 contributes 41 formalized nodes, 174 declarations, and 56 incoming
 edges. Chapter 3 contributes 7 formalized nodes, 32 declarations, and 19 incoming
 edges. Chapter 4 contributes 73 formalized nodes, 568 declarations, and 159 incoming edges. Chapter
 5 contributes 31 nodes (28 formalized and 3 open), 203 declarations, and 70 incoming edges. Chapter
 6 contributes 70 formalized nodes, 441 declarations, and 189 incoming edges. Chapter 7 contributes
 39 formalized nodes, 224 declarations, and 114 incoming edges. Chapter 8 contributes 14 formalized
 nodes, 131 declarations, and 42 incoming edges. Chapter 9 contributes 19 formalized nodes, 109
-declarations, and 64 incoming edges. These counts are a synchronized verification contract shared
+declarations, and 64 incoming edges. Chapter 10 contributes 23 formalized nodes,
+276 declarations, and 59 incoming edges. These counts are a synchronized verification contract shared
 by the inventories,
 Verso sources, `blueprint-verso/scripts/validate_manifest.py`, and `AGENTS.md`.
 
@@ -80,13 +81,14 @@ tooling pipeline runs, and no local filesystem path appears in package metadata.
 
 ## Phase 1 - Complete Carlet inventory
 
-Status: in progress. Chapters 2--9 are source-reviewed and Blueprint-synchronized under
+Status: complete. Chapters 2--10 are source-reviewed and Blueprint-synchronized under
 `.agents/inventory/`. Chapter 6 has 70 promoted mathematical statements and 18 additional
 source-recovery records; Chapter 7 has 39 promoted mathematical statements and 10 additional
 source-recovery records; Chapter 8 has 14 promoted mathematical statements and 5 additional
 source-recovery records; Chapter 9 has 19 promoted mathematical statements and 10 additional
+source-recovery records; Chapter 10 has 23 promoted mathematical statements and 9 additional
 source-recovery records. These recovery records preserve cited or underspecified families that are
-not promoted to Blueprint nodes. Chapter 10 is not yet inventoried.
+not promoted to Blueprint nodes.
 
 Read Chapters 2--10 in full and create one Blueprint node per in-scope item. Record full statements,
 source locations, representation decisions, and mathematical dependencies. Mark referenced results
@@ -305,12 +307,24 @@ source-recovery records rather than theorem evidence.
 
 ## Phase 10 - Chapter 10 symmetric functions
 
+Status: complete. All 23 reviewed source statements are formalized by 276 associated declarations
+with 59 reviewed dependency edges.
+
 - symmetric-function representation and elementary-symmetric ANF;
 - Walsh transform and nonlinearity;
 - resiliency and algebraic immunity;
 - rotation-symmetric and Matriochka-symmetric superclasses.
 
-This phase reuses the general criteria and does not redefine them for symmetric functions.
+The completed layer reuses the Chapter 2 numerical and algebraic normal forms, FABL Krawtchouk
+polynomials, Chapter 5 restriction/normality bounds, Chapter 6 bent and direct-sum theorems,
+Chapter 7 resiliency bounds, Chapter 8 propagation rigidity, and Chapter 9 majority immunity. It
+also contains a checked fast-Walsh certificate for the nine-variable rotation-symmetric function
+of nonlinearity 241.
+
+The odd-dimensional optimal-nonlinearity classification and its two window consequences are closed
+through the complete-quadratic normal form and complementary-pair restrictions. The
+odd-dimensional optimal-immunity uniqueness theorem is closed by constructing low-degree symmetric
+annihilators and inductively forcing the two half-threshold weight profiles.
 
 ## Phase 11 - Carlet closure
 

.agents/SPEC.md

@@ -32,16 +32,17 @@ PDFs, manifests, graphs, and caches are not sources of truth.
 
 ## Current verified baseline
 
-The reviewed Blueprint contains 294 source-facing statements, of which 291 are associated with
-1882 proved Lean declarations and 3 remain visibly open, connected by 713 mathematical dependency
+The reviewed Blueprint contains 317 source-facing statements, of which 314 are associated with
+2158 proved Lean declarations and 3 remain visibly open, connected by 772 mathematical dependency
 edges. Chapter 2 contributes 41 formalized statements, 174 declarations, and 56
 incoming edges. Chapter 3 contributes 7 formalized statements, 32 declarations, and 19 incoming
 edges. Chapter 4 contributes 73 formalized statements, 568 declarations, and 159 incoming edges.
 Chapter 5 contributes 31 statements (28 formalized and 3 open), 203 declarations, and 70 incoming
 edges. Chapter 6 contributes 70 formalized statements, 441 declarations, and 189 incoming edges.
 Chapter 7 contributes 39 formalized statements, 224 declarations, and 114 incoming edges. Chapter
 8 contributes 14 formalized statements, 131 declarations, and 42 incoming edges. Chapter 9
-contributes 19 formalized statements, 109 declarations, and 64 incoming edges.
+contributes 19 formalized statements, 109 declarations, and 64 incoming edges. Chapter 10
+contributes 23 formalized statements, 276 declarations, and 59 incoming edges.
 
 The completed Chapter 2 frontier includes Proposition 5's numerical-normal-form integrality
 criterion, the full raw Poisson formula, affine invariance, restriction recovery, the
@@ -100,6 +101,15 @@ cover algebraic-immunity consequences for weight, normality, and nonlinearity, h
 bounds, optimal majority and threshold families, the trace-power cyclic-run estimate, and the
 Carlet--Feng construction with its degree and nonlinearity bounds.
 
+The Chapter 10 inventory is source-reviewed and Blueprint-synchronized. Its 23 formalized nodes
+cover symmetric weight profiles, Relations (71)--(73), elementary-symmetric numerical and
+algebraic normal forms, binomial interpolation, power-of-two periodicity, Krawtchouk/Walsh
+formulas, even and odd normality, Theorems 16 and 17, numerical-degree and prime bounds, rotation
+symmetry, the explicit nine-variable nonlinearity-241 witness and its bent extensions, and
+Matriochka symmetry. The odd-dimensional optimal symmetric-nonlinearity classification, its two
+high-nonlinearity window consequences, and the optimal-algebraic-immunity uniqueness theorem are
+also complete.
+
 Chapter 2 has no open node: the finite-field coordinate theorem identifies ANF degree with the
 maximum binary weight in the univariate support, cyclotomic-orbit noncancellation closes Carlet
 Proposition 3, and the trace-pairing coordinate theorem is compiled. Chapter 3 likewise has no open node: the
@@ -123,6 +133,12 @@ dimension ranges, all three odd quotient-coordinate forms, the inclusive order-c
 endpoints, cyclic rather than linear binary runs, the corrected `n>=2` Carlet--Feng domain, and the
 survey's exact real nonlinearity inequality.
 
+Chapter 10's fidelity record uses a finite truncated periodicity condition, restores
+“nonconstant” in the Relation (73) conjectural sequel, claims cyclic invariance only for the
+explicit nine-variable seed, and separates the seed's proved Walsh certificate from empirical
+optimality searches. The classification endpoints retain the source hypotheses and exact integer
+thresholds.
+
 Source-facing splits remain explicit in Chapter 4. Rodier's one-sided lower endpoint and sharp
 interval have distinct nodes, as do the finite Hamming-ball and Plotkin lemmas and the resulting
 higher-order asymptotic estimate. The Reed--Muller coset-distance theorem

.agents/audit/dependency-dag.md

@@ -20,7 +20,8 @@ spine. The current baseline is:
 | Carlet Chapter 7 | 39 | 39 | 0 | 224 | 114 |
 | Carlet Chapter 8 | 14 | 14 | 0 | 131 | 42 |
 | Carlet Chapter 9 | 19 | 19 | 0 | 109 | 64 |
-| **Total** | **294** | **291** | **3** | **1882** | **713** |
+| Carlet Chapter 10 | 23 | 23 | 0 | 276 | 59 |
+| **Total** | **317** | **314** | **3** | **2158** | **772** |
 
 An item marked `[open]` has a complete mathematical statement but no Lean association. In the
 tables below, `consumer <- prerequisite-1, prerequisite-2` denotes one incoming edge from each
@@ -1182,10 +1183,131 @@ carlet-9-carlet-feng-nonlinearity
      carlet-2-trace-pairing-coordinates
 ```
 
+## Chapter 10 reviewed dependency DAG
+
+Chapter 10 contributes 23 promoted statements, all with proved associations. The following is the
+complete reviewed 59-edge graph.
+
+### Symmetric representations and transforms
+
+```text
+carlet-10-def-symmetric
+  <- carlet-2-def-boolean-function, carlet-2-def-support-weight
+carlet-10-rel-71-nnf
+  <- carlet-10-def-symmetric, carlet-2-nnf-existence-uniqueness,
+     carlet-2-prop-4-nnf-mobius
+carlet-10-univariate-binomial-representation
+  <- carlet-10-rel-71-nnf
+carlet-10-rel-72-anf
+  <- carlet-10-rel-71-nnf, carlet-2-anf-existence-uniqueness
+carlet-10-low-degree-classification
+  <- carlet-10-rel-72-anf, carlet-2-def-algebraic-degree,
+     carlet-2-def-affine-functions, carlet-6-rel-56-complete-quadratic
+carlet-10-power-two-periodicity
+  <- carlet-10-rel-72-anf, carlet-2-def-algebraic-degree
+carlet-10-krawtchouk-fourier-walsh
+  <- carlet-10-def-symmetric, carlet-2-pseudoboolean-fourier,
+     carlet-2-def-walsh-transform
+```
+
+### Normality, propagation, and nonlinearity
+
+```text
+carlet-10-even-middle-layer-normality
+  <- carlet-10-def-symmetric, carlet-5-def-4-normality
+carlet-10-theorem-16
+  <- carlet-10-def-symmetric, carlet-10-low-degree-classification,
+     carlet-4-def-propagation-criteria
+carlet-10-even-bent-symmetric-classification
+  <- carlet-10-theorem-16, carlet-6-def-7-bent,
+     carlet-6-rel-56-complete-quadratic
+carlet-10-odd-weak-normality-bound
+  <- carlet-10-def-symmetric, carlet-5-def-4-normality,
+     carlet-5-affine-flat-restriction-bound
+carlet-10-theorem-17
+  <- carlet-10-def-symmetric, carlet-5-rel-42-restriction-nonlinearity,
+     carlet-4-def-nonlinearity
+carlet-10-odd-optimal-nonlinearity-classification
+  <- carlet-10-theorem-17, carlet-10-low-degree-classification,
+     carlet-6-rel-56-complete-quadratic
+carlet-10-high-nonlinearity-quadratic-window
+  <- carlet-10-theorem-17, carlet-10-even-bent-symmetric-classification,
+     carlet-10-odd-optimal-nonlinearity-classification,
+     carlet-10-low-degree-classification
+carlet-10-high-nonlinearity-quadratic-or-odd-window
+  <- carlet-10-theorem-17, carlet-10-even-bent-symmetric-classification,
+     carlet-10-odd-optimal-nonlinearity-classification,
+     carlet-2-def-support-weight
+```
+
+### Numerical degree, resiliency, and algebraic immunity
+
+```text
+carlet-10-numerical-degree-half-bound
+  <- carlet-10-univariate-binomial-representation
+carlet-10-rel-73
+  <- carlet-10-univariate-binomial-representation
+carlet-10-prime-successor-full-numerical-degree
+  <- carlet-10-def-symmetric, carlet-10-rel-73,
+     carlet-7-prop-32-nnf-characterization
+carlet-10-largest-prime-numerical-degree-bound
+  <- carlet-10-def-symmetric, carlet-10-rel-73,
+     carlet-7-prop-32-nnf-characterization
+carlet-10-odd-optimal-ai-uniqueness
+  <- carlet-10-def-symmetric, carlet-9-majority-parameters,
+     carlet-4-def-annihilator-algebraic-immunity
+```
+
+### Rotation and Matriochka symmetry
+
+```text
+carlet-10-def-rotation-symmetric
+  <- carlet-10-def-symmetric
+carlet-10-rotation-symmetric-above-quadratic
+  <- carlet-10-def-rotation-symmetric,
+     carlet-4-odd-dimension-quadratic-covering-bounds,
+     carlet-6-direct-sum, carlet-6-rel-56-complete-quadratic
+carlet-10-def-matriochka-symmetric
+  <- carlet-10-def-symmetric
+```
+
+Only the explicit nine-variable seed in the rotation-symmetric existence statement is asserted to
+be invariant under the full cyclic coordinate action. Its direct sums with complete quadratic bent
+blocks retain the exact nonlinearity formulas but need not be rotation symmetric on all coordinates.
+The seven generic fast-Walsh certificate declarations associated with this statement are reusable
+finite-Walsh verification infrastructure whose direct source-facing use is the certified seed; they
+do not create an additional Blueprint statement.
+
+### Chapter 10 source-recovery boundary
+
+Nine reviewed inventory records remain outside the promoted 23-node graph and contribute neither
+manifest nodes nor dependency edges:
+
+- `carlet-10-symmetric-filter-implementation` lacks an LFSR state, correlation statistic, and
+  circuit or runtime cost model;
+- `carlet-10-additional-propagation-nonlinearity-families` and
+  `carlet-10-additional-resiliency-families` require theorem-complete statements from the cited
+  primary sources;
+- `carlet-10-numerical-degree-conjecture` is explicitly conjectural, and
+  `carlet-10-numerical-degree-finite-checks` lacks dimension ranges, extremizing profiles, and
+  independently checkable certificates;
+- `carlet-10-even-optimal-ai-families` omits the dimension ranges, profiles, and equivalence-class
+  data needed for a classification;
+- `carlet-10-rotation-bent-correlation-families` lacks exact parameterized theorems, while
+  `carlet-10-rotation-dihedral-finite-searches` lacks the functions and exhaustive-search
+  certificates needed for its claimed optima; and
+- `carlet-10-matriochka-complexity-and-parameters` combines an unspecified cost comparison with an
+  explicitly open cryptographic-parameter program.
+
+The numerical-degree conjecture's Relation (73) reformulation is deliberately corrected from the
+printed “no binary solution” to “no nonconstant binary solution”: constant weight profiles are
+immediate solutions. This conjectural specialization uses the nonnegative degree bound `d=n-4`
+and is therefore stated only from dimension four onward.
+
 ## Remaining proof frontier
 
-Three source statements remain open, all in the analytic Chapter 5 character-sum branch. Their complete
-statements remain visible without placeholder associations:
+Three source statements remain open, all in the Chapter 5 analytic character-sum branch. Their
+complete statements remain visible without placeholder associations:
 
 - `carlet-5-theorem-7-weil-bound` and `carlet-5-weil-nonlinearity-bound` require the analytic
   additive-character Weil estimate. The trace-pairing coordinate identification and the
@@ -1196,7 +1318,8 @@ statements remain visible without placeholder associations:
 
 Four further Chapter 5 citation-recovery records are intentionally outside the 31-node graph until
 their primary-source parameters support complete statements; they do not affect the manifest
-counts or edges.
+counts or edges. The nine Chapter 10 recovery records listed above likewise remain outside the
+23-node graph.
 
 Proposition 12 is closed: Chapter 3's affine-flat and equality-case slice layer proves the exact
 source classification. Chapter 4 is closed: Rodier's interval, the exact dimension-seven maximum,
@@ -1208,7 +1331,9 @@ reviewed frontier. Chapter 6 is closed: all 70 nodes have proved associations, w
 source-recovery records remain outside the graph until their cited statements or certificates can
 be recovered faithfully. Chapter 7 is closed: all 39 nodes have proved associations, while its ten
 source-recovery records preserve citation-only or underspecified construction and counting
-families.
+families. Chapters 8 and 9 are closed with 14 and 19 formalized nodes. Chapter 10 is closed with all
+23 nodes formalized; its nine recovery records preserve incomplete, conjectural, empirical, or
+operational source claims without changing the graph.
 
 ## Machine verification