{"schema_version":1,"research_id":"eoa_inverse_innovation_exp06_external_evaluation_20260803","source_assessment_id":"catalytic_pathway_enablement__mathematics:P3:v0","cell_id":"catalytic_pathway_enablement__mathematics","search_queries":["site:github.com/leanprover-community/mathlib4/issues matrix linear map theorem counterpart basis toMatrix","site:leanprover-community.github.io/mathlib4_docs LinearMap.toMatrix Matrix.toLin","site:leanprover-community.github.io mathlib matrix linear map basis equivalence theorem","formalized mathematics proof maintenance library automation theorem transport representations matrices linear maps","site:github.com/leanprover-community/mathlib4/issues \"toMatrix\" theorem","site:github.com/leanprover-community/mathlib4/pulls \"toMatrix\" linear map matrix theorem","site:leanprover.zulipchat.com toMatrix matrix linear map theorem mathlib","site:github.com/leanprover-community/mathlib4 \"Matrix.toLin\" \"LinearMap.toMatrix\"","Lean mathlib transport theorem across equivalence tactic equiv_rw","site:leanprover-community.github.io/mathlib4_docs transport equivalence tactic theorem","site:github.com/leanprover-community/mathlib4 \"equiv_rw\"","Lean theorem transfer package transport across isomorphism matrix linear map","site:leanprover-community.github.io/contribute mathlib maintainers review automation contributor burden","site:leanprover-community.github.io/mathlib4_docs \"to_dual\" automatically transport theorems","site:github.com/leanprover-community/mathlib4/issues \"matrix\" \"linear map\"","site:github.com/leanprover-community/mathlib4/issues basis matrix theorem linear algebra","site:lean-lang.org theorem proving Lean kernel checks proof official","site:lean-lang.org/doc/reference/latest trusted kernel theorem proving Lean","site:lean-lang.org/doc/reference/latest tactics generated proof kernel checked","Lean 4 trusted kernel elaborator generated proof official documentation","site:bls.gov/ooh computer information technology software developers median pay 2025","site:bls.gov/oes 15-1252 software developers May 2025 wage","BLS software developers occupational outlook handbook median annual wage May 2024","github mathlib4 pull request LinearMap.toMatrix matrix theorem","github mathlib4 issue Matrix.toLin linear map","github mathlib4 PR toMatrix_comp theorem","github leanprover community mathlib Matrix.toLin theorem counterpart","https://api.github.com/search/issues?q=repo%3Aleanprover-community%2Fmathlib4+toMatrix+is%3Aissue","https://api.github.com/search/issues?q=repo%3Aleanprover-community%2Fmathlib4+%22linear+map%22+matrix+is%3Aissue","https://api.github.com/search/issues?q=repo%3Aleanprover-community%2Fmathlib4+toMatrix+is%3Apr"],"sources":[{"source_id":"S1","title":"Mathlib.LinearAlgebra.Matrix.ToLin","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/ToLin.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"Undated; current documentation accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib already defines basis-indexed linear equivalences between matrices and linear maps.","The implementation includes inverse laws and preservation lemmas for identity, composition, multiplication, powers, reindexing, kernels, and ranges.","The proposal's central mathematical facilitator and much of its supported-operation grammar already exist."]},{"source_id":"S2","title":"Maths in Lean: linear algebra","publisher":"Lean/mathlib community","url":"https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/templates/theories/linear_algebra.md","source_class":"OFFICIAL_GUIDANCE","publication_date":"Undated; current guide accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib deliberately supports both matrix and linear-map representations.","The guide says matrices are suited to entrywise computation while linear maps are suited to coordinate-free proofs.","Explicit bases are required for the general matrix–linear-map equivalence, supporting the proposal's basis-safety boundary."]},{"source_id":"S3","title":"Mathlib.Tactic.Translate.ToDual","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Translate/ToDual.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"Undated; current documentation accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib already automatically generates transported theorem and definition declarations for a supported representation-changing translation.","The mechanism handles name mappings, reordered arguments, self-translations, and existing target declarations.","This is a close operational analogue to a versioned theorem-counterpart generator."]},{"source_id":"S4","title":"The transport tactic","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib_docs/tactic/transport.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"Legacy mathlib3 documentation; accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Legacy mathlib implemented generic transport of structures and goals across equivalences using equiv_rw.","The tool could leave subgoals when preservation support was incomplete, illustrating the need for an eligibility boundary and supporting lemmas.","The page is explicitly legacy and does not establish availability of the same tactic in current mathlib4."]},{"source_id":"S5","title":"Contributing to mathlib","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/contribute/index.html","source_class":"OFFICIAL_GUIDANCE","publication_date":"2026","accessed_at":"2026-08-03","claims_supported":["Mathlib maintainers determine fit and maintainability for contributions and are the identifiable authorizing group.","The guide reports more than 2,600 open pull requests in mid-2026 and warns that review and merging can take time.","The project requires expert supervision, maintainability, integration, and human understanding of generated code, limiting unattended adoption."]},{"source_id":"S6","title":"Lean Language Reference: Tactic Proofs","publisher":"Lean FRO","url":"https://lean-lang.org/doc/reference/latest/Tactic-Proofs/","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"Current reference accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Lean tactics construct proof terms that the kernel independently checks.","A tactic bug cannot by itself make the kernel accept an invalid proof term.","Kernel checking establishes formal type correctness, not whether the generated theorem statement captures the intended counterpart."]},{"source_id":"S7","title":"Maintaining a Library of Formal Mathematics","publisher":"arXiv / CICM proceedings authors","url":"https://arxiv.org/abs/2004.03673","source_class":"PRIMARY_RESEARCH","publication_date":"2020-05-26","accessed_at":"2026-08-03","claims_supported":["Mathlib's authors identify contributor entry barriers and review burden as material library-maintenance problems.","Mathlib already develops automated checks and documentation tools to reduce those burdens.","This supports the general value of reusable proof-engineering infrastructure but does not quantify matrix–linear-map transport frequency."]},{"source_id":"S8","title":"Software Developers, Quality Assurance Analysts, and Testers","publisher":"U.S. Bureau of Labor Statistics","url":"https://www.bls.gov/ooh/computer-and-information-technology/software-developers.htm","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2025-08-28","accessed_at":"2026-08-03","claims_supported":["The May 2024 U.S. median annual wage was $133,080 for software developers and $102,610 for software QA analysts and testers.","These wage benchmarks support resource-equivalent labor estimates, subject to specialist premiums, benefits, and volunteer-project economics."]}],"problem_evidence":{"support":"WEAK","rationale":"Official sources confirm that mathlib intentionally maintains both representations, that explicit bases mediate their equivalence, and that formal-library contribution and review burden matters. The ToLin file's many hand-authored preservation and correspondence lemmas make recurring representation work plausible. However, the searches did not find an external issue set, case audit, or measured queue showing repeated unmet requests for matrix/linear-map counterpart theorems. The proposal's exact prevalence and consequence therefore remain unverified.","source_ids":["S1","S2","S5","S7"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"Mathlib maintainers are an identifiable authorizing and adopting group, and official guidance expresses pressure around maintainability, expert review, and more than 2,600 open PRs. The maintenance paper also explicitly seeks tools that lower contributor and reviewer burden. No source expressed a specific request for this matrix–linear-map gateway, so stakeholder pull is general rather than solution-specific.","source_ids":["S5","S7"]},"prior_art":{"proximity":"SUBSTANTIAL_COLLISION","closest_analogues":[{"name":"Mathlib Matrix.toLin / LinearMap.toMatrix equivalence and preservation-lemma suite","similarity":"Provides the proposal's reusable facilitator, inverse laws, explicit-basis interface, and transport laws for many named operations.","remaining_difference":"It exposes mathematical equivalences and lemmas rather than a declaration-level gateway that generates, screens, logs, versions, benchmarks, and withdraws counterpart theorems.","source_ids":["S1","S2"]},{"name":"Mathlib @[to_dual] declaration translator","similarity":"Automatically translates theorem and definition declarations across a controlled correspondence, including names and argument reordering.","remaining_difference":"It targets order duality through a global translation dictionary, not explicit-basis matrix–linear-map equivalence or the proposed eligibility, fidelity-review, and regeneration protocol.","source_ids":["S3"]},{"name":"Legacy mathlib3 transport/equiv_rw","similarity":"Transports mathematical structures and goals across equivalences and relies on supporting congruence or simp lemmas.","remaining_difference":"It is legacy, targets generic structure/goal transport, and does not provide current matrix-specific counterpart declaration management.","source_ids":["S4"]},{"name":"Manual use of documented matrix–linear-map equivalences","similarity":"Contributors can already choose explicit bases, invoke toMatrix/toLin, and use preservation lemmas to derive counterparts.","remaining_difference":"The proposal adds a bounded grammar, automatic target-statement construction, standardized rejection, telemetry, and version-regression lifecycle.","source_ids":["S1","S2"]}],"distinctive_claim_remaining":"For an explicitly bounded theorem grammar, a matrix–linear-map-specific declaration gateway can combine existing equivalences and preservation lemmas into faithful, kernel-accepted counterpart declarations with materially less total author-plus-reviewer work than best-practice manual transport, while rejecting every basis-sensitive or unsupported case and imposing acceptable proof-size, checking-time, and maintenance overhead. No searched source established that integrated workflow or its performance.","confidence":"HIGH"},"implementation_evidence":{"support":"STRONG","rationale":"The mathematical equivalence, inverse laws, and numerous operation-preservation lemmas already exist, and mathlib demonstrates automatic declaration translation in to_dual. Lean's kernel can check generated proof terms independently. The remaining engineering is primarily syntax traversal, explicit-basis contracts, proof-term construction, eligibility diagnostics, regression tests, and lifecycle integration. Important feasibility limits remain: theorem statements are dependently typed and heterogeneous; generic transport can leave obligations; kernel acceptance does not establish intended statement fidelity; and maintainers require expert-supervised, maintainable output.","source_ids":["S1","S3","S4","S5","S6"]},"scores":{"meaningful_impact":{"score":2,"rationale":"Formal-library review burden is real, but the affected matrix–linear-map counterpart volume and delay are not externally measured.","source_ids":["S5","S7"]},"stakeholder_pull":{"score":2,"rationale":"Maintainers are credible authorizers and express general review pressure, but no direct request or committed sponsor for this gateway was found.","source_ids":["S5","S7"]},"incremental_advantage":{"score":2,"rationale":"The equivalence, preservation lemmas, generic equivalence transport, and declaration translation patterns already exist; advantage is workflow integration and measured fidelity rather than a new transport mechanism.","source_ids":["S1","S3","S4"]},"distinctiveness_plausibility":{"score":2,"rationale":"A matrix-specific guarded declaration gateway is contrastively describable, but it substantially composes established mathlib facilities.","source_ids":["S1","S3","S4"]},"technical_implementability":{"score":4,"rationale":"Existing equivalences, inverse laws, operation lemmas, metaprogramming precedents, and kernel checking make a bounded prototype credible.","source_ids":["S1","S3","S6"]},"adoption_authority_feasibility":{"score":3,"rationale":"Mathlib maintainers can authorize integration or recommend a standalone dependency, but high review load and strict maintainability standards create a material adoption hurdle.","source_ids":["S5"]},"evidence_readiness":{"score":2,"rationale":"The proposed archive benchmark is bounded, but no external prevalence audit, archived-pair corpus, prototype results, or maintainer commitment was found.","source_ids":["S5","S7"]},"safety_net_benefit":{"score":3,"rationale":"Kernel checking, explicit bases, rejection, and human fidelity review can constrain failures, although kernel checking and ordinary review already exist and statement-intent errors remain possible.","source_ids":["S2","S5","S6"]},"scalability":{"score":3,"rationale":"Reusable syntax and preservation rules could scale across routine statements, but basis sensitivity, dependent types, unsupported predicates, proof-term growth, and version drift bound coverage.","source_ids":["S1","S3","S4"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"Build an isolated prototype for the initial grammar; curate 10 eligible and 2 deliberately ineligible archived pairs; execute manual and gateway comparators; conduct blinded fidelity review; and test one simulated API-change regeneration cycle.","confidence":"MODERATE","assumptions":["Approximately 4–10 specialist person-weeks across Lean implementation, corpus preparation, blinded review, and analysis.","Existing mathlib equivalence and preservation lemmas are reused rather than reimplemented.","No live-library merge or production support is included.","BLS software-developer and QA wages are labor anchors; Lean specialists and fully loaded costs may exceed them."],"source_ids":["S1","S8"]},"initial_deployment_startup":{"band_2026_usd":"50K_TO_250K","scope":"Harden syntax traversal and diagnostics, expand regression coverage, document the contract, add CI/version withdrawal behavior, obtain security and maintainability review, and prepare a standalone package or mathlib-quality pull request.","confidence":"LOW","assumptions":["Roughly 0.4–1.2 specialist FTE-years including reviewer and steward time.","Scope remains limited to finite-dimensional matrix–linear-map transport and a small operation grammar.","The estimate excludes a general-purpose theorem-translation framework and major upstream API redesign.","Mathlib's review queue may increase elapsed time without equivalent paid labor."],"source_ids":["S1","S3","S5","S8"]},"operational_launch":{"band_2026_usd":"10K_TO_50K","scope":"Release one approved gateway version, train or document use for contributors, validate initial projects, establish incident and withdrawal procedures, and staff launch-period review.","confidence":"LOW","assumptions":["No automatic merging of generated declarations.","Launch initially supports a small number of expert contributors.","Compute costs are minor relative to expert review and integration labor.","Ordinary mathlib review remains mandatory."],"source_ids":["S5","S6","S8"]},"annual_recurring":{"band_2026_usd":"10K_TO_50K","scope":"Maintain the equivalence dictionary and grammar, replay regressions after relevant API changes, triage rejected cases, monitor proof size and checking time, refresh documentation, and perform periodic fidelity audits.","confidence":"LOW","assumptions":["Approximately 0.1–0.3 specialist FTE plus CI compute and reviewer time.","One stable bounded grammar is maintained; broad representation-generalization is excluded.","Major Lean or mathlib representation changes could temporarily push costs above this band.","Volunteer labor is counted at resource-equivalent market value."],"source_ids":["S5","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"UNCERTAIN","reason":"General contributor/reviewer burden and the coexistence of both representations are externally supported, but no direct audit establishes recurring counterpart requests, manual transport burden, or divergence at meaningful frequency.","source_ids":["S1","S2","S5","S7"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"Mathlib maintainers are an identifiable authorizing group for library integration, and official guidance describes their maintainability and review role; a standalone dependent repository is also an explicitly recognized route.","source_ids":["S5"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The remaining claim compares an integrated guarded gateway against current manual use of equivalences and lemmas on total work, fidelity, rejection, proof size, checking time, and regeneration performance.","source_ids":["S1","S3","S4"]},"bounded_next_evidence_step":{"status":"YES","reason":"A 12-pair concealed archival benchmark with manual and existing-tool comparators, blinded review, adverse cases, fixed thresholds, and a simulated API change is bounded and reversible.","source_ids":["S1","S6"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"A non-exported archival experiment can retain kernel checking and human review, merge nothing, use no sensitive data, and stop on any statement mismatch. Live adoption still requires maintainer authorization.","source_ids":["S5","S6"]},"credible_cost_scope_and_range":{"status":"YES","reason":"The work can be scoped in specialist person-weeks or FTE fractions and anchored to government wage data, though Lean-specialist premiums and volunteer-project review latency create substantial uncertainty.","source_ids":["S8"]}},"next_evidence_step":"With a mathlib maintainer or designated linear-algebra reviewer, freeze one current mathlib commit and pre-register a 12-case archival trial: 10 accepted matrix/linear-map theorem pairs spanning equality, zero, addition, scalar multiplication, identity, and composition, plus two entry- or basis-order-sensitive cases that must be rejected. Conceal target declarations and randomize eligible cases between (A) the proposed gateway and (B) best-practice manual transport using current toMatrix/toLin, simp, convert, and available preservation lemmas; record whether generic equivalence transport offers a usable third comparator. Give both contributors identical source theorems, bases, and environment. Require all eligible outputs to kernel-check and pass blinded reviewer comparison of quantifiers, assumptions, conclusions, explicit bases, readability, and naming; require both adverse cases to be rejected before elaboration. Measure author time, reviewer time, elapsed time, manual edits, failures, proof-term size, elaboration/checking time, and diagnostic quality. After six cases, simulate a non-live API rename or preservation-lemma change and test withdrawal, regression replay, and recovery. Treat the incremental claim as supported only if the gateway reduces median total human time by at least 30% versus the manual comparator, has zero semantic or basis mismatches, rejects both adverse cases, keeps median proof size and checking time below twice the comparator, and restores the regression suite within one specialist day. Falsify or redesign if any unintended statement passes, an adverse case is accepted, median total work is not at least 20% lower, more than 30% of the representative eligible set requires unplanned repair, or regeneration exceeds the precommitted bound. This experiment authorizes no live merge or grammar expansion.","blocking_evidence":["No external count or representative audit of requested matrix–linear-map counterpart theorems was found.","No measured baseline for manual coordinate setup, proof assembly, repair, or reviewer burden was found.","No maintainer, reviewer, or funder was found expressing solution-specific demand or willingness to steward the gateway.","No prototype evidence establishes statement fidelity, eligible-case coverage, proof-term size, checking cost, or diagnostic quality.","It is unknown whether current best-practice simp/convert scripts make most proposed transports too cheap to justify a gateway.","It is unknown whether a representative archived target-pair corpus can be curated without selection bias.","No live evidence establishes regeneration cost under real mathlib API evolution."],"research_disposition":"PARTNERED_RESEARCH_PROGRAM","world_novelty_boundary":"This evaluation measured only externally visible problem support, stakeholder authority, documented technical ingredients, close software/practice analogues, and testability through bounded web research. It did not measure world novelty, patentability, freedom to operate, market size, realized impact, or exhaustive unpublished/current development. The absence of a searched matrix-specific gateway is not a world-novelty finding.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Secure a named mathlib maintainer or linear-algebra reviewer to approve the frozen archival protocol and fidelity rubric.","Produce a representative, auditable prevalence sample of counterpart requests or duplicated manual transports and quantify complete author-plus-reviewer burden.","Implement the isolated bounded-grammar prototype and publish its exact supported operations, rejection rules, proof-term construction, and regression corpus.","Run the preregistered manual-versus-gateway benchmark with concealed targets, blinded statement review, two adverse cases, and fixed time, fidelity, proof-size, and checking-cost thresholds.","Demonstrate withdrawal and recovery after a controlled API change, including a measured regeneration cost and an enforced no-merge rollback."],"reason":"Web evidence establishes strong technical feasibility and substantial collision with existing equivalences and theorem-translation practices, but it does not establish the exact problem's prevalence or the gateway's incremental labor, fidelity, coverage, and maintenance advantage. Those questions require proprietary or curated archive data, expert field participation, and executable testing rather than more bounded web search."},"proposal_index":3}