feat(Circuits): charge inversion’s nonlinear feature entropy

[SamuelSchlesinger]

Samuel’s dot here.

Depends on #68. This is a stacked PR targeting feat/collision-feature-budget, so its diff contains only the circuit integration and blueprint additions.

Result

For inversion over a finite binary field with a supplied common input/output linear coordinate basis and n ≥ 3, signed unbounded AND/OR/XOR circuits satisfy

g ≥ ((3 + 4c) / (2 + 2c)) n − (log₂5 + 8c) / (2 + 2c),

where c = 1 − H₂(1/4). Numerically, this is

g ≥ 1.579380164285695… n − 1.611690328097512…

The larger leading coefficient comes with a larger finite penalty than the existing majority-fibre theorem; both bounds remain available. Historical priority is not claimed.

Changes

• Extract an explicit affine-plus-conjunction representation for every circuit output using the existing gateValues_mem induction
• Apply feat(Circuits): bound biased features by average collisions #68’s collision bound to actual conjunction gate outputs, choosing each marked gate’s rare Boolean value
• Prove the feature budget N ≥ n + c·m − log₂5, where N counts conjunction gates and m counts multiple-primary conjunctions
• Combine the feature budget with distinct-output counting, primary-summary entropy and the existing affine-restriction inequality
• Export the normalized exact gate bound and add two matching blueprint nodes

There are no independence, depth, fan-in, fanout or nonlinear-reuse restrictions. The feature-budget theorem itself does not require n ≥ 3; that condition is used for the final gate-count theorem.

Verification

All checks passed on exact tree 3dbe505a782381cc8c3c926ca4c2fb03ad991e81, based on #68 head ec175563:

• Focused Lean build with --wfail
• Full library, five executable validation roots, seven isolated API checks and runLinter (7,537 jobs)
• Style lint and all 25 maintenance-script tests
• Environment lint for the library and five validation roots
• Axiom guard: 92,560 declarations, 68,270 theorems, zero project axioms, standard axioms only
• Blueprint check: 1,215 nodes and 4,256 Lean references
• Independent source and mathematical review of the exact tree, with no blocking findings
• git diff --check

No sorry, custom axioms, native proof shortcuts, dependency changes or author-credit changes are introduced. Stacked PR CI passed every gate on merge commit 17fa7e389dc03d049a650b9a658be96c47cf1e7e, combining head 03164e5b with #68 head ec175563. The exact checkout SHA was verified in the job log. This tests the stated stacked base; after retargeting to dev, the new merge result must pass CI again.