Repository navigation
Conversation
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
(cherry picked from commit 315141c)
(cherry picked from commit c8c4bbc)
(cherry picked from commit e2e14c3)
(cherry picked from commit dfbb926)
(cherry picked from commit 3aeda2f)
Make the selected-root literal generator emit module headers and convert the Lean sources main gained after the original sweep. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Mark meta helpers in HexIntFactor.Export, give the intfactor tests and the polynomial Smith bench the meta imports their compile-time checks need, expose definitions that proofs and the compiler unfold, use private module imports in the ordered-function lint test, and drop private from leaf bench drivers whose public declarations mention those names. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…der (#10845) * feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
Reuse the original sweep's import all and meta import headers for chapters main has since rewritten, import the defining modules of documented and evaluated declarations, give the selected-root byte data the codec and Init.Data.Repr bodies its kernel proof reduces, and mark the PolyFast env linter meta. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
* perf: share certified parent isolation across real-root entries * bench: plot and profile actual root-enumeration pairs * perf: materialize root selector cache before filtering * bench: retain real-root cache comparisons and readiness concerns * perf: share factorization for reducible real-root groups * bench: retain reducible controls and paired performance ranges * test: cross-check cached exactification on reducible parents --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* docs: reconcile current Sturm evidence and auxiliary sign timing * docs: retain every Sturm finding and attribute saved sign profiles * docs: list quartic obligations and reconcile prerequisite dispositions * test: retain reproducible benchmark source comparison * test: pin compared benchmark revisions by commit identity --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
) * Complete Sturm and real-algebraic Phase-4 prerequisite audit * Allow focused native scalar evidence refresh * Supply current scalar observations and inherited Sturm depth sweeps * Share certified refinement and factorization across real roots of one parent * Retain totally real root observations and final readiness verification * Check reducible real-root fallback and clarify source-scoped observations * Record practical reducible-parent costs and fallback coverage * Align root-cache specification and restrict reducible cost claims --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* feat: expose SignDet semantics through the companion import * fix: retain explicit SignDet proof audit coverage after migration * fix: preserve benchmark freshness across proof module migration --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
…10864) Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Record BKR and Thom libraries through Phase 4 * Clarify upstream numeral defect and retained performance dispositions * Align evidence references with the public companion exports * Reconcile remaining evidence scope and repeated-work explanations --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory * Reuse supplied common-field irreducibility proofs Refs #10358 * Clarify supplied irreducibility checking and native search Refs #10358 * Record supplied common-field proof validation Refs #10358 * Bind supplied irreducibility checks to integrated main Refs #10358 * Scope supplied proofs and clarify certification diagnostics Refs #10358 * Record scoped proof regressions and inspectable evidence Refs #10358 * Document and identify supplied irreducibility failures Refs #10358 * Bind final irreducibility diagnostics and validation records * Clarify common-field proof priority and tighten refusal control * Record final scoped-instance review and tightened control --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* doc: assess SignDet companion declarations and polish their API * fix: include existing consumers and make SignDet review evidence reproducible --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
) * feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory * Reuse supplied common-field irreducibility proofs Refs #10358 * Clarify supplied irreducibility checking and native search Refs #10358 * Record supplied common-field proof validation Refs #10358 * Bind supplied irreducibility checks to integrated main Refs #10358 * Scope supplied proofs and clarify certification diagnostics Refs #10358 * Record scoped proof regressions and inspectable evidence Refs #10358 * Document and identify supplied irreducibility failures Refs #10358 * Bind final irreducibility diagnostics and validation records * Clarify common-field proof priority and tighten refusal control * Record final scoped-instance review and tightened control * Add matched probes for supplied RCF irreducibility construction cost * Emit complete inventories for the external proof collector * Record supplied-proof comparison and document native joint realization * Bind diagnostic documentation and inspected examples to their source * test(rcf): keep supplied-instance budget exhaustion terminal * docs(rcf): retain supplied-instance budget control evidence * feat(rcf): realize native shared-formula rows at one real point * docs(rcf): state native joint formula semantics and frozen replay gates * docs(rcf): expose native formula API and exact remaining replay boundary * docs(rcf): retain source-bound native formula proof and rendering records * Keep paired RCF diagnostics outside CI and tighten native API evidence * Bind post-review native proof and manual checks to committed sources * Clarify the single fixed coefficient and wrap native API documentation * Link historical RCF records to reviewed and clarified source bindings * test(rcf): realize successive native samples jointly * docs(rcf): retain successive sample conformance evidence * docs(rcf): connect successive sample validation records * test(rcf): require native computed rows in witness proofs * docs(rcf): bind computed-row marker validation * docs(rcf): record final marker build job counts * docs(rcf): retain final upstream integration validation --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* doc: record Sturm pair proof completion through Phase 5 * doc: reconcile merged sign readiness and distribution prerequisites * doc: clarify Sturm acceptance evidence and source coverage * doc: make Sturm acceptance evidence reproducible and precise * doc: track the direct Sturm oracle requirement under integration * Keep the scanner header correction for a separate source change --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* doc: prepare SignDet pair proof acceptance through Phase 5 * doc: record the merged native formula consumer milestone * doc: bind SignDet proof acceptance to executed conformance and public theorems * doc: complete SignDet theorem mapping and evidence scope --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* test: verify Sturm frontend signs with direct pinned FLINT fixtures * test: cover Sturm public query contracts and enforce oracle refusal controls * test: bind the expanded Sturm corpus and shared oracle source * test: guard Sturm upper endpoints and prepared certificate refusal * test: retain source bindings for complete Sturm replay controls * docs: distinguish source parent from the Sturm oracle PR base --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory * Reuse supplied common-field irreducibility proofs Refs #10358 * Clarify supplied irreducibility checking and native search Refs #10358 * Record supplied common-field proof validation Refs #10358 * Bind supplied irreducibility checks to integrated main Refs #10358 * Scope supplied proofs and clarify certification diagnostics Refs #10358 * Record scoped proof regressions and inspectable evidence Refs #10358 * Document and identify supplied irreducibility failures Refs #10358 * Bind final irreducibility diagnostics and validation records * Clarify common-field proof priority and tighten refusal control * Record final scoped-instance review and tightened control * Add matched probes for supplied RCF irreducibility construction cost * Emit complete inventories for the external proof collector * Record supplied-proof comparison and document native joint realization * Bind diagnostic documentation and inspected examples to their source * test(rcf): keep supplied-instance budget exhaustion terminal * docs(rcf): retain supplied-instance budget control evidence * feat(rcf): realize native shared-formula rows at one real point * docs(rcf): state native joint formula semantics and frozen replay gates * docs(rcf): expose native formula API and exact remaining replay boundary * docs(rcf): retain source-bound native formula proof and rendering records * Keep paired RCF diagnostics outside CI and tighten native API evidence * Bind post-review native proof and manual checks to committed sources * Clarify the single fixed coefficient and wrap native API documentation * Link historical RCF records to reviewed and clarified source bindings * test(rcf): realize successive native samples jointly * docs(rcf): retain successive sample conformance evidence * docs(rcf): connect successive sample validation records * test(rcf): require native computed rows in witness proofs * docs(rcf): bind computed-row marker validation * docs(rcf): record final marker build job counts * docs(rcf): retain final upstream integration validation * feat(rcf): realize native specialization and degrees jointly * docs(rcf): retain native specialization proof evidence * fix(rcf): retain source sizes and test infinitesimal leading signs * docs(rcf): bind revised source-size and false-row validation * test(rcf): consume source sizes and realized coefficient laws * docs(rcf): retain original-coordinate consumer verification * docs(rcf): state fresh-import verification limits precisely --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
) * Reuse direct canonical constants in nested rational-function fields * Keep numeral construction inside the measured call * Include four depths in the short nested-sign validation * Retain constant-construction and consumer comparisons * Restore rational-function performance acceptance with retained evidence * Distinguish retained degree evidence from current benchmark coverage * Label the constructor and descriptive operation-count derivations * Bind full cast inspection and evidence validation to the measured computation * Retain the complete runtime-cast comparison and source snapshots * Validate historical sources without freezing future arithmetic edits --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* test: enforce Sturm API lints and assess compiled declaration references * test: bind Sturm lint and declaration-use evidence to source * test: refresh Sturm references after direct oracle integration * test: distinguish Sturm production use and consistent replay forgeries * test: retain classified Sturm references and generated origins * test: trace Sturm downstream references and bind the complete audit input cone * test: preserve genuine methods when filtering generated Sturm users * test: verify complete Sturm API dispositions and canonical source bindings * docs: assess every Sturm API without downstream production references * test: cover Sturm production imports and preserve clients through generated equations * docs: retain complete Sturm production coverage and verified reference derivations * fix: bind Sturm coverage sources and state alias-audit limits precisely * docs: assess Sturm private constructor and delimit retained evidence --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
…sion (#10874) * feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory * Reuse supplied common-field irreducibility proofs Refs #10358 * Clarify supplied irreducibility checking and native search Refs #10358 * Record supplied common-field proof validation Refs #10358 * Bind supplied irreducibility checks to integrated main Refs #10358 * Scope supplied proofs and clarify certification diagnostics Refs #10358 * Record scoped proof regressions and inspectable evidence Refs #10358 * Document and identify supplied irreducibility failures Refs #10358 * Bind final irreducibility diagnostics and validation records * Clarify common-field proof priority and tighten refusal control * Record final scoped-instance review and tightened control * Add matched probes for supplied RCF irreducibility construction cost * Emit complete inventories for the external proof collector * Record supplied-proof comparison and document native joint realization * Bind diagnostic documentation and inspected examples to their source * test(rcf): keep supplied-instance budget exhaustion terminal * docs(rcf): retain supplied-instance budget control evidence * feat(rcf): realize native shared-formula rows at one real point * docs(rcf): state native joint formula semantics and frozen replay gates * docs(rcf): expose native formula API and exact remaining replay boundary * docs(rcf): retain source-bound native formula proof and rendering records * Keep paired RCF diagnostics outside CI and tighten native API evidence * Bind post-review native proof and manual checks to committed sources * Clarify the single fixed coefficient and wrap native API documentation * Link historical RCF records to reviewed and clarified source bindings * test(rcf): realize successive native samples jointly * docs(rcf): retain successive sample conformance evidence * docs(rcf): connect successive sample validation records * test(rcf): require native computed rows in witness proofs * docs(rcf): bind computed-row marker validation * docs(rcf): record final marker build job counts * docs(rcf): retain final upstream integration validation * feat(rcf): realize native specialization and degrees jointly * docs(rcf): retain native specialization proof evidence * fix(rcf): retain source sizes and test infinitesimal leading signs * docs(rcf): bind revised source-size and false-row validation * test(rcf): consume source sizes and realized coefficient laws * docs(rcf): retain original-coordinate consumer verification * docs(rcf): state fresh-import verification limits precisely * feat(rcf): preserve native sample coefficient conversion * style(rcf): normalize sample manual ending * docs(rcf): retain native sample conversion validation records * test(rcf): check sample point consumers and selected conjugate rows * docs(rcf): retain point and conjugate consumer verification * test(rcf): realize a guarded sample over an infinitesimal parent * test(rcf): check selected sample conversion over an infinitesimal parent * test(rcf): retain the selected sample equation at its real reader * test(rcf): retain selected model sample validation records --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* feat(HexRCF): retain selected fields in complete root production * feat(HexRCF): retain authenticated source field certificates * fix(HexRCF): transport source certificates through literal equality * test(HexRCF): audit quoted proof sharing and retain kernel diagnostics * docs(HexRCF): retain fixed-field proof syntax accounting * docs(HexRCF): specify cached syntax audit scope * test(HexRCF): add independent fixed-field proof cost probes * test(HexRCF): retain independent proof costs and shared syntax audit * test(HexRCF): expose optional proof phase profiling * docs(HexRCF): retain independent scaling and kernel attribution evidence * feat(HexRCF): lower rational algebraic sources with original guards * test(HexRCF): keep scientific attribution outside routine CI * fix(HexRCF): authenticate mixed rational divisors and radical aliases * feat(HexRCF): check source conversions and quote reduced field coordinates Preserve original guards across checked construction and explicit projection; compose exact lowering proofs for source, guards and radicands. Quote canonical field coordinates with kernel-checked degree bounds and provide matched quotation controls/probes. Refs #10358, #10634. * fix(HexRCF): guard discarded conversions and retain quotation comparison Reject escaping and unsupported raw divisors in checked-conversion branches; cover actual nonzero QAdjoin division and both quotation modes. Share cast normalization and remove unused rewrite wrappers. Retain all 24 paired quotation samples; keep the production default unchanged because direct degree proofs did not establish a speedup. Refs #10358, #10633, #10634. * Fix multi-prime certificate replay under ordinary public imports (#10621) * fix: replay multi-prime certificates under public imports * fix: register replay regressions and narrow certificate evaluation * fix: preserve quoted statements and record visibility exemptions * perf: use guarded kernel reduction for closed certificate replay * fix: identify certificate quotation failures at the API boundary --------- Co-authored-by: Kim Morrison <kim@lean-fro.org> * test(HexRCF): consume public multi-prime quotation through optional import Adopt merged #10621 without privileged imports. Generate and quote the quartic certificate through the unchanged public API, check its ordinary-kernel replay and exercise selected-root source authentication in rcf. Refs #10358, #10620. * perf(HexRCF): prove coordinate degree from literal array length Use the existing polynomial size bound to avoid rational evaluation in each literal degree proof. Keep reduced-coordinate quotation opt-in pending its matched comparison. Refs #10358, #10634. * bench(HexRCF): retain array-bound quotation comparison * fix(HexRCF): consume merged public replay and stabilize rejection checks * feat(HexRCF): replay exact interval field signs with Sturm fallback * perf(HexRCF): select certified interval quotation with retained evidence * feat(HexRCF): quote public multi-prime common-field certificates * test(HexRCF): cover common multi-prime replay and audit provenance * test(HexRCF): prove named-constant goals from caller bounds * Fix retained algebraic guards and bind proof-route regressions * Retain common-field root comparisons with proved interval signs * Verify both interval quotation modes and retain audit capture provenance * Compare combined kernel replay with separately checked conjuncts * Retain paired kernel replay measurements and document limits * Compare checked monic carrier proposals with raw cores * Retain monic carrier comparisons and document progress boundary * Prove normalized carrier progress and enable checked monic cores * Connect normalized carrier laws and clarify replay controls * Prove normalized leading value at the selected field embedding * Verify tactic carrier option wiring and preserve measurement provenance * Index fixed-field sign evidence and preserve replay equivalence * Preserve all recorded signs when index routing misses * Enable indexed replay with preserved hits and retained proof comparisons * test: audit quoted sign indices and preserve linear replay controls * feat: expose authenticated coefficient preparation and finite replay * docs: distinguish delivered base transport from joint sample realization * fix: restore state when direct divisor preflight fails * docs: identify the existing positive chain normalization * fix: harden prepared proof acceptance and original guards * fix: bind prepared diagnostics and discard check-only proofs * docs: record merged finite-reader coverage laws * perf: assemble fresh tactic inputs privately and batch public binding * docs: retain matched fresh-validation proof costs * fix: assert common-field validation routes and screen source evidence * docs: retain routed common-field validation comparison * fix: screen native input data and assert matched validation arms * docs: retain matched validation-arm comparison and limits * fix: keep frozen sign quotation independent of producer controls * test: pin frozen replay evidence and terminal producer controls * Specialize native coefficient representations and verify ordinary real samples * Exercise native zero and duplicate atoms and preserve remaining realization gates * Record the merged coefficient dependency envelope and its remaining reader obligations * Connect source signs at selected sections and check noncanonical cancellation * Interpret shared formulas over native real samples * Check comparison tags on native constant and root cells * Keep factor measurement coverage on the exact adapter Lake blob * State the precise imported-module and link-argument scope * Compose registered bounds with checked algebraic enclosures * Bind the mixed-bounds exemption to the merged main Lake blob * Keep mixed-coefficient manual examples readable at narrow widths * Preserve rational bounds, share enclosures and pin replay controls * Kernel-check public enclosures and strengthen mixed coefficient controls * Pin enclosure target and discriminate public kernel acceptance * Authenticate positive rational-root aliases and closed root division * Bind proof-only Lake exemption to current upstream integration * Preserve unsupported sibling decline control with nested radical * Preserve original coefficient owners through native gathering * Strengthen root alias refusal and perfect-power coverage * Defer recognition exhaustion until sibling classification completes * Preserve structured root recognition errors and bound rational numerators * Bind runtime-neutral Lake audit to integrated source * Bound finite root enclosures before normalization and expose gathered valuations * Bind Lake runtime audit to merged native-realization interfaces * Bound inverse-root admission and combined generator degrees * Stop common-degree admission early and identify its diagnostic * Recognize real roots through type-argument metadata * Share typed real-power admission across coefficient handlers * Short circuit root detection and strengthen typed enclosure controls * Bound reciprocal-degree numerators before rational normalization * Check intermediate arithmetic hidden by zero powers * Admit rational guards and retain zero-power bases once * Share nested rational guard admission and restore its local state * Pin enclosing guard bounds and failed-admission isolation * Limit guard sharing to bounded arithmetic operands * Authenticate roots of closed algebraic bases with frozen evidence Refs #10358. Reuse authenticated fixed-field base coordinates for native proposals; check selected embedding, power and sign evidence in ordinary kernel proofs. Admit degree before root construction, retain original guards and typed failures, and extend existing rcf/manual/conformance coverage. * Link retained proof evidence to its archived source Refs #10358. Preserve upstream proof-probe pruning while keeping the active evidence inventory link valid. * Share algebraic-base authentication and preserve typed declines * Reuse recursive base proofs and certify only the selected common field * Compose finite bounds with authenticated algebraic-base roots * Unify mixed-root proof audits and clarify registration scope * Allow ordered-subsequence coefficient gathering in rcf * Check actual gathering refusal and provider-derived production * Distinguish kernel gathering laws from executable controls * Cover mixed bounds with roots of non-rational algebraic bases * Exercise explicit real-power guard preflight * Compose finite infinitesimal replay with shared source formulas * Fit the realization API example to narrow manual layouts * Audit frozen replay data and separate Boolean refusal * Restrict the complete frozen-data construction closure * Allow only explicit foreign primitives in frozen replay data * Produce shared sentences in original selected number fields * Cover original field embeddings and clarify native API use * Distinguish the middle cubic embedding from both outer roots * Connect original-field production to frontend coefficient semantics * Exercise cubic coordinates and reuse original-field presentations * Cover variable disequality and retain substantive proof audits * Replay an ordinary selected-root source row * Guard generated selected-field replay acceptances * Check selected-field rows from certificate bytes * Guard byte proof bodies and forged packet controls * Check original packing records in selected-root replay * Check swapped packing evidence and literal zero provenance * Pin packing inventory order and swapped-packet premises * Check supplied selected-root catalog literals and bytes * Check catalog semantic refusals and source transport bodies * Pin catalog refusal diagnostics and returned root bytes * Select validated catalog bases for RCF coefficient gathering * Validate registered catalog gathering and refusal Require real models only for jointly admissible installed prefixes. Exercise a non-prefix registered owner and stale-version refusal, and pin six exact complete axiom inventories. Clarify the automatic manual example and record the revised build/render source bindings. The compiled packet costs and common-field kernel experiment remain bound to historical d84cecf. Integrated main changes owner dependencies and Mathlib/Tau Ceti pins without changing the measured source files; these observations do not time the new integration or establish strict replay. * Bind catalog integration checks to the merged Lake configuration * Exercise actual provider selection and preserve manual size limits Reuse the owner single-constant fixture for native version refusal, incompatible-entry skipping and rational priority. Audit all provider support proofs. State the registered instance provider-induced interpretation precisely and keep original-model factory laws distinct. Preserve every displayed Lean block modulo whitespace within the3000-line chapter cap. Link retained packet costs to the exact historical source, verify desktop/narrow layout, and bind all revised diagnostics and source hashes. * Clarify selected model premises and split caller bounds manual * Preserve the original model in single-prefix registered gathering * Check a registered further root with shared Ioc guards * Bind registered-source validation to the merged main baseline * Use shared domain lowering and check excluding domains and endpoints * Clarify sentence guard scope and execute rational endpoint controls * Preserve ordered registered coefficient values through native gathering Refs #10358. * Bind registered coefficient evidence to the landed main integration * Clarify native signature coverage and retain static-check evidence * Consume reconciled catalog gathering with ordered RCF source semantics * Retain selected provider history in reconciled RCF production * Bind reconciled history validation to the final integrated tree * Describe prefix selection without solver fallback terminology * Check supplied inverse source equations and original guards * Bind inverse validation to integrated main and preserve prior evidence * Guard inverse replay reductions and remove conformance manual dependency * Correct public query availability in RCF evidence inventory * Reuse supplied common-field irreducibility proofs Refs #10358 * Clarify supplied irreducibility checking and native search Refs #10358 * Record supplied common-field proof validation Refs #10358 * Bind supplied irreducibility checks to integrated main Refs #10358 * Scope supplied proofs and clarify certification diagnostics Refs #10358 * Record scoped proof regressions and inspectable evidence Refs #10358 * Document and identify supplied irreducibility failures Refs #10358 * Bind final irreducibility diagnostics and validation records * Clarify common-field proof priority and tighten refusal control * Record final scoped-instance review and tightened control * Add matched probes for supplied RCF irreducibility construction cost * Emit complete inventories for the external proof collector * Record supplied-proof comparison and document native joint realization * Bind diagnostic documentation and inspected examples to their source * test(rcf): keep supplied-instance budget exhaustion terminal * docs(rcf): retain supplied-instance budget control evidence * feat(rcf): realize native shared-formula rows at one real point * docs(rcf): state native joint formula semantics and frozen replay gates * docs(rcf): expose native formula API and exact remaining replay boundary * docs(rcf): retain source-bound native formula proof and rendering records * Keep paired RCF diagnostics outside CI and tighten native API evidence * Bind post-review native proof and manual checks to committed sources * Clarify the single fixed coefficient and wrap native API documentation * Link historical RCF records to reviewed and clarified source bindings * test(rcf): realize successive native samples jointly * docs(rcf): retain successive sample conformance evidence * docs(rcf): connect successive sample validation records * test(rcf): require native computed rows in witness proofs * docs(rcf): bind computed-row marker validation * docs(rcf): record final marker build job counts * docs(rcf): retain final upstream integration validation * feat(rcf): realize native specialization and degrees jointly * docs(rcf): retain native specialization proof evidence * fix(rcf): retain source sizes and test infinitesimal leading signs * docs(rcf): bind revised source-size and false-row validation * test(rcf): consume source sizes and realized coefficient laws * docs(rcf): retain original-coordinate consumer verification * docs(rcf): state fresh-import verification limits precisely * feat(rcf): preserve native sample coefficient conversion * style(rcf): normalize sample manual ending * docs(rcf): retain native sample conversion validation records * test(rcf): check sample point consumers and selected conjugate rows * docs(rcf): retain point and conjugate consumer verification * test(rcf): realize a guarded sample over an infinitesimal parent * test(rcf): check selected sample conversion over an infinitesimal parent * test(rcf): retain the selected sample equation at its real reader * test(rcf): retain selected model sample validation records * feat(rcf): authenticate selected coefficients at one real reader * docs(rcf): record selected source proof validation boundaries * test(rcf): retain selected source checks and rendered manual * Exercise selected and inherited coordinates jointly and clarify supplied guards * Retain current source-identity validation and manual evidence --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Bind adapter overview corrections to checked implementation * Clarify cell soundness attribution and retained observations * Bind clarified cell documentation to unchanged checked source * Repair architecture report links after theory rename * Reuse checked algebraic cell rows across comparison formulas * Record checked Boolean cell reuse and manual evidence * Document exact formula reuse boundary in adapter overview * Bind formula reuse overview to checked implementation * Preserve historical replay identities across the Theory rename * Construct checked carriers, full root tables and supplied ordinary cell rows * Keep the root construction example readable on narrow screens * Record native cell construction proofs and validation evidence * Document actual carrier and complete-cell construction boundaries * Bind construction overview to checked source and retained evidence * Discover ordinary cell points through the actual common-context partition * Strengthen retained certificate mutation and unrelated-path controls * Record source-bound ordinary discovery validation and remaining acceptance gates * Construct accepted ordinary-model cell evidence through proved sector requests * Qualify the tower signature in the ordinary point-row manual example * Fit the ordinary point-row example on narrow manual pages * Bind ordinary cell-decision proofs, native diagnostics and manual validation to exact sources * Bind cell-decision documentation to the checked implementation and full-build sources * Retain child-level row-production diagnostics and exact source bindings * Bind the expanded row-cost report and retain its prior documentation version * Use proved endpoint requests in public cell discovery * Register explicit cell stress target with DAG checks * Fix public discovery driver and update audit documentation * Use a regular comment for the explicit stress evaluation * Record final public endpoint validation and retained attempts * Clarify scratch timing and separate stress target documentation * Bind endpoint documentation to its exact revision * Prove executable complete-cell construction and original verdicts * Retain producer traces and reuse prepared cell queries * Check quotation module ownership and demonstrate an accepted verdict * Fit executable-cell proof example on narrow screens * Record source-bound executable-cell validation and manual inspection * Bind executable-cell documentation to its validated source versions * Construct complete cells from original selected number-field inputs * Wrap fixed-field producer example for narrow screens * Record selected-field cell validation and retained source-scoped evidence * Bind selected-field documentation and validation to exact versions * Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Pin final transport exhaustion and assigned fact accounting * Retain exact transport-budget regressions and final proof evidence --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Fit the ordinary point-row example on narrow manual pages * Bind ordinary cell-decision proofs, native diagnostics and manual validation to exact sources * Bind cell-decision documentation to the checked implementation and full-build sources * Retain child-level row-production diagnostics and exact source bindings * Bind the expanded row-cost report and retain its prior documentation version * Use proved endpoint requests in public cell discovery * Register explicit cell stress target with DAG checks * Fix public discovery driver and update audit documentation * Use a regular comment for the explicit stress evaluation * Record final public endpoint validation and retained attempts * Clarify scratch timing and separate stress target documentation * Bind endpoint documentation to its exact revision * Prove executable complete-cell construction and original verdicts * Retain producer traces and reuse prepared cell queries * Check quotation module ownership and demonstrate an accepted verdict * Fit executable-cell proof example on narrow screens * Record source-bound executable-cell validation and manual inspection * Bind executable-cell documentation to its validated source versions * Construct complete cells from original selected number-field inputs * Wrap fixed-field producer example for narrow screens * Record selected-field cell validation and retained source-scoped evidence * Bind selected-field documentation and validation to exact versions * Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Quote polynomial readers by refinement within shared reflection budgets * Fit shared quotation manual examples on narrow screens * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Retain shared-request quotation proof and manual evidence * Pin final transport exhaustion and assigned fact accounting * Record shared quotation input guards and bounded validation * Retain exact transport-budget regressions and final proof evidence * Retain shared-request transport and final manual evidence * Check nested predecessor transport without native codec reduction * Retain nested quotation and module validation evidence * Quote normalized coefficient vectors through public owner laws * Retain public polynomial quotation validation and failed probes * Preserve original instances and export quoted polynomial data * Retain exact-instance and cross-module quotation evidence * Protect accepted constant-form canonical codec callbacks * Retain constant callback regression and exact source validation * Protect annotated decode callbacks and reject malformed steps * Retain annotated callback and complete-shape validation --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Bind selected-field documentation and validation to exact versions * Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Quote polynomial readers by refinement within shared reflection budgets * Fit shared quotation manual examples on narrow screens * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Retain shared-request quotation proof and manual evidence * Pin final transport exhaustion and assigned fact accounting * Record shared quotation input guards and bounded validation * Retain exact transport-budget regressions and final proof evidence * Retain shared-request transport and final manual evidence * Allow structured error types in checked reader quotation * Retain algebraic root-table quotation and real witness evidence * Check algebraic root-table quotation and bounded real witnesses in CI * Compile emitted polynomial and root-table data for runtime consumers * Check nested predecessor transport without native codec reduction * Retain nested quotation and module validation evidence * Quote normalized coefficient vectors through public owner laws * Retain public polynomial quotation validation and failed probes * Check expanded root-table quotation proof inventory * Preserve original instances and export quoted polynomial data * Retain exact-instance and cross-module quotation evidence * Record final root-table input quotation budget * Retain compiled root-table replay and final proof evidence * Check complete real solution set and terminal root-table rejection * Retain exact table equation and document its complete solution list * Wrap the table-specific solution example for narrow displays * Protect accepted constant-form canonical codec callbacks * Retain constant callback regression and exact source validation * Check strict real ordering in the complete root-table example * Retain complete ordered root-table and final manual evidence * Protect annotated decode callbacks and reject malformed steps * Retain annotated callback and complete-shape validation * Compose scalar quotation through selected predecessors * Wrap the recursive decoder manual example * Check nested scalar refusal and late rollback * Use the published cubic source link in the manual * Protect annotated scalar decodes and check charged retries * Fit the scalar lookup signature on narrow screens * Record recursive scalar quotation checks and rendered examples --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Register explicit cell stress target with DAG checks * Fix public discovery driver and update audit documentation * Use a regular comment for the explicit stress evaluation * Record final public endpoint validation and retained attempts * Clarify scratch timing and separate stress target documentation * Bind endpoint documentation to its exact revision * Prove executable complete-cell construction and original verdicts * Retain producer traces and reuse prepared cell queries * Check quotation module ownership and demonstrate an accepted verdict * Fit executable-cell proof example on narrow screens * Record source-bound executable-cell validation and manual inspection * Bind executable-cell documentation to its validated source versions * Construct complete cells from original selected number-field inputs * Wrap fixed-field producer example for narrow screens * Record selected-field cell validation and retained source-scoped evidence * Bind selected-field documentation and validation to exact versions * Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Quote polynomial readers by refinement within shared reflection budgets * Fit shared quotation manual examples on narrow screens * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Retain shared-request quotation proof and manual evidence * Pin final transport exhaustion and assigned fact accounting * Record shared quotation input guards and bounded validation * Retain exact transport-budget regressions and final proof evidence * Retain shared-request transport and final manual evidence * Check nested predecessor transport without native codec reduction * Retain nested quotation and module validation evidence * Quote normalized coefficient vectors through public owner laws * Retain public polynomial quotation validation and failed probes * Preserve original instances and export quoted polynomial data * Retain exact-instance and cross-module quotation evidence * Compose scalar quotation through selected predecessors * Check nested scalar refusal and late rollback * Use the published cubic source link in the manual * Protect annotated scalar decodes and check charged retries * Fit the scalar lookup signature on narrow screens * Quote original sign packets through checked prepared contexts Refs #10358. Restore the exact optional-reader result, compose packet-backed coefficient decoding with its real interpretation, and check transactional rejection and final budget exhaustion. The public frozen-signature decoder equation remains an explicit owner gate. * Check sign-packet provenance and complete caller restoration Refs #10358. Require the decoded-value proof to depend on the new packet fact and canonical reader law; check complete caller metavariable restoration after success and exact-budget replay. Document the public-codec gate. * Wrap sign-packet manual examples for narrow displays Refs #10358. Retain the failed10px/6px layout captures and clarify the fixture depth. The checked expressions are unchanged. * Record checked sign-packet quotation and public replay gate Refs #10358. Retain87 verified source-bound artifacts, fresh proof audits and reviews, final desktop/narrow captures, failed layouts and public-module probes, live memory policy, and exact prerequisite merge verification. Distinguish validation observations from scaling and speedup evidence. * Keep the renderer snapshot as immutable text evidence Refs #10358. Preserve exact renderer bytes under .lean.txt, record the actual CI copyright-lint failure, and retain all six successful metadata checks after git tracking. No Lean source or workflow changes. * Derive evidence checks from captured tracked-file results Refs #10358. Assert and derive metadata from all six real exit statuses, retain the completed fresh Opus review, label the byte-identical probe alias, and exclude live CI observers from completed artifacts. --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Construct complete cells from original selected number-field inputs * Wrap fixed-field producer example for narrow screens * Record selected-field cell validation and retained source-scoped evidence * Bind selected-field documentation and validation to exact versions * Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Quote polynomial readers by refinement within shared reflection budgets * Fit shared quotation manual examples on narrow screens * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Retain shared-request quotation proof and manual evidence * Pin final transport exhaustion and assigned fact accounting * Record shared quotation input guards and bounded validation * Retain exact transport-budget regressions and final proof evidence * Retain shared-request transport and final manual evidence * Check nested predecessor transport without native codec reduction * Retain nested quotation and module validation evidence * Quote normalized coefficient vectors through public owner laws * Retain public polynomial quotation validation and failed probes * Preserve original instances and export quoted polynomial data * Retain exact-instance and cross-module quotation evidence * Compose scalar quotation through selected predecessors * Check nested scalar refusal and late rollback * Use the published cubic source link in the manual * Protect annotated scalar decodes and check charged retries * Fit the scalar lookup signature on narrow screens * Quote original sign packets through checked prepared contexts Refs #10358. Restore the exact optional-reader result, compose packet-backed coefficient decoding with its real interpretation, and check transactional rejection and final budget exhaustion. The public frozen-signature decoder equation remains an explicit owner gate. * Check sign-packet provenance and complete caller restoration Refs #10358. Require the decoded-value proof to depend on the new packet fact and canonical reader law; check complete caller metavariable restoration after success and exact-budget replay. Document the public-codec gate. * Wrap sign-packet manual examples for narrow displays Refs #10358. Retain the failed10px/6px layout captures and clarify the fixture depth. The checked expressions are unchanged. * Record checked sign-packet quotation and public replay gate Refs #10358. Retain87 verified source-bound artifacts, fresh proof audits and reviews, final desktop/narrow captures, failed layouts and public-module probes, live memory policy, and exact prerequisite merge verification. Distinguish validation observations from scaling and speedup evidence. * Keep the renderer snapshot as immutable text evidence Refs #10358. Preserve exact renderer bytes under .lean.txt, record the actual CI copyright-lint failure, and retain all six successful metadata checks after git tracking. No Lean source or workflow changes. * Derive evidence checks from captured tracked-file results Refs #10358. Assert and derive metadata from all six real exit statuses, retain the completed fresh Opus review, label the byte-identical probe alias, and exclude live CI observers from completed artifacts. * Generate checked coefficient tuple selectors * Assemble and authenticate selected fixed-field coordinates * Exercise public field assembly and independent source controls * Preserve the inherited coordinate proof boundary * Use published source links in the rendered RCF manual * Wrap the public fixed-field manual example for narrow pages * Record source-bound fixed-field authentication evidence * Retain exact sample and reader ties in selected-source proofs * Bind revised source proof evidence to actual sample and reader tests * Regenerate negative-root fixtures and check the direct point row * Verify complete source, audit and literal evidence bindings * Retain and check negative fixture provenance --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Record combined cell integration against current main * Bind combined integration documentation to its exact version * Tighten producer import audits and remove unused hashing assumptions * Record complete affected-target validation and final manual inspection * Bind final validation documents and source-scoped artifact versions * Name the exact adapter modules excluded by quotation audits * Bind the precise quotation-boundary documentation revision * Compose finite cell-row replay around descriptor restoration * Record finite cell serialization validation and remaining descriptor gate * Bind serialization report and collector to their committed artifacts * Check large cell-fold proofs directly in the guarded kernel * Check large cell-fold proofs directly in the guarded kernel * Record matched cell-fold assembly observations and current manual validation * Bind the fold-assembly report and collector to their source versions * Validate finite cell parser composition against current main * Bind current-main parser validation documents * Collect complete cell payload literals for finite reader coverage * Record finite payload inventory proofs and refusal controls * Bind the finite inventory report and collector versions * Restore complete cell payloads through checked owner graph bindings * Record complete payload restoration through the owner binding API * Bind the complete payload restoration report versions * Replay complete frozen root tables and cell matrices from finite literals * Prove accepted complete root-and-cell output for native discovery * Record complete root-and-cell replay and producer acceptance * Bind complete replay evidence documents to their committed versions * Quote complete root-and-cell packets at the original guarded source * Record complete packet quotation checks and retained source evidence * Bind complete quotation report and collector versions * Document complete packet soundness and guarded source quotation * Replay complete packets from the original selected number field * Wrap complete packet examples for narrow manual layouts * Emit checked root graphs and strengthen complete replay refusal controls * Bind selected-field acceptance and manual examples to emitted packets * Record emitted-packet integration and inspected manual evidence * Bind integrated packet evidence documents and inspected artifacts * Check every packet-quotation refusal restores state * Record final refusal attribution and state-restoration checks * Bind final refusal evidence report and collector versions * Produce complete packets from independently owned coefficient values * Identify gathered selected-field coordinates through the canonical reader * Prove complete gathered replay at original selected-field values * Retain gathered packet proof, build and manual evidence * Bind gathering evidence to exact source and retained artifacts * Construct native cell packets from original algebraic coefficient tuples * Audit original algebraic guards and retain the stronger stress case * Register the explicit algebraic cell stress build target * Link original-input cell validation without replacing existing evidence * Preserve the fixed-matrix evidence link * Retain original-input proofs, manual validation and interrupted stress evidence * Bind original-input validation to exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Derive accepted guard validity and distinguish conjugate quantifiers * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Reuse owner descriptor restoration and graph binding laws * Retain direct owner descriptor reuse validation * Bind owner descriptor reuse to its exact source and artifacts * Retain current-main integration and revised acceptance evidence * Bind revised acceptance proofs and current-main validation * Record metadata exit statuses and unchanged implementation sources * Bind explicit metadata checks and source identity validation * Prepare native algebraic packet inputs from checked source expressions * Scope preparation proof auxiliaries and test domains and false verdicts * Keep native preparation guard check within narrow manual layout * Retain native source preparation validation and interrupted stage diagnostics * Bind native source preparation report and all retained artifacts * Check cancellation around native algebraic preparation and packet production * Retain cancellation integration and fresh public codec exposure probes * Bind current cancellation and API boundary validation artifacts * Retain current-main algebraic preparation integration evidence * Bind landed-owner integration logs to exact documents and sources * Strengthen source preparation rollback and completed regressions * Retain corrected source preparation validation and compiler ordering * Bind corrected validation to exact source and artifact commits * Exercise post-mutation exceptions and mixed native input roles * Retain final source preparation conformance and review evidence * Bind final conformance to its exact evidence commit * Replay complete cell packets through checked supplied operations * Construct checked real models of retained algebraic towers * Quote checked supplied-operation predicates at original goals * Check original goals from actual reached-record assembly * Fit supplied-operation example on narrow manual pages * Retain supplied-operation assembly proofs and validation evidence * Bind assembly evidence to committed documents and artifacts * Abstract maximal closed coefficients and preserve polynomial bounds * Assert exact replay refusals and actual record dependencies * Record exact refusal and reached-record audit validation * Bind expanded replay controls to committed evidence * Retain scalar codec provenance and wrong-program refusal coverage * Retain scalar provenance, wrong-program checks and isolated memory evidence * Bind final scalar-provenance control validation * Prove maximal closed coefficient goals in fresh kernel modules * Check evidence log versions and identify sampled resource values * Bind checked evidence provenance to committed documents * Document maximal closed coefficients with checked tactic examples * Describe maximal coefficient recognition and proof boundaries * Fit maximal coefficient examples on narrow manual screens * Use square-root notation to fit the checked manual examples * Retain source-scoped maximal coefficient validation and manual captures * Bind maximal coefficient report and artifacts to their retained commit * Include closed coefficient examples as a focused manual subsection * Place the included subsection after the parent section blocks * Retain included-subsection validation with final metadata and inspected captures * Bind the final manual validation report to its artifact commit * Retain formula and negative-embedding refusal under maximal abstraction * Preserve existing conformance target order when adding maximal checks * Record integrated kernel proofs and the compiled missing-record diagnostic * Bind integration and compiled diagnostic artifacts to their report commit * Validate maximal coefficients against the landed parent and public graph reader * Bind final merged-main evidence to its committed artifacts * Preserve equality witnesses and strengthen maximal coefficient controls * Handle metadata and aliases in checked equality-witness selection * Require provider evidence in the aliased witness proof * Retain checked equality-witness and maximal-source validation evidence * Bind final witness evidence to the committed report and captures * Authenticate selected source coefficients from checked scalar replay * Check registered zero guards and import the source selection manual API * Check maximal registered zero products and terminal divisor refusals * test(HexRCF): bind guarded fixtures to whole source coefficients * docs(HexRCF): retain selected-source proof and full compatibility evidence * docs(HexRCF): bind retained source evidence to committed artifacts * fix(HexRCF): preserve maximal metadata and order source guards consistently * docs(HexRCF): bind source audits, base tests and routing observations * docs(HexRCF): identify committed review-validation artifacts * feat(HexRCF): characterize algebraic producer acceptance * fix(HexRCF): retain finite leaf witnesses and canonical metadata * fix(HexRCF): preserve quotient witnesses without duplicate bounds * fix(HexRCF): check finite witness evidence consistently * docs(HexRCF): retain final finite compatibility and manual evidence * feat(HexRCF): prove acceptance at checked original algebraic sources * fix(HexRCF): preserve proof budgets and exact source acceptance bindings * fix(HexRCF): account retained identities within preparation budgets * fix(HexRCF): give manual proof checks private auxiliary names * docs(HexRCF): fit source acceptance example to narrow pages * docs(HexRCF): shorten narrow example failure text * docs(HexRCF): retain complete source acceptance validation * docs(HexRCF): retain landed-parent integration evidence * fix(HexRCF): validate original source guard inventories * test(HexRCF): bound repeated original-source scans * docs(HexRCF): retain guard and budget validation * Quote supplied root replay with ordinary kernel equations * Keep the root quotation example readable on narrow screens * Authenticate frozen cubic scalar payloads through merged public codecs * Retain source-bound root quotation validation and rendered evidence * Strengthen quotation validation and interpret the frozen cubic over the reals * Handle function-valued Boolean recursors through checked prefix transport * Record final quotation controls, real-witness audit and bounded validation * Keep rational algebraic inputs in their checked parent context * Record checked rational-point preparation and bounded diagnostic evidence * Retain the stronger stress timeout after rational-point preparation * Quote canonical rational payloads through checked public codec equations * Record generic rational quotation proofs and checked manual rendering * Audit imported caller-registered pi and exp proof bodies * Bound rational codec recognition and strengthen independent quotation controls * Record bounded codec decline and final independent quotation audit * Retain fresh ordinary-kernel evidence for caller-registered constants * Retain named-constant audit dependency and admission checks * Clarify rational decoder eligibility and pin original coefficient values * Retain final rational quotation eligibility and manual evidence * Quote selected-field scalars using checked sign facts and exact codec arguments * Retain exact scalar quotation, producer-free proof audit and manual evidence * Quote polynomial readers by refinement within shared reflection budgets * Fit shared quotation manual examples on narrow screens * Audit named proof auxiliaries and scalar data; validate quotation inputs * Retain full scalar data and named auxiliary-body proof evidence * Meter instantiated inputs and enforce exact scalar reader targets * Record instantiated-input audits and enforced resource controls * Retain shared-request quotation proof and manual evidence * Pin final transport exhaustion and assigned fact accounting * Record shared quotation input guards and bounded validation * Retain exact transport-budget regressions and final proof evidence * Retain shared-request transport and final manual evidence * Check nested predecessor transport without native codec reduction * Retain nested quotation and module validation evidence * Quote normalized coefficient vectors through public owner laws * Retain public polynomial quotation validation and failed probes * Preserve original instances and export quoted polynomial data * Retain exact-instance and cross-module quotation evidence * Compose scalar quotation through selected predecessors * Check nested scalar refusal and late rollback * Use the published cubic source link in the manual * Protect annotated scalar decodes and check charged retries * Fit the scalar lookup signature on narrow screens * Quote original sign packets through checked prepared contexts Refs #10358. Restore the exact optional-reader result, compose packet-backed coefficient decoding with its real interpretation, and check transactional rejection and final budget exhaustion. The public frozen-signature decoder equation remains an explicit owner gate. * Check sign-packet provenance and complete caller restoration Refs #10358. Require the decoded-value proof to depend on the new packet fact and canonical reader law; check complete caller metavariable restoration after success and exact-budget replay. Document the public-codec gate. * Wrap sign-packet manual examples for narrow displays Refs #10358. Retain the failed10px/6px layout captures and clarify the fixture depth. The checked expressions are unchanged. * Record checked sign-packet quotation and public replay gate Refs #10358. Retain87 verified source-bound artifacts, fresh proof audits and reviews, final desktop/narrow captures, failed layouts and public-module probes, live memory policy, and exact prerequisite merge verification. Distinguish validation observations from scaling and speedup evidence. * Keep the renderer snapshot as immutable text evidence Refs #10358. Preserve exact renderer bytes under .lean.txt, record the actual CI copyright-lint failure, and retain all six successful metadata checks after git tracking. No Lean source or workflow changes. * Derive evidence checks from captured tracked-file results Refs #10358. Assert and derive metadata from all six real exit statuses, retain the completed fresh Opus review, label the byte-identical probe alias, and exclude live CI observers from completed artifacts. * Generate checked coefficient tuple selectors * Assemble and authenticate selected fixed-field coordinates * Exercise public field assembly and independent source controls * Preserve the inherited coordinate proof boundary * Use published source links in the rendered RCF manual * Wrap the public fixed-field manual example for narrow pages * Record source-bound fixed-field authentication evidence * Retain exact sample and reader ties in selected-source proofs * Bind revised source proof evidence to actual sample and reader tests * Regenerate negative-root fixtures and check the direct point row * Verify complete source, audit and literal evidence bindings * Retain and check negative fixture provenance * Quote public scalar packets through dependent matches * Retain public packet validation and proof-cost diagnostics * Keep dependent replay conversion abstract * Retain dependent quotation audits and conversion diagnostics --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Exercise original ex2 comparisons across the live cubic context * Regenerate and verify original ex2 live-context fixtures --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
* Checkpoint nested native reconstruction and bounded proof construction * Cover coefficient agreement orders and composed replay * Reuse checked dependency audits in nested reconstruction * Cover shared audit reads and declaration kinds * Independently audit native realization proof dependencies * Traverse proof and proposition together during dependency audits * Project bounded coefficient entries from retained blocks * fix(real-closure): retain coefficient request dictionaries * Adapt coefficient index controls to traversal reuse * Share finite reconstruction support through checked tuple data * Route finite ancestor operations before scanning descendant inventories * Retain an expensive actual nested guard for focused proof diagnostics * Measure the captured guard before module serialization * Check inline measurement helpers before preparing the nested guard * Expose the complete nested finite-replay fixture through normal modules * Export original joint tower proof with public root and product consumers * Pass explicit cache choice in coefficient agreement probe * Reject cached operand dependencies by owning module * Reject cached operand dependencies by owning module * Bind original joint fixture to full dependency audit evidence --------- Co-authored-by: Kim Morrison <kim@lean-fro.org>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The factorization and graph-iso freshness checks accept a .lean transition that only inserts `module`, makes each import public and opens `public section`: undoing exactly that must reproduce the baseline blob. The proof-probe isolation test reads module import forms. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…modules Each line is the import the compiler names in its `consider adding` hint. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…drivers name A public declaration's signature may not mention a private one under the module system. Each change removes `private` from a declaration that an `Unknown identifier` or instance-search error in the same file names. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Mark elaboration-time helpers `meta`, expose the local definitions the compiler and the ECPP fixture checks name, add meta imports for code that #guard evaluates natively, and drop `private` where Lean's note names the declaration a public signature needs. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…aluate Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… system Environment lint tests, kernel-replay audits and the quoteTerms benchmark need data a module sees only through `import all`; check_modules.py names them with the reason. HexECPPTheory.Tests no longer imports LintTests, which the library already builds as its own target. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Each definition is one a converted conformance or test proof unfolds by `decide`, `simp` or `rfl`, whose body only names public declarations. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s need `smoothPower_nil`/`smoothPower_cons` give the stage-1 loop's equations, and `nttPrimes_length`, `nttPrimes_map_maxLog` and `NttPrime.maxLength_eq` state the catalogue's shape. The primality bench and the NTT consumers now rewrite with these instead of unfolding private helpers. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…c facts Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…xt visibility layer Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nstances unfold Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…evaluate Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… sweep The regenerated commits redo the conversion on current main; this merge records the earlier branch head so the pull request updates without a force push. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
`deriving @[expose] DecidableEq` on the RCF syntax and SignDet JSON values lets importing modules decide their equality. Test fixtures that proofs reduce through are exposed; local types that public signatures name are public. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… for kernel checks Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… sweep freshness check The module-header conversion touches three files in the factorization relevant set: a module header and dropped `private` in the PARI driver, an `@[expose]` on `HexMatrix.writeRow`, and three new NTT catalogue theorems. None changes compiled code. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The signature equality checks decide with the structural instance instead of the pointer-shortcut one, whose core wrapper has no exposed body. The nested normalization bench gives `traceOp` its logical body and traces through an `@[implemented_by]` implementation, so `traceOp_eq` no longer unfolds `dbgTrace`. Signature, constant-key and RCF syntax equality are derived with exposed bodies. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…/module-headers Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This branch has not been deployed
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.
This PR converts every current Lean source outside
reports/to the module system and adds a source-only CI lint,scripts/check_modules.py, that fails on any tracked Lean file whose first token is notmodule. Tests, bench and conformance drivers, examples, experiments, the manual and the Lean emitted by generators (the selected-root literals, the Conway replay and the algebraicReprchecks) are all covered, so a library that never adopted the module system fails here instead of breaking the released aggregate.Most files take
public importandpublic section. Where compile-time evaluation, proofs or the compiler need more, files usemeta import,import allor@[expose]. Leaf bench drivers that no module imports dropprivatewhere their public declarations mention those names. The manual reachability check and the proof-probe import isolation check recognize module imports, and the graph-isomorphism figure freshness check accepts a header-only legacy-to-module conversion.This supersedes the module-header part of #10666 "Fix factorization process cleanup and require Lean modules in CI"; its PARI part landed in #10830.
🤖 Prepared with Claude Code