[kim-em]

Compile authenticated real coefficient sources and reconstruct complete root/cell packets, then prove the original real sentence in one cumulative reflection request. This removes the example-specific coefficient-family proof and composes source preparation, selected-root authentication, stored arithmetic, cell replay and source finishing.

The complete algebraic example proves ∃ x : ℝ, x² − √2 ≥ 0 ∧ x² − √2 ≤ 0 ∧ 0 = 0. Its coefficient identity comes from fresh descriptor/equation/window replay inside the same request. The final proof audit forbids the older imported selected-root/coefficient identities and earlier complete-packet proofs. The retained real model, source alias, coefficient-map laws and seed facts remain explicit inputs.

Implementation:

• TowerCompile.compile/prepareWith interpret rational literals, arithmetic, inversion and natural powers under the exact retained ordinary-real model. Both ordered source inventories are preserved, including original divisors hidden by zero multiplication. Source usage must continue into the enclosing request, and every transferred limit is checked. No raw-syntax field instance or new formula AST is introduced.
• CellQuote.valuationWith checks the finite coordinate/proof counts and assembles the entire source valuation from ordered scalar proofs in the ordinary kernel. The complete source example consumes this helper and the compiler within its existing transaction.
• SourceBuild.build/buildOn produce selected-source packets using existing owner enumeration or checked count-one open domains. Generic progress/acceptance laws consume actual coverage, unique selected windows and codec/DAG laws; successful producer outputs are not progress hypotheses.
• SourceIdentity.restorePacketWith retains the checked descriptor/header and prepared context for subsequent interpretation; quotePacketWith remains compatible. RowQuote, complete cell replay and source finishing retain exact ordered inputs, original guards, strict folds and original-target equivalence.
• Proof admission shares its visited set only within an individual check. Exact targets, unsafe/admitted dependency rejection, hidden-body inspection, fresh kernel checking and proof-only producer boundaries remain.

Validation:

• Prepared source valuations, implementation 8f7774eb33, evidence 5709cc18e9: 159 bound sources; final complete request 9,337,057 charged nodes; two graph-memo reuses/seven validations. Fresh full audit rechecks 1,192 theorem bodies/202 definitions/1,352 nonempty traces, with exactly propext, Classical.choice, Quot.sound. The unchanged original goal and every earlier dependency/producer guard are checked. Preliminary failures are retained separately from final success.
• Zero/one/two-coordinate requests use 7,590/11,174/16,484 nodes. Their fresh importing audit rechecks fourteen actual theorem bodies with thirteen nonempty traces and the standard three axioms. Swapped coordinates/proofs, missing entries, wrong counts and unresolved caller coordinates reject without retained declaration/metavariable changes. Arithmetic compiler controls additionally cover wrong sources/models, original guards, transferred limits, callback rollback and exhaustion; its independent audit checks 36 actual theorem bodies.
• Final seven-target integration passes 14,417 Lake jobs with cached dependencies reused: full source audit, valuation audit, compiler audit, base handlers, existing real-coefficient tactic checks, optional default umbrella and complete manual. Runtime 9min15.978s, peak7.6GiB/no swap. Full quotation separately takes 13min17.611s/2.3GiB; its fresh audit takes 3min22.868s/2.7GiB. This is affected-target evidence, not the entire default conformance suite or a scientific timing comparison.
• Complete current manual/render and all six actually viewed 1440px/390px API/code/provenance captures pass, with zero changed-block overflow. Render23.489s/1.7GiB, browser10.499s/2.8GiB, no swap. Ten repository checks, twelve DAG tests, source-bound verifier, 124 relative links and whitespace checks pass.
• Earlier joint source/goal, public-model consumption and arithmetic compiler records retain their own immutable pins. The compiled packet study retains all 440 fixed-schedule observations across five independent axes. It excludes preparation/proofs and retains default native predecessor arithmetic; it establishes neither strict all-depth replay nor an asymptotic timing law. No new numerical study or speedup claim is made here.

All own Lean/Lake/benchmark/browser calls are serial under a hard aggregate 32GiB cap, zero swap and LEAN_NUM_THREADS=2. The base rational umbrella remains independent. No AGENTS.md/PLAN.md edit, new axiom/admission, CI job, duplicate issue/PR, owner proof copy or downstream worker.

This remains partial implementation. Generic source/provider/predecessor/history discovery, complete automatic frontend/backend integration, accepted algebraic completeness, strict all-depth missing/reached-record coverage and general joint realization/export remain unfinished. Public presentation-model equations are merged and consumed through ordinary imports; #10377 coverage/order laws are already available. Public numeric-frame/general-export integration still needs actual reviewed and merged owner artifacts. #10633/#10634 work and its measured limitations are preserved. #10358 stays open; #10331 owns dispatch.

Mandatory fresh Opus review hit the weekly quota when this PR opened; that failed attempt is not a review. Reported availability is October19 16:00UTC. Keep draft until actual review, addressed findings and final-head green CI. Merge using gh pr merge --squash --auto without --delete-branch after those gates pass.

Refs #10358, #10331