Add closed-ball deviation direct data alias - #2757
Merged
Merged
Conversation
phasetr
marked this pull request as ready for review
May 20, 2026 12:56
phasetr
added a commit
that referenced
this pull request
Aug 3, 2026
Follow-up to 0a52f59 after independent review. Documentation only: Lean doc comments, `docs/index.md` rows, and `tex/proof-guide.tex`. No statement, proof term, or public name changes. 1. Off-by-one in the identical-statement group. The pilot canonicalizes three of *four* declarations that share the statement, not three of three. `freeEnergyComplexAlongExhaustion_closedBallBranchDeviationRelCompact_patch` (`ClosedBallPatches/RelCompact.lean`, PR #2745) carries the byte-identical statement as well, but was deliberately excluded from the pilot: it proves the statement by the independent `toDeviationData` route into `freeEnergyComplexAlongExhaustion_branchDeviationRelCompact_patch`, and it still has its own in-repo consumers (`BranchLocallyBoundedPatches/ RelCompact.lean`, its own `_of_isCompact`, and the Z^d wrapper). The owner doc comment, the excluded theorem's doc comment, the two `docs/index.md` rows, and the PR #2745/#2752/#2756/#2768 proof-guide theorem environments now say "owner for the three pilot-scoped declarations" and disclose the fourth instead of implying an exhaustive three-element group. 2. Stale construction path in the PR #2756 proof-guide environment. It stated that the direct-range endpoints build their relatively compact range data "through the PR #2757 direct-route data alias". Since 0a52f59 none of the three endpoints listed there calls `toRangeRelCompactData_direct`: the abstract one forwards to the owner, the `_of_isCompact` one calls the abstract one, and the positive-real one calls the `_of_isCompact` one; the owner calls `toRangeRelCompactData_closedBallLocal_direct`. The data alias itself remains in use by the other closed-ball conversions (`toRangeRelCompactData_viaDeviation_direct` and the eventual-overlap conversion), so it is not orphaned. The sentence now states the actual post-PR path. 3. Correction to the 0a52f59 commit message (left as pushed; not rewritten). It justified keeping `...ClosedBallBranchDeviationAscoliData.toRangeRelCompactData_viaLocal_direct` with the blanket claim "this repo does not run reference-0 deletion campaigns". That claim is false: deliberate zero-consumer deletions have happened repeatedly (272b310/#4641, 3fbc873/#4749, 051aa85/#4751, f891116/#4764), as have duplicate retirements (6147071/#4839, 2613222/#4851), and `lean-coding-conventions` points the other way (reference-0 declarations are decorative and should generally be removed). The real, narrower reason is that removing or re-pointing that declaration is outside the minimal scope of the #4854 pilot. The `docs/index.md` rows and the via-local proof-guide environment are reworded to that narrower claim and now say explicitly that this is a scope statement about this PR, not a general exemption for reference-0 declarations. Verification: `lake build` full, zero warnings and zero errors; `lake exe GKSTest` passes; `latexmk -g -pdf proof-guide.tex` clean with zero Overfull/Underfull boxes, zero LaTeX/package warnings and zero undefined references; no Japanese characters in the proof guide. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
phasetr
added a commit
that referenced
this pull request
Aug 3, 2026
Two documentation-only wording fixes from the #4868 review round. - tex/proof-guide.tex (PR #2756 direct range patch bridge theorem): the sentence "reach the owner through this alias" had an ambiguous antecedent. The preceding sentence names the PR #2757 data-layer alias `toRangeRelCompactData_direct`, which the same theorem block already states no listed endpoint calls, so the sentence could be read as self-contradictory. Name the intended referent explicitly: the theorem-level alias `_closedBallBranchDeviationRelCompact_directRange_patch` (ClosedBallPatches/Direct.lean:184, and PosReal.lean:103 through it, reach the owner at Direct.lean:142), and say it is not the data alias. - docs/index.md (PR #2752 row): the deliberately-excluded fourth declaration `..._closedBallBranchDeviationRelCompact_patch` was pointed at with "(PR #2745 row above, `ClosedBallPatches/RelCompact.lean`)", but that row's declaration column lists only the `_of_isCompact` companion. Say instead that it is the abstract endpoint of the PR #2745 bridge, declared in `ClosedBallPatches/RelCompact.lean`, and that the row above lists its `_of_isCompact` companion. The TeX paragraph keeps its line count, so the guide citation pin at line 26910 in scripts/test_dead_candidate_scan.py is unaffected. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
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.
Summary
Add a direct-route alias for the closed-ball branch-deviation Ascoli data to relatively compact range data conversion:
Ambient.LeeYangPointwiseNormAllStageCompactRealClosedBallBranchDeviationAscoliData.toRangeRelCompactData_directThe alias delegates to the existing
toRangeRelCompactData_closedBallLocal_directroute, keeping the data boundary parallel toLeeYangClosedBallBranchLocallyBoundedAscoliData.toRangeRelCompactData_direct. The PR #2756 directRange patch endpoint now routes through this alias.Part of #628.
Verification
lake build IsingModel.AmbientComplexAnalyticity IsingModel.Concrete.LatticeGraphCorrelation.PerStageComplexsorry/admitgreptex/proof-guide.texgit diff --checklatexmk -lualatex -f -interaction=nonstopmode proof-guide.texlake buildlake build test.IsingModel.GKSTestlake exe GKSTest