Conversation
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 396 maxHeartbeats units across 9 files (1,978 added LOC). Sum of Count-heartbeats wall-clock total: 29.00 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Champernowne.CountExtras |
3.10 s |
LeanPool.Champernowne.Defs |
2.90 s |
LeanPool.Champernowne.DigitCount |
2.70 s |
LeanPool.Champernowne.Asymptotics |
2.70 s |
LeanPool.Champernowne.Positions |
2.20 s |
LeanPool.Champernowne.Count |
1.50 s |
LeanPool.Champernowne.Prefix |
1.30 s |
LeanPool.Champernowne.Main |
1.10 s |
LeanPool.Champernowne |
1.00 s |
Per-file `lean --profile` output
LeanPool/Champernowne.lean
import took 1.77s
cumulative profiling times:
elaboration 0.153ms
import 1.77s
initialization 30.3ms
interpretation 149ms
linting 0.361ms
module linting 0.00104ms
overlappingInstancesLinter 0.442ms
parsing 0.029ms
tacticAnalysis 0.871ms
real 2.52
user 1.00
sys 0.84
LeanPool/Champernowne/Asymptotics.lean
import took 900ms
cumulative profiling times:
attribute application 0.154ms
compilation (IR) 0.0326ms
compilation (LCNF base) 0.653ms
compilation (LCNF impure) 0.137ms
compilation (LCNF mono) 0.236ms
congr simp thm 11.8ms
dsimp 34ms
elaboration 73.1ms
fix level params 1.48ms
import 900ms
initialization 29.5ms
instantiate metavars 3.26ms
interpretation 719ms
let-to-have transformation 0.221ms
linting 44ms
module linting 0.00136ms
norm_num 15.3ms
overlappingInstancesLinter 5.05ms
parsing 25.4ms
process pre-definitions 14.6ms
ring 76.8ms
share common exprs 19.3ms
simp 165ms
tactic execution 394ms
tacticAnalysis 61.9ms
type checking 251ms
typeclass inference 720ms
real 2.54
user 3.35
sys 0.78
LeanPool/Champernowne/Count.lean
import took 788ms
cumulative profiling times:
attribute application 0.119ms
blocked (unaccounted) 89.3ms
compilation (IR) 0.581ms
compilation (LCNF base) 7.9ms
compilation (LCNF impure) 2.44ms
compilation (LCNF mono) 5.39ms
congr simp thm 3.48ms
elaboration 35.8ms
fix level params 0.485ms
import 788ms
initialization 40.4ms
instantiate metavars 4.24ms
interpretation 294ms
let-to-have transformation 0.139ms
linting 13.8ms
module linting 0.00139ms
overlappingInstancesLinter 2.91ms
parsing 12.3ms
process pre-definitions 7.71ms
share common exprs 6.96ms
simp 128ms
tactic execution 102ms
tacticAnalysis 32.8ms
type checking 40.7ms
typeclass inference 106ms
real 1.75
user 1.44
sys 0.74
LeanPool/Champernowne/CountExtras.lean
import took 785ms
cumulative profiling times:
attribute application 0.328ms
compilation (IR) 0.151ms
compilation (LCNF base) 2.72ms
compilation (LCNF impure) 0.732ms
compilation (LCNF mono) 1.1ms
congr simp thm 4.06ms
elaboration 153ms
fix level params 1.86ms
import 785ms
initialization 33.8ms
instantiate metavars 6.77ms
interpretation 529ms
let-to-have transformation 0.445ms
linting 62.9ms
module linting 0.00128ms
norm_num 2.69ms
overlappingInstancesLinter 7.57ms
parsing 49.2ms
process pre-definitions 28.2ms
ring 21.8ms
share common exprs 17.2ms
simp 130ms
tactic execution 995ms
tacticAnalysis 116ms
type checking 708ms
typeclass inference 378ms
real 2.68
user 3.84
sys 0.75
LeanPool/Champernowne/Defs.lean
import took 738ms
cumulative profiling times:
attribute application 0.057ms
blocked (unaccounted) 1.44ms
compilation (IR) 0.307ms
compilation (LCNF base) 5.13ms
compilation (LCNF impure) 1.78ms
compilation (LCNF mono) 2.53ms
congr simp thm 0.694ms
elaboration 28.7ms
fix level params 0.0837ms
import 738ms
initialization 36.5ms
instantiate metavars 0.15ms
interpretation 181ms
let-to-have transformation 0.044ms
linting 4.21ms
module linting 0.00119ms
overlappingInstancesLinter 1.89ms
parsing 3.36ms
process pre-definitions 2.07ms
share common exprs 0.504ms
simp 7.89ms
tactic execution 11.5ms
tacticAnalysis 13.2ms
type checking 10.5ms
typeclass inference 14ms
real 1.53
user 0.92
sys 0.72
LeanPool/Champernowne/DigitCount.lean
import took 755ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 186ms
cumulative profiling times:
attribute application 0.216ms
congr simp thm 2.96ms
elaboration 121ms
fix level params 2.4ms
import 755ms
initialization 33.8ms
instantiate metavars 8.09ms
interpretation 933ms
let-to-have transformation 0.419ms
linting 76.6ms
module linting 0.00128ms
norm_num 13.9ms
overlappingInstancesLinter 7.91ms
parsing 52.7ms
process pre-definitions 22.1ms
ring 116ms
share common exprs 38.7ms
simp 209ms
tactic execution 1.01s
tacticAnalysis 123ms
type checking 787ms
typeclass inference 635ms
real 2.86
user 4.78
sys 0.73
LeanPool/Champernowne/Main.lean
import took 909ms
cumulative profiling times:
attribute application 0.0205ms
congr simp thm 0.691ms
elaboration 3.86ms
fix level params 0.0335ms
import 909ms
initialization 36.2ms
instantiate metavars 0.0673ms
interpretation 182ms
let-to-have transformation 0.0158ms
linting 1.68ms
module linting 0.00127ms
norm_num 1.23ms
overlappingInstancesLinter 2ms
parsing 1.1ms
process pre-definitions 0.392ms
share common exprs 0.161ms
simp 3.1ms
tactic execution 4.67ms
tacticAnalysis 5.93ms
type checking 5.98ms
typeclass inference 2.39ms
real 1.69
user 0.98
sys 0.75
LeanPool/Champernowne/Positions.lean
import took 750ms
cumulative profiling times:
attribute application 0.11ms
compilation (IR) 0.0717ms
compilation (LCNF base) 0.46ms
compilation (LCNF impure) 0.326ms
compilation (LCNF mono) 0.523ms
congr simp thm 0.9ms
elaboration 38.2ms
fix level params 0.592ms
import 750ms
initialization 41.4ms
instantiate metavars 2.7ms
interpretation 294ms
let-to-have transformation 0.118ms
linting 25.9ms
module linting 0.00155ms
norm_num 1.6ms
overlappingInstancesLinter 3.97ms
parsing 14.4ms
process pre-definitions 6.98ms
ring 25.6ms
share common exprs 11.8ms
simp 23.6ms
tactic execution 226ms
tacticAnalysis 54.6ms
type checking 182ms
typeclass inference 104ms
real 1.87
user 1.70
sys 0.67
LeanPool/Champernowne/Prefix.lean
import took 740ms
cumulative profiling times:
attribute application 0.0523ms
compilation (IR) 0.0535ms
compilation (LCNF base) 0.515ms
compilation (LCNF impure) 0.252ms
compilation (LCNF mono) 0.292ms
congr simp thm 0.97ms
elaboration 8.61ms
fix level params 0.134ms
import 740ms
initialization 29.7ms
instantiate metavars 0.224ms
interpretation 171ms
let-to-have transformation 0.0358ms
linting 4.12ms
module linting 0.00473ms
overlappingInstancesLinter 2.04ms
parsing 3.13ms
process pre-definitions 1.27ms
share common exprs 0.581ms
simp 6.96ms
tactic execution 20.9ms
tacticAnalysis 11.5ms
type checking 3.03ms
typeclass inference 2.97ms
real 1.49
user 0.87
sys 0.70
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low risk] Adds a new mathematical proof library module. No new defect was found to block merging, but upstream fidelity and prior-art claims remain independently unverified. SummaryThe PR imports a discrete proof of Champernowne normality in every base, with counting infrastructure and a project card. Since the previous review, the inspected changes revise proofs in the existing five-eighths theorem module; no new defect was established.
Reviews (17) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
{
"review": "Separate thorough agentic source, diff, mathematics, engineering and policy review",
"head_commit": "1ab4ffb1a4798beb01d7b6f3325af343df660ca2",
"conclusion": "APPROVE",
"merge_condition": "Do not merge until the configured GPT-6-Astra review is available and passes. All required CI and the complete documentation workflow have passed; Greptile has no actionable finding.",
"coverage": {
"upstream": "31a76dbde2727745beb6fb81af4cab1ce6a15fda; actual public repository, root Apache-2.0 license, announcement, README and every imported source file inspected in bounded chunks.",
"files": {
"Defs.lean": "Digit construction, occurrence counter and exact quantifiers of normality.",
"Prefix.lean": "Finite-block coherence, valid index bounds and identification of prefixes with the digit stream.",
"Count.lean": "Append lower bounds, occurrence-position characterization, allWords completeness/cardinality and window pigeonhole.",
"DigitCount.lean": "Periodic injection, substring/arithmetic equivalence, partial cohort estimates, exponential error absorption and general block bound.",
"Positions.lean": "findGreatest straddling index, lower transfer, complementary-word upper transfer and prefix chain.",
"Asymptotics.lean": "Unbounded index/digit length, error/n limit, natural-to-real casts, little-o and final frequency limit.",
"Main.lean": "All-base endpoint and decimal specialization.",
"CountExtras.lean": "All append/take/drop/flatten API, exact periodic bijection, digitEquiv and round trips, head/interior/past-end counts, both cohort formulas.",
"LeanPool/Champernowne.lean": "Public export closure, attribution and generated card.",
"LeanPool/projects.yml": "Every headline/informal pair, primary source, commit, license, provenance and scope.",
"LeanPool.lean": "Generated reachability, with no unrelated project change."
},
"preservation": "All 96 signatures recognized by the comparison script are unchanged after two name-only renamings; the equation-style allWords definition was checked separately. The two added lemmas factor existing arguments. No upstream theorem in the selected mathematical scope was removed or weakened.",
"exclusions": "Sandbox diagnostics, comparator challenge/bridge and build scaffolding are outside the imported proof/API closure; CountExtras was intentionally retained for reuse."
},
"rubrics": {
"faithfulness": {
"verdict": "pass",
"bottom_line": "The Lean proves precisely the advertised discrete all-base normality theorem and exact within-cohort counts.",
"proves_the_claim": "proves_it",
"claim_note": "champernowne_normal (b : ℕ) (hb : 2 ≤ b) concludes IsNormalSequence b (champDigit b); this quantifies over every nonempty word with entries below b and uses real-valued occurrence-count/n limits.",
"assumed_inputs": "Only b ≥ 2 and the explicitly stated word/base/length/head conditions for counting lemmas; no analytic or counting theorem is postulated in a structure or class.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate headline was found in Mathlib, the pool registry/tree, repository history, or pool issues/PRs.",
"already_formalized": "",
"novelty_note": "Existing Mathlib digits/filter/asymptotic infrastructure does not already supply the Champernowne normality result; the pool normal-family search hits concern unrelated complex analysis.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "A named theorem in normal-number theory with a substantial reusable counting development warrants preservation.",
"fit": "good_fit",
"level": "graduate",
"branch": "normal numbers and combinatorics on words",
"mode": "theory_building",
"significance_one_sentence": "Establishes the classical explicit normal-sequence construction uniformly in every base, with exact finite digit-block counts and quantitative prefix estimates rather than an isolated wrapper lemma.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The actual upstream theorem and announcement support the card; the 1933 decimal result is identified as historical background to an explicitly labelled discrete all-base generalization.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "Focused modules, explicit finite-counting/asymptotic boundaries, preserved generality and measured removal of duplication and solver hot spots make this a maintainable import.",
"code_quality": 4,
"findings": []
}
},
"additional_user_axes": {
"edge_cases": "Checked b=2, one-digit words, words beginning with zero, m=word length, empty-word exclusion and total division at n=0. Leading-zero versus nonzero-head cohort formulas have the intended different head contribution; the limit ignores finitely many initial n. No real-number expansion or transcendence theorem is claimed.",
"license_and_provenance": "Apache-2.0 verified in upstream LICENSE and all retained source headers. Arthur Champernowne remains credited; AI provenance follows his explicit Claude Code announcement and this AI-assisted port. No license ambiguity found.",
"trust": "Existing repository audit over all 99 public declarations passes, and its compiled-environment audit, including private/generated auxiliaries, has zero findings. No sorry/admit, prohibited axiom, unsafe/partial/native_decide, option backdoor, or waiver was imported.",
"dependencies_and_size": "Eight mathematical modules plus an entry point, no added package, exact pinned Lean/Mathlib revisions. Definitions, endpoints and the entire imported dependency closure were inspected; no generated certificate or case-table bulk was added.",
"measured_cost": "Warm-dependency clean project builds: baseline 29.40/29.90 s; optimized 8.42 s and final-head repeat 8.82 s. Build graph 8932→1752 jobs. The two largest original hot spots fell from 22734.694→3492.475 and 12947.983→1179.957 conventional heartbeats. Remaining proof costs do not show a material safe optimization requiring further churn.",
"local_validation": "Warning-free build; mk_all --check; runLinter on all nine modules; lint-style; full textual quality scans; import metadata/card/declaration validation; public-axiom and environment audits; diff whitespace/content separation. Final local quality run reports TOTAL ERRORS 0. No Python code changed.",
"ci_observed": "Lean Action CI run 35436833905 succeeded on the reviewed head: generated index, full pool build, challenge/solution build, Mathlib linters, style checker and repository quality/trust audit all passed. Documentation run 35436833931 and proof-profile run 35436833927 passed. The protected Build project, Content / non-content separation and Documentation preflight checks are green."
},
"material_findings": [],
"repairs_verified": [
"Current-toolchain warning and simplification repairs",
"Namespace/public exports and focused imports",
"Factored repeated cohort-error and head/interior counting arguments",
"Prefix dependency fan-out reduction",
"Two scanner-compatible identifier renamings without statement changes",
"Accurate discrete theorem card, provenance, source pin and historical attribution",
"Generated index and clean content-only scope"
],
"external_blocker": "GPT review not run: GitHub reports LLM Review disabled_manually, the documented restricted local alias is absent, and both existing Azure SSH routes timed out. No workflow/configuration change or paid API fallback was used."
} |
|
Merge blocker: the configured GPT-6-Astra review could not run. GitHub reports
No workflow, review policy, VM configuration, credential, or paid API fallback was changed. Greptile is green with no actionable finding; the separate thorough review approves the content. All local checks and the complete documentation workflow pass. Full Lean CI has now passed, including the full-pool build, challenge/solution build, Mathlib linters, style checker and repository quality/trust audit. All required checks are green. Leaving this PR open as a draft until the configured GPT review can complete. The disabled workflow and unavailable Azure connection are external blockers, not a request to waive review. |
# Conflicts: # LeanPool/projects.yml
Vilin97
added
the
needs-maintainer
|
Daily needs-maintainer cycle completed at Resolved: the configured review-service blocker and the review’s unused-premise finding. Repair commit changes only Verified at this exact head: full Lean CI, documentation, all required status contexts, and the five-rubric GPT-6-Astra/xhigh review pass. The review has no findings. Local project build, all module linters, style/index/diff checks, textual/card validation, all 99 public-declaration axiom closures and the compiled-environment audit also passed. Pinned upstream source and Apache-2.0 attribution were checked independently. The initial upstream commit corroborates AI participation; the historical Zulip announcement could not be independently fetched this cycle. No conflicting attribution evidence was found. Removing |
# Conflicts: # LeanPool.lean # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All four card headlines match the Lean statements and underlying definitions. |
| Novelty | ✅ pass |
Searches of the pinned Mathlib and existing pool found no duplicate of any of the four headline results. |
| Significance | ✅ pass |
This completed development of Champernowne normality meets the significance bar through a classical named theorem and substantial supporting counting and asymptotic theory. |
| Sources | ✅ pass |
The credited upstream normality theorem and cohort formulas support the claims, and the card explicitly distinguishes the all-base result from Champernowne’s 1933 base-ten theorem. |
| Code quality (advisory) | ✅ pass |
Clear module boundaries, shared cohort-error and exact-sum lemmas, and separation of optional counting infrastructure make this maintainable; no material quality findings. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Only the disclosed base and word conditions: b ≥ 2, nonempty words with digits below b, and—for cohort counts—length w ≤ m and the stated first-digit condition; no substantive result is taken as an additional hypothesis. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | number theory and uniform distribution |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The theorem proves overlapping word-frequency convergence to b^(-length w) for the actual concatenated digit stream in every base b ≥ 2; both exact cohort formulas also match, including the boundary k = m.
Establishes normality of the concatenated positive-integer digit sequence in every integer base at least two, with reusable exact cohort counts and quantitative prefix estimates.
Tokens: 2,917,944 in / 16,451 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $59.5927 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Vilin97
removed
the
needs-maintainer
Changes requested by automated reviewReviewed exact current head The exact current head is merge-conflicted ( Acceptance condition: repair the named defect on a new head and make all required protected checks green. Do not change repository policy or add waivers. |
Exact-head reconciliationReviewed exact current head |
Changes requested by automated reviewReviewed exact current head |
|
Re-reviewed The full contribution proves the stated discrete all-base normality theorem and exact cohort counts. The pinned upstream source, Apache-2.0 license and initial AI-credit commit agree. The earlier position-zero repair is preserved. This cycle pushed the main-integration commit, resolving the registry conflict while preserving all 219 main cards plus the original Champernowne card and all nine Lean files. Targeted warning-free project build, actual The older automation hold is now contained: the existing |
Vilin97
added
the
needs-maintainer
# Conflicts: # LeanPool/projects.yml
Vilin97
added
the
needs-manual-rebase
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "237c011ff604dd21d8b27a9f49c7986da1d4581c",
"verdict": "approve",
"assessment": "The four registered headlines faithfully prove discrete normality in every base b ≥ 2 and the two exact cohort-count formulas. Occurrences overlap, words are nonempty valid digit lists, and the card expressly limits its scope to digit sequences. The position-zero generalization of filter_blockAt_partial_congr is retained. This is a significant named theorem with reusable counting infrastructure; the exact-head five-rubric review has no findings.",
"source": "The credited pinned upstream formalization supports the discrete all-base theorem; the card accurately distinguishes it from the historical base-ten result.",
"validation": "CI run 36017676884 passed the full build, indexes, Lean linters, style and quality/trust audit at this SHA. Documentation and separation checks have now also completed successfully. No source changes or further author action are needed. Posted as COMMENT because the authenticated maintainer also authors this PR.",
"findings": []
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Current-main refresh reviewed at 231918dda2ddf707dd64859ac35fc1a00065a44e.
Merged main 0e9b057b62cc4eaa1b4a42cf23766cf7b9bd3537 while preserving all 9 project Lean files byte-for-byte from the previously reviewed head 01dad7a4e314b809492fc952f09c799c9a0cf99b. All 218 main project cards and this project's card retain their values and original bytes. The actual pinned mk_all --module --check passes, and the diff against main remains confined to this project, its registry entry, and the generated root index.
The prior substantive review recommendation carries forward unchanged. Fresh required CI at this merge head remains necessary; no additional compiler run was launched for unchanged project source.
Vilin97
removed
the
needs-maintainer
Vilin97
removed
the
needs-manual-rebase
Vilin97
added
the
needs-maintainer
Daily disposition: needs maintainer — protected merge operationReviewed exact head
The remaining authority boundary is operational: this repository has |
This branch has not been deployed
1 participant
Proves that concatenating the base-b digits of the positive integers gives a normal digit sequence for every b ≥ 2: each nonempty length-k word of valid digits has limiting frequency b⁻ᵏ, with overlapping occurrences counted. Preserves the substring-counting API, digit-string equivalence, exact cohort counts, and quantitative prefix bounds as reusable infrastructure. The card describes a discrete all-base theorem; it makes no additional claim about a real-number expansion bridge, irrationality, or transcendence.
Source and eligibility
31a76dbde2727745beb6fb81af4cab1ce6a15fda.6d526899e90104cbcc0d65dff1287adeab183b75). Both fall within this acquisition run’s half-open window, [2026-07-19 09:45:17 UTC, 2026-09-12 09:45:17 UTC). Eligibility does not rely on the later CI-only commit date.Import and port
Imports eight mathematical modules plus the project entry module, about 1,960 source lines. Retains every upstream mathematical declaration in that scope, including the useful optional exact-counting API. Excludes the upstream sandbox, comparator challenge and bridge, and build/CI scaffolding. There are no new package dependencies.
Ports to Lean 4.34.0 and Mathlib 5ed2965256430c3649e86755f9576b54eca72435. Adds the
Champernownenamespace and public module exports; removes a tactic continuation now closed by simplification; replaces deprecated lemmas and warning-producingshowtactics; renames two question-mark-containing identifiers for compatibility with the repository declaration audit. Theorem strength and base/digit hypotheses are unchanged. Refreshes stale upstream planning-document references, the project card, and generated index.Measured optimization
Controlled command:
lake build LeanPool.Champernowne, after deleting only this project’s.lake/build/lib/lean/LeanPool/Champernowne*and corresponding IR artifacts. Same WSL host (32 logical CPUs), toolchain, warm exact-revision Mathlib cache, and default Lake parallelism. Measurements include Lake startup; they are warm-dependency project builds, not cold full-pool builds.le_base_pow_count_boundaryproof heartbeatsle_base_pow_countOccurrences_champBlocksproof heartbeatsThe roughly 70–72% wall-time reduction comes from replacing
import Mathlibwith focused imports, using public module exports, narrowing the main import chain, moving a prefix lemma into its natural module so exact counts build independently, extracting the repeated cohort-error estimate, and consolidating the two exact cohort-sum proofs. Heartbeats were obtained with Lean’s trace profiler and divided by 1,000 to use Lean’s conventional heartbeat units; profiling overhead is excluded from build timings. The legacy heartbeat linter was also run but did not reliably measure proof bodies on this toolchain, so it is not the source of these figures. Remaining largest proof is under 7,000 measured heartbeats; no heartbeat/recursion overrides are present.Validation
lake exe mk_all --check.runLinter --no-buildexplicitly over all nine imported modules.lake exe lint-style LeanPool.Champernowne.git diff --check; content-only scope. No Python code, CI, review policy, quality checker, linter settings, or waivers changed.Maintainer repair and current validation
Commit
2cc87eed5829cc29be2361d5e41a6b5e29218407removes an unused positive-position premise fromfilter_blockAt_partial_congr, so its proven conversion also applies at position zero. Its caller and docstring are updated; the four project headlines are unchanged.The repaired tree passed the targeted build, all nine module linters, style/index checks, textual/card checks and the complete project axiom/backdoor audits. Full CI, documentation and the complete five-rubric GPT-6-Astra/xhigh review passed at
2cc87eed5829cc29be2361d5e41a6b5e29218407; the review has no findings. The existing Azure worker is reachable. The manually disabled workflow and VM configuration remain unchanged.The maintainer blocker is resolved and this PR is ready for review. It remains unmerged while behind
main, as required by branch protection. Disposition and validation evidence.