Release v0.7.0

[Polarnova]

Summary

• formalize all 23 source-facing results in Carlet Chapter 10, with 276 unique Lean declaration associations and 59 reviewed dependency edges
• add the Chapter 10 production, Blueprint, inventory, and audit surfaces while reusing the existing Fourier, normality, bent, propagation, direct-sum, and algebraic-immunity APIs
• default the Blueprint dependency graph to the chapter overview without overriding later user selections
• bump the package and downstream documentation to v0.7.0

Validation

• lake build CryptBoolean.Carlet.Chapter10
• narrow AlgebraicImmunity and Blueprint module builds
• embedded dependency-graph JavaScript runtime harness
• forbidden-token scan
• Blueprint statement-style check: 317 statements / 314 formalized / 3 open
• source contract check: 2158 unique declarations / 772 dependency edges
• staged diff and whitespace checks

The complete root, axiom, Blueprint, manifest, and publication builds remain the required GitHub Actions gate before creating the v0.7.0 tag.

[Copilot]

Pull request overview

This PR prepares the v0.7.0 release by extending CryptBoolean’s verified surface from Carlet Chapters 2–9 to Chapters 2–10, adding the full Chapter 10 production/Blueprint layer (symmetric, rotation-symmetric, and related results), and updating the repository’s versioning and Blueprint validation baselines accordingly.

Changes:

• Add the full Carlet Chapter 10 production modules (symmetric representations, Krawtchouk/Walsh formulas, normality/propagation/nonlinearity results, numerical-degree bounds, rotation/Matriochka symmetry) and expose Chapter 10 through the library root imports.
• Extend the Blueprint (Verso) Chapter 10 content and update statement/declaration/edge baselines in the validator scripts and internal audit/spec docs.
• Update the Blueprint site JS to default the dependency graph view to the chapter/group overview without overriding later user selection, and bump version references to v0.7.0.

Reviewed changes

Copilot reviewed 35 out of 35 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
README.md	Updates documented release scope to Chapters 2–10 and bumps the suggested rev to v0.7.0.
lakefile.lean	Bumps the Lake package version to 0.7.0.
CryptBoolean/Carlet/Chapter10/Symmetric.lean	Introduces symmetry definitions and canonical weight-profile machinery.
CryptBoolean/Carlet/Chapter10/RotationSymmetric.lean	Adds rotation symmetry, ANF invariance characterization, and certified 9-variable witness material.
CryptBoolean/Carlet/Chapter10/Propagation.lean	Formalizes Chapter 10 propagation-criterion results for symmetric functions (Theorem 16 framing).
CryptBoolean/Carlet/Chapter10/PrimeDegree.lean	Adds prime-based numerical-degree bounds and resiliency consequences for symmetric functions.
CryptBoolean/Carlet/Chapter10/Periodicity.lean	Adds power-of-two periodicity characterization for symmetric profiles vs algebraic degree.
CryptBoolean/Carlet/Chapter10/Normality.lean	Adds complementary-pair restrictions and even/odd normality bounds for symmetric functions (Theorem 17 framing).
CryptBoolean/Carlet/Chapter10/LowDegree.lean	Adds low-degree symmetric classifications and equivalent profile recurrences.
CryptBoolean/Carlet/Chapter10/Krawtchouk.lean	Adds Krawtchouk/Fourier/Walsh layer formulas and symmetric spectrum expansions.
CryptBoolean/Carlet/Chapter10/ElementarySymmetric.lean	Adds elementary-symmetric bases, Relations (71)–(72) infrastructure, and profile transforms.
CryptBoolean/Carlet/Chapter10.lean	Aggregates Chapter 10 production imports under a single chapter module.
CryptBoolean/Carlet/Chapter04/OddWeightingNonlinearity.lean	Makes an affine-function parity lemma public for downstream Chapter 10 use.
CryptBoolean/Carlet/Chapter04/OddDimensionBestNonlinearity.lean	Exposes Walsh certificate infrastructure needed by Chapter 10 rotation-symmetric witness proofs.
CryptBoolean.lean	Imports Chapter 10 into the root verified production surface.
blueprint-verso/scripts/validate_manifest.py	Updates expected statement/formalized/declaration/edge totals and adds Chapter 10 to expected chapter/group counts.
blueprint-verso/scripts/check_statement_style.py	Updates expected statement/formalized/open counts to the new baseline.
blueprint-verso/CryptBooleanBlueprint/Site.lean	Adds JS logic to default dependency-graph view selection to chapter/group overview.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/RotationMatriochka.lean	Adds Chapter 10 Blueprint prose for rotation-symmetric and Matriochka-symmetric material.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Resiliency.lean	Adds Chapter 10 Blueprint prose for numerical-degree/resiliency statements.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Representation.lean	Adds Chapter 10 Blueprint prose for symmetry definitions and (71)–(72) representation results.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Nonlinearity.lean	Adds Chapter 10 Blueprint prose for normality/nonlinearity theorems and classifications.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/Fourier.lean	Adds Chapter 10 Blueprint prose for Krawtchouk/Fourier/Walsh formulas.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10/AlgebraicImmunity.lean	Adds Chapter 10 Blueprint prose for optimal algebraic immunity classification.
blueprint-verso/CryptBooleanBlueprint/Carlet/Chapter10.lean	Aggregates Chapter 10 Blueprint includes.
blueprint-verso/CryptBooleanBlueprint/Blueprint.lean	Includes Chapter 10 in the main Blueprint and updates chapter count text/group list.
AGENTS.md	Updates the “Current verified surface” baseline counts and adds Chapter 10 summary.
.agents/SPEC.md	Updates verified baseline counts and Chapter 10 inventory/fidelity notes.
.agents/PLAN.md	Marks Phase 10 complete and updates baseline counts.
.agents/audit/fidelity.md	Updates baseline totals and adds Chapter 10 fidelity boundary notes and recovery boundary.
.agents/audit/dependency-dag.md	Extends the reviewed dependency DAG summary and totals to include Chapter 10.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.