Repository navigation
feat(Circuits): bring the inversion feature bound onto dev - #70
Merged
Merged
Conversation
Extract affine-plus-conjunction representations of circuit outputs and apply the collision budget to the actual nonlinear feature vector. Combine its quarter-bias charge with primary-message entropy and affine restrictions to prove the exact 1.579380164... leading coefficient. Use a supplied common binary-field basis and retain the earlier finite bounds with their smaller penalties. Add matching blueprint nodes.
…generators feat(Circuits): charge inversion’s nonlinear feature entropy
Preserve both the new conditional-fibre blueprint sections and the unchanged nonlinear-feature sections at their shared insertion point. The four feature-integration Lean files are unchanged from reviewed #69. Recheck the full library, validation and API roots, style and environment linters, maintenance tests, axiom guard and blueprint consistency.
SamuelSchlesinger
marked this pull request as ready for review
October 5, 2026 04:01
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Samuel’s dot here.
This brings the already-reviewed integration from #69 onto
dev. #68 was merged intodevfirst, and #69 was subsequently merged into its stacked base branch,feat/collision-feature-budget. This follow-up closes that remaining integration step.Scope
The diff is exactly #69’s five files and 304 added lines, with no additional source edits:
The theorem uses a supplied common input/output binary-field basis, with n ≥ 3 for the final gate bound. The earlier majority-fibre bound remains available with its smaller finite penalty.
Verification
The original exact source tree passed independent mathematical review and all local repository gates, and #69’s stacked CI passed.
During verification,
devadvanced to84173cd9and added sections at the same blueprint insertion point. Headfc5114785b6ac6029abc80422fca1e258e3cd36cnow incorporates that commit and preserves both section groups. All four Lean file blobs remain identical to reviewed #69; removing our unchanged 62-line blueprint block reproduces the entire new dev chapter byte-for-byte.Fresh independent review and all local gates passed on resolved tree
601c3d268d5fc9d3a2624ac2243107e692687ae2: full aggregate build (7,577 jobs), style lint, 25 maintenance tests, all environment linters, the 93,081-declaration axiom guard with zero project axioms, and blueprint checks (1,232 nodes; 4,326 Lean references). The update was fast-forwarded without force-pushing.Fresh current-base CI passed every gate on merge commit
a4c620087cc9e676fa0b1ff6e8295f10001036af, with the checkout SHA verified in the job log. The earlier-base run was not used to approve the merge.Merged into
devatbe804d01819fb13987a36e8856e14600dc6ad70e. The actual merge tree equals the tested and independently reviewed tree601c3d268d5fc9d3a2624ac2243107e692687ae2; the feature-budget and exact gate-bound theorems were verified in the resulting dev file. No theorem or proof was changed during conflict resolution.