Blueprint key lemma equivalence#43
Open
FordUniver wants to merge 9 commits into
Open
Conversation
Major changes:
- Extract inner product equivalence as separate helper lemma (lem:inner-product-equivalence)
* Provides complete proof for Λiff sorry at KeyLemma.lean:114
* Shows inner product expansion and algebraic equivalence chain
* Links to Lean code with \lean{Λiff}
- Restructure main proof into 4 explicit steps matching Lean:
* Step 1: Define N'_i(x) and σ_i (Lean lines 92-109)
* Step 2: Apply Geometric Lemma (Lean lines 117-122)
* Step 3: Derandomization via averaging (Lean lines 124-139)
* Step 4: Define Y'_i and verify inequalities (Lean lines 141-201)
- Add explicit Lean code references throughout:
* Comments indicating corresponding Lean line numbers
* References to Lean lemmas (pidgeon_thing, Λiff)
* Remarks explaining Lean structure differences
- Complete both calculation cases:
* Case 1 (color ℓ): Full 6-step calculation
* Case 2 (colors i≠ℓ): Full 6-step calculation (previously omitted)
- Make derandomization argument explicit:
* Define set P of "good pairs"
* Show probability → cardinality conversion
* Explain averaging/pigeonhole principle
Impact:
- Blueprint now provides complete guide for filling Lean sorry
- Structure matches Lean code 1:1 for easier formalization
- All intermediate steps justified and linked
- Ready for Lean formalization
Stats: 157 insertions(+), 82 deletions; 75 net lines added
Mark the Λiff lemma (inner product equivalence) as fully proven: - Remove outdated "(currently marked as sorry)" text - Add \leanok marker for blueprint dependency tracking The Λiff proof was completed by combining inner_expanded and dot_expanded into a unified inner_and_dot_expanded lemma, which successfully performs the scalar cancellation α·pY·(1/√(α·pY))² = 1 using field_simp and Real.sq_sqrt. Note: blueprint/lean_decls is gitignored (likely auto-generated), so Λiff will be added to it by the blueprint build process.
The \leanok marker indicates completion status, not prose text. The blueprint should remain a mathematical document, not a progress report.
Line numbers create maintenance burden as the code evolves. Removed from: - 3 visible text references (lines 103, 140, 218) - 4 maintainer comment references (lines 94, 123, 136, 165) All references read naturally without line numbers, e.g.: - 'In Lean (lines 92-95), this is proven...' → 'In Lean, this is proven...' - 'at lines 124-139' → (removed entirely) The mathematical content and Lean implementation details remain clear without brittle line references.
- Remove \lean{Λiff} and \leanok from lem:inner-product-equivalence
- Remove \lean{key} from lem:key-lemma
- These declarations will be added in the lean-proofs branch
Changed \autoref{key:lemma} to \autoref{lem:key-lemma} and
\autoref{lem:lambda} to \autoref{lem:geometric} to match actual
labels defined in the document.
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.
No description provided.