Tiered Formal and Numerical Methods for T-Duality and Frontier String Dynamics on K3 × T²: Closing the Loop via LeanFlow Stiff Solvers with Native Duality, Topological Data Analysis, and Lean 4 Checking

Corrected version of the manuscript and its reproducible artifacts. This version supersedes Zenodo record 22683565 (DOI 10.5281/zenodo.22683565) and withdraws claims made there; see the Correction notices in the manuscript. New in this version (2026-09-21): corrections found by bridging to an external Lean 4 formalization. The full evidence record, with reproduction commands, is included as STREAM1_BRIDGE.md; the pre-registration and its addendum A10 are included as PRE_REGISTRATION.md. The Fricke point was misstated. The manuscript named it tau = i. The implemented potential is stationary at tau = i/sqrt(12) (dV/dy = 0) and not at tau = i (dV/dy = 1.423). By the self-dual locus N*tau^2 = -1 these are levels 1 and 12, and level 12 is what the repository uses elsewhere. Corrected in 10 places across 4 files. A numerics defect in the invariant-projection layer. The solver applied S : tau -> -1/tau to the solution array after integration, but the implemented potential is not S-invariant (measured max |V(S tau) - V(tau)| = 8.77, against 6.7e-16 for T : tau -> tau + 1), so the fold moved trajectory points to physically inequivalent points. The S-step is now off by default. Folding under Gamma_0(12)+ would not have been valid either (35.81): the potential is a hand-built double well with no modular symmetry. The projections were applied to the wrong state components. Both used state indices (0,1), but the cosmology state is [a, x, y, u, v]: index 0 is the scale factor and Im(tau) is at index 2. The scale factor was being folded (1.98e9 reported folds on one run) and Re(tau), legitimately 0 at the Fricke point and 0.5 at the orbifold point, was clamped to 1/sqrt(12). The solver now requires explicit modulus indices. Blast radius, measured. No committed simulation artifact is affected: workshopcosmo.py imports no leanflow module (verified in a clean interpreter) and calls SciPy directly. On the leanflow solver path the change is large -- the old fold moved 100% of trajectory points, max |dy| = 3.175 -- so numbers from that path predating 2026-09-21 should not be trusted. A previously untraceable number is now identified. The reported min(y) = 0.289 is 1/sqrt(12) = 0.28867..., the value of the metric-positivity clamp, not a minimum attained by any trajectory. It is withdrawn as a physical result. The 'Dual-Tier Execution Architecture' section described a system that does not exist. There are no Rust contract assertions in any inner loop (all 41 asserts in rust_simulator/src/ are inside #[cfg(test)] modules and are compiled out of release builds); there is no SIMD anywhere in the crate; the metric-positivity and Weak Energy Condition bounds are Python and are applied after integration, not during time-stepping; and the 'non-blocking Unix domain socket IPC / C-FFI with JSON-RPC' is in fact a blocking subprocess CLI call with a 15 s timeout. All four withdrawn. A false claim in paper-support code. t_duality_calculus.py printed 'Symmetric square modular invariant verified for L_3 = Sym^2 L_2' whenever c_eff == 1701, an unrelated arithmetic identity that could never fail; and the relation is wrong as stated, since the kernel-proved form carries a non-trivial prefactor, L_3 = P_2 . Sym^2(L_2) with P_2 = 1 - 26z - 27z^2.Parameter count, stated by tier. Dolgachev (1996) Thm 7.1 -- literature, Tier L, not kernel-proved -- gives the coarse moduli space of M_n-polarized K3 surfaces as the Fricke modular curve H/Gamma_0(n)+, a curve, hence ONE modulus. The programme's earlier target of zero free parameters by derivation is therefore unreachable on the mathematics side, where the floor is one, not zero. Reading that modulus as a cosmological free parameter is Tier C and is NOT registered as a prediction. The external formalization states program-wide that no exact physical observable exists anywhere in it, that the Sym^2 relation supplies no physical coupling, and that the coincidence between the Fricke involution and the Narain T-duality generator is a fact about a lattice isometry and not a physical identification. Kernel-checked dependencies, pinned by commit. SocrateAI-DualScaleTopologicalUniverseModel-LeanProposal at commit bb74acb56f386a97e433f94eb0b2632ed03bc4ca (DOI 10.5281/zenodo.22853239), zero sorry; and SocrateAI-Scientific-Agora-LeanMaster at commit ede49f06800cde8177867c02bb08d44f7be275c5 (v3.44.0). Transcribed into leanflow/core/gamma0n_plus.py and guarded by 34 tests. Status of the remaining contents, by evidence tier. (1) The integer O(d,d;Z) T-duality charge action and generalized metric at B = 0, K3/Mukai/K3xT2 lattice signatures, flux-tadpole arithmetic and Mathieu-moonshine dimension facts are kernel-checked in LeanMaster and restated in lean_foundation/. They do not cover the field-level Buscher rules for metric, B-field and dilaton. (2) Local Lean files in proofs/ are superseded and are not a verification of the physics they name: BuscherRules.lean rests on five global axioms, one of which (inv_inv) proves False when instantiated at Nat. (3) All simulation telemetry in this bundle was REGENERATED on 2026-09-21 through the documented workshopcosmo driver with every stochastic stage seeded, and verified byte-identical across three independent full reruns; TELEMETRY_PROVENANCE.json records the commands, seeds, resolved configs, toolchain versions and sha256 of every file. This was possible only after fixing two defects found in the attempt: the Rust binary parsed only --mode and silently ignored the --grid-size / --t-max flags that the documented driver passes, so its outputs could not be reproduced from the command that supposedly made them; and the TDA Mapper defaulted to an unseeded run. The telemetry remains EXPLORATORY and no manuscript number derives from it (verified by grep). Equivalence-class counts are configuration-dependent. (4) No benchmark or cost figure is claimed; the external rusty-SUNDIALS integrator is not present in this repository and was not used.