{"schema_version":1,"research_id":"eoa_inverse_innovation_exp06_external_evaluation_20260803","source_assessment_id":"representation_independent_interface_contract__mathematics:P1:v0","cell_id":"representation_independent_interface_contract__mathematics","search_queries":["site:github.com/leanprover-community/mathlib4 issue Polynomial representation finsupp performance","site:leanprover-community.github.io/mathlib4_docs MvPolynomial Basic finsupp","formalized mathematics polynomial representation change proof library abstraction interface","site:github.com/leanprover-community/mathlib4 polynomial implementation detail coeff ext","site:leanprover-community.github.io/archive polynomial representation mathlib change representation","site:github.com/leanprover-community/mathlib4/issues \"Polynomial\" \"representation\"","site:github.com/leanprover-community/mathlib4/pulls MvPolynomial performance representation","proof assistant abstract data type representation independence theorem library polynomial","proof assistant library abstraction barriers representation change breaks proofs study","formal proof maintenance definition unfolding representation dependence paper","Coq polynomial abstract interface multiple representations formalization","Isabelle polynomial representations code equations abstract transfer","site:leanprover-community.github.io/contribute implementation details API abstraction mathlib","site:leanprover-community.github.io/mathlib4_docs \"implementation detail\" polynomial","site:github.com/leanprover-community/mathlib4 \"implementation detail\" \"Polynomial\"","site:leanprover-community.github.io/archive MvPolynomial computable implementation performance","site:leanprover-community.github.io/mathlib4_docs Plausible property based testing","Lean 4 property based testing Plausible mathlib documentation","site:leanprover-community.github.io/mathlib4_docs testing framework random generators","site:github.com/leanprover-community/mathlib4 Plausible testable","site:github.com/isabelle-prover/mirror-isabelle Polynomial.thy code abstract coeffs","Isabelle Polynomial.thy github HOL Computational Algebra Polynomial","site:isabelle.in.tum.de \"code abstract\" \"coeffs 0\" polynomial","Isabelle polynomial abstract type coefficients implementation official"],"sources":[{"source_id":"S1","title":"Mathlib.Algebra.MvPolynomial.Basic","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MvPolynomial/Basic.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"undated; accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib defines multivariate polynomials directly as finitely supported coefficient functions, (σ →₀ ℕ) →₀ R.","The public documentation exposes coefficient lookup, monomial construction, ring operations, support, and coefficient extensionality.","The current mathlib representation is not the normalized ordered pair-list posited by the candidate."]},{"source_id":"S2","title":"Mathlib.Algebra.Polynomial.Basic","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Polynomial/Basic.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"undated; accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib's univariate Polynomial is an irreducible structure wrapping a finitely supported coefficient representation.","Its documentation says raw representation conversions generally should not be used once the polynomial API is constructed.","This is close prior art for hiding polynomial representation behind coefficient-level operations and lemmas."]},{"source_id":"S3","title":"Groebner bases discussion","publisher":"Lean/mathlib community Zulip archive","url":"https://leanprover-community.github.io/archive/stream/113488-general/topic/Groebner.20bases.html","source_class":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2023-06-23","accessed_at":"2026-08-03","claims_supported":["Mathlib contributors expressed a concrete need for performant, computable multivariate-polynomial implementations.","Participants stated that different representations are natural for different algorithms and that the current finitely supported-function representation is a poor computational data structure.","The discussion supports stakeholder interest in alternative representations, but not commitment to the proposed interface pilot."]},{"source_id":"S4","title":"Code generation from Isabelle/HOL","publisher":"Isabelle project, Technical University of Munich","url":"https://www.isabelle.in.tum.de/website-Isabelle2021/dist/Isabelle2021/doc/codegen.pdf","source_class":"OFFICIAL_GUIDANCE","publication_date":"2021","accessed_at":"2026-08-03","claims_supported":["Isabelle documents datatype refinement using abstract and concrete types, conversion/projection functions, representation invariants, and certified primitive-operation equations.","The manual demonstrates substituting an amortized queue representation and generating code behind an abstract signature.","The proposed invariant-and-abstraction-function workflow is established proof-assistant practice."]},{"source_id":"S5","title":"Internalizing Representation Independence with Univalence","publisher":"ACM SIGPLAN POPL / arXiv","url":"https://arxiv.org/abs/2009.05547","source_class":"PRIMARY_RESEARCH","publication_date":"2020-09-11","accessed_at":"2026-08-03","claims_supported":["Representation-independence metatheorems establish interchangeability of implementations related by an operation-preserving correspondence.","The paper formalizes transfer across implementations in Cubical Agda and applies it to matrices, queues, and finite multisets.","Formal representation-independent substitution is established research rather than a novel general mechanism."]},{"source_id":"S6","title":"Plausible.Testable","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/mathlib4_docs/Plausible/Testable.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"undated; accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Lean's Plausible framework generates counterexamples for testable propositions and shrinks failing cases.","It supports custom generators for newly defined types and bounded randomized property checks.","The candidate's bounded executable algebraic testing is technically supported, although passing samples does not prove universal correctness."]},{"source_id":"S7","title":"How to contribute to mathlib","publisher":"Lean/mathlib community","url":"https://leanprover-community.github.io/contribute/how-to-contribute.html","source_class":"OFFICIAL_GUIDANCE","publication_date":"undated; accessed 2026-08-03","accessed_at":"2026-08-03","claims_supported":["Mathlib maintainers approve production changes after CI passes.","Experimental work can be developed on a separate branch or fork before a production pull request.","Maintainers are identifiable authorizers, but the source contains no authorization or funding for this candidate."]},{"source_id":"S8","title":"Executable Multivariate Polynomials","publisher":"Archive of Formal Proofs","url":"https://devel.isa-afp.org/entries/Polynomials.html","source_class":"PRIMARY_RESEARCH","publication_date":"2010-08-10","accessed_at":"2026-08-03","claims_supported":["The Archive of Formal Proofs contains a longstanding formalization of executable multivariate polynomials over arbitrary ordered semirings.","It implements addition, multiplication, substitution, comparison, and polynomial-order results.","Executable alternative polynomial formalizations are mature prior art."]}],"problem_evidence":{"support":"WEAK","rationale":"A visible computational problem exists: mathlib contributors report that its finitely supported-function MvPolynomial is unsuitable for many algorithms and that different algorithms favor different representations (S3). However, the candidate does not identify the allegedly ordered-list-based library or provide the proposed 20-lemma dependency audit. The closest identifiable library, mathlib, instead defines MvPolynomial as a finitely supported coefficient function and already supplies coefficient/extensional APIs (S1). Thus the exact claimed proof breakage, prevalence, and consequence remain unverified.","source_ids":["S1","S3"]},"stakeholder_evidence":{"support":"WEAK","rationale":"Mathlib contributors have expressed interest in computable, algorithm-specific polynomial representations (S3), and mathlib maintainers are identifiable production authorizers (S7). No maintainer, downstream theorem owner, or funder was found requesting this particular opaque-contract/conformance-suite pilot, allocating resources, or accepting its migration costs.","source_ids":["S3","S7"]},"prior_art":{"proximity":"ESTABLISHED_PRACTICE","closest_analogues":[{"name":"Mathlib MvPolynomial coefficient-function model","similarity":"It already models a multivariate polynomial as a finitely supported function from exponent vectors to coefficients and provides coefficient lookup, extensional equality, constructors, and ring laws—the candidate's proposed abstract mathematical meaning and most of its observable vocabulary.","remaining_difference":"MvPolynomial is documented as a reducible abbreviation over AddMonoidAlgebra rather than a representation-opaque interface parameterized over independently implemented backends; no shared two-backend theorem-corpus gate was found.","source_ids":["S1"]},{"name":"Mathlib Polynomial irreducible wrapper and API","similarity":"It wraps a finitely supported representation in a kernel-irreducible structure and explicitly discourages use of raw conversions after the API is constructed.","remaining_difference":"It concerns univariate polynomials and a single implementation, not a sparse-map/list substitution trial with a common 20-theorem corpus.","source_ids":["S2"]},{"name":"Isabelle datatype refinement","similarity":"It uses abstract types, concrete representations, projections, invariants, certified operations, and representation-specific code equations while preserving an abstract interface.","remaining_difference":"It is a generic proof-assistant refinement mechanism rather than the candidate's exact Lean multivariate-polynomial contract and leakage-review workflow.","source_ids":["S4"]},{"name":"Formal representation independence and theorem transfer","similarity":"It formally connects multiple implementations through operation-preserving relations and transfers correctness results between them.","remaining_difference":"The cited research uses univalence, higher inductive types, and Cubical Agda; the candidate proposes ordinary opaque modules, abstraction proofs, and black-box theorem/test suites in an unspecified library.","source_ids":["S5"]},{"name":"AFP Executable Multivariate Polynomials","similarity":"It is a mature executable multivariate-polynomial development with formal operations and laws.","remaining_difference":"The entry does not establish the candidate's specific claim that the same preselected downstream theorem proofs can be reused unchanged across two opaque implementations.","source_ids":["S8"]}],"distinctive_claim_remaining":"Within one named formal library and a predeclared corpus of 20 representation-independent polynomial lemmas, a coefficient-function interface plus enforced opacity and one shared conformance oracle will let both a wrapper over the incumbent representation and an independently written sparse-map implementation re-establish the identical theorem statements without either proof accessing representation-specific definitions. This corpus-level result is contrastive and falsifiable, but it is an implementation benchmark, not demonstrated world novelty.","confidence":"HIGH"},"implementation_evidence":{"support":"STRONG","rationale":"All central mechanisms are technically credible: mathlib already has the proposed coefficient-function semantics and extensional API (S1), an irreducible polynomial wrapper pattern (S2), property-based counterexample generation and shrinking (S6), and an established branch/CI workflow (S7). Isabelle documents invariant-preserving abstract datatype refinement (S4), while prior research and AFP artifacts show formal representation independence and executable polynomial developments (S5, S8). Remaining feasibility questions are workflow-specific: whether Lean opacity prevents every relevant proof reach-through, whether the exact theorem statements are sufficiently abstract, and how much proof duplication is required.","source_ids":["S1","S2","S4","S5","S6","S7","S8"]},"scores":{"meaningful_impact":{"score":3,"rationale":"Alternative polynomial representations plausibly matter for executable algebra, but the claimed downstream proof-rewrite burden and affected corpus have not been observed in a named library.","source_ids":["S1","S3"]},"stakeholder_pull":{"score":2,"rationale":"Contributors express demand for different computable representations, but no adopter or funder has requested this intervention.","source_ids":["S3","S7"]},"incremental_advantage":{"score":2,"rationale":"The bounded shared-theorem-corpus gate could add disciplined evidence beyond a single representation's API, but most proposed mechanisms already exist independently in mathlib, Isabelle, and representation-independence research.","source_ids":["S1","S2","S4","S5"]},"distinctiveness_plausibility":{"score":1,"rationale":"The general pattern is established practice; only the exact two-implementation, 20-lemma benchmark remains potentially distinctive.","source_ids":["S1","S2","S4","S5","S8"]},"technical_implementability":{"score":4,"rationale":"Existing coefficient models, opaque wrappers, refinement proofs, executable polynomial libraries, and property-based testing make an isolated prototype technically credible.","source_ids":["S1","S2","S4","S6","S8"]},"adoption_authority_feasibility":{"score":3,"rationale":"Maintainers are clearly the production authorizers and isolated branch work is permitted, but no authorization for this pilot was found.","source_ids":["S7"]},"evidence_readiness":{"score":2,"rationale":"The experiment is well bounded, but it lacks a named target library, frozen lemma corpus, dependency inventory, authorizer commitment, and measured baseline.","source_ids":["S1","S3","S7"]},"safety_net_benefit":{"score":4,"rationale":"A separate branch/namespace, unchanged production definitions, identical theorem statements, and rollback on semantic divergence create a strong reversible safety net.","source_ids":["S7"]},"scalability":{"score":3,"rationale":"A reusable abstract interface can scale across implementations, but proof obligations, generators, and theorem-port work are algebra- and library-specific; no scaling measurements exist.","source_ids":["S4","S5","S6"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"Freeze and audit 20 lemmas, specify the coefficient-function interface, construct an incumbent wrapper and minimal sparse-map backend, and run the first theorem/property comparison in an isolated branch.","confidence":"LOW","assumptions":["One experienced Lean/formal-algebra engineer for roughly 4–8 weeks.","The 20 lemmas are already selected and compile in a reproducible target revision.","No production migration or general-purpose performance engineering is included.","No external compensation or wage source was found; this is a resource-equivalent estimate."],"source_ids":["S1","S6","S7"]},"initial_deployment_startup":{"band_2026_usd":"50K_TO_250K","scope":"Harden the interface and both backends, complete abstraction proofs, expand edge-case generators, document the contract, and obtain maintainer review for a bounded non-production package.","confidence":"LOW","assumptions":["Two skilled contributors for approximately 3–6 months combined.","Review findings require ordinary revisions rather than redesigning Lean abstractions or polynomial semantics.","The scope remains a standalone or experimental package."],"source_ids":["S4","S6","S7"]},"operational_launch":{"band_2026_usd":"250K_TO_1M","scope":"Integrate a production-quality abstraction into a major formal library, migrate an agreed theorem subset, add compatibility/deprecation tooling, benchmark implementations, and pass maintainer CI/review.","confidence":"LOW","assumptions":["Approximately 1–3 formalization engineer-years including review and migration effort.","Production adoption is authorized after the pilot.","The launch does not attempt to migrate every polynomial theorem or remove the incumbent public type immediately.","The range reflects uncertainty from the missing dependency audit and target-library decision."],"source_ids":["S1","S2","S3","S7"]},"annual_recurring":{"band_2026_usd":"10K_TO_50K","scope":"Maintain the contract, shared conformance suite, generators, compatibility checks, documentation, and review of proposed representation leaks.","confidence":"LOW","assumptions":["Roughly 0.1–0.3 experienced contributor FTE annually.","Only two or a few implementations are supported.","Major semantic or toolchain migrations would be separately funded."],"source_ids":["S6","S7"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"NO","reason":"The exact ordered-list library, representation-dependent 20-lemma corpus, and observed proof failures are not identified or externally documented. Available evidence supports a related computational-representation problem but also shows that mathlib already uses the proposed coefficient-function meaning.","source_ids":["S1","S3"]},"externally_credible_adopter_or_authorizer":{"status":"UNCERTAIN","reason":"Mathlib maintainers are credible authorizers and contributors want alternative computable polynomial representations, but no maintainer or theorem owner has expressed intent to adopt or fund this candidate.","source_ids":["S3","S7"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The claim names two implementations, a frozen 20-lemma corpus, a public vocabulary, and an observable pass/fail outcome: identical statements reproved without representation access.","source_ids":["S1","S2","S4"]},"bounded_next_evidence_step":{"status":"YES","reason":"An isolated branch with 20 preselected lemmas, one incumbent wrapper, one sparse-map backend, one finite ring, fixed exponent limits, and recorded failures is bounded and reversible.","source_ids":["S6","S7"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The authorized experimental form can remain on a separate branch or fork, avoids changing production definitions, and can be deleted without user-facing migration. Production replacement would require a later maintainer decision.","source_ids":["S7"]},"credible_cost_scope_and_range":{"status":"UNCERTAIN","reason":"The work packages are bounded, but no target-library dependency inventory, staffing quote, compensation benchmark, or maintainer estimate was found; all monetary bands are low-confidence resource equivalents.","source_ids":["S1","S3","S7"]}},"next_evidence_step":"After naming the target library and obtaining permission from its relevant maintainers, freeze exactly 20 existing polynomial lemmas and the target revision before implementation. Audit whether each proof uses only coefficient/evaluation/ring vocabulary or unfolds representation. Comparator A is the unchanged incumbent proofs/API; comparator B is a one-time coefficient-lemma rewrite without a new abstraction; the intervention arm is one shared opaque interface instantiated by an incumbent wrapper and an independently coded sparse map. Require identical theorem statements, zero representation-specific imports or escape hatches in intervention proofs, agreement of every queried coefficient and evaluation over a predeclared finite ring and exponent bound, and all shared algebraic properties to pass. Falsify the problem if the audit finds no representation-dependent proof or the existing API already permits backend replacement locally. Falsify the intervention if either backend needs representation access, any theorem statement changes, an abstract result diverges, or the intervention requires more proof edits than comparator B. This step requires live formalization and cannot be resolved by further bounded web search.","blocking_evidence":["No real target library is named for the alleged normalized ordered-list representation.","No externally inspected 20-lemma dependency inventory or baseline failure log exists.","No maintainer, downstream theorem owner, or funder has committed to the pilot.","No live ordered-list wrapper, independent sparse-map implementation, abstraction proofs, or shared-suite results exist.","No measured proof-edit count, compile-time cost, runtime performance, or review burden exists.","No externally grounded labor-rate or project estimate supports the 2026-USD bands."],"research_disposition":"KNOWN_PRACTICE_DIFFUSION","world_novelty_boundary":"The search establishes only that coefficient-function polynomial semantics, API-based representation hiding, datatype refinement, executable polynomial implementations, property-based testing, and formal representation independence already exist. It does not measure world novelty of the exact 20-lemma/two-backend experiment, patentability, freedom to operate, market size, realized impact, or exhaustive prior art.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Name the actual library and obtain written maintainer or theorem-owner interest in the isolated pilot.","Freeze and publish the 20-lemma corpus, target revision, dependency classifications, and baseline proof-failure counts.","Implement both backends and the public-only shared suite with comparators and falsifiers fixed before results are observed.","Report theorem-statement changes, proof-edit counts, escape hatches, semantic divergences, compile/runtime costs, and property-test counterexamples.","Replace resource-equivalent cost assumptions with a contributor estimate grounded in the audited corpus."],"reason":"Web evidence shows a real adjacent demand for alternative computable polynomial representations, but the candidate's general mechanism substantially collides with established practice and its only remaining incremental claim is a library-specific corpus-level substitution result. That result requires proprietary-to-the-project dependency data and live Lean implementation/testing, so additional bounded web research cannot resolve it."},"proposal_index":1}