feat(FineGrained): exact MAX-SAT and polynomial-bit weighted counting - #2100

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

`Cslib.Circuits.Boolean.PopulationCount.treeStepCode` and `Cslib.Crypto.Homomorphic.augmentCode` (private) (Complexity/Crypto/Computational/Homomorphic/Circuit/PolyTime.lean:55) share a 149-node subterm, 75% of the smaller body, built from `Cslib.Circuits.Boolean.appendCode`, `Cslib.Circuits.Boolean.compCode`, `Cslib.Circuits.Boolean.Op`, `List.nil`, `List.range`, `List.map`. Advisory only; see the job summary.

`Cslib.Circuits.Boolean.linearThresholdCircuit` and `Cslib.Circuits.Boolean.MassProduction.Uhlig.restriction` (Complexity/Computability/Circuit/Boolean/MassProduction/Uhlig/Layer.lean:74) share a 311-node subterm, 73% of the smaller body, built from `Equiv`, `Cslib.BitString`, `Equiv.symm`, `Cslib.BitString.equivFin`. Advisory only; see the job summary.

`Cslib.Circuits.Boolean.linearThresholdCircuit` and `Cslib.Circuits.Boolean.thresholdDeMorganCircuit` (Complexity/Computability/Circuit/Boolean/ThresholdNC1.lean:113) share a 327-node subterm, 69% of the smaller body, built from `Cslib.Circuits.Circuit.append`, `Cslib.Circuits.Boolean.signature`, `Cslib.Circuits.Boolean.wordConstCircuit`, `Equiv`, `Cslib.BitString`, `Equiv.symm`. Advisory only; see the job summary.