Formalize the literal smooth Gaussian source in the Lifetime interface

frontiers/source_lifetime_realization_20261017/.gitignore

@@ -0,0 +1,3 @@
+.lake/
+__pycache__/
+*.pyc

frontiers/source_lifetime_realization_20261017/EVIDENCE_EXPORT.md

@@ -0,0 +1,13 @@
+# Exact public evidence projection
+
+The final evidence exporter preserves the full selected UTF-8 receipt, log, review, fixture and verification-program text. It replaces only three explicitly enumerated local filesystem prefixes, longest prefix first, with `@C291_ROOT@`, `@PINNED_LEAN_RUNTIME@`, and `@PINNED_DEPENDENCY_CACHE@`. Relative suffixes, process identifiers, execution times, resource limits, environment import paths, outcomes, diagnostics, multiline axiom lists, private/generated declaration names and actual agent attribution remain intact. It does not select individual receipt fields or reserialize receipt JSON.
+
+`PUBLIC_EVIDENCE_PROJECTION.json` names every exported file, its original and exported SHA-256 values and byte lengths, its evidence role, and each prefix replacement count. The public mapping lists logical labels; the corresponding private mapping retains exact machine prefixes. Original and projected hashes are deliberately distinct when text changed. A file requiring no projection retains its exact original bytes. Known private storage identifiers, storage URLs and unmatched machine paths cause the export to fail. Full output is rejected rather than silently dropped when a check cannot be satisfied.
+
+`prepare_public_evidence_inputs.py` selects the complete final nineteen-module build and five named-module standard kernel-replay receipt/start/stdout/stderr quartets, plus both preserved final-sequence failures (26 execution quartets in all); the original failed sequence, audit-recovery sequence, terminal sequence and both recovery START records; all five actual negative-control/probe executions; exact fixtures, raw single-edit clones and their manifests; the original baseline's retained instrumentation failure and separately observed proof-binding probe; full final nonauthor review and its acceptance bindings; source inventories and the terminal dependency rehash summary; and the actual verification and projection scripts. The exporter requires terminal source-bound results before writing a new final directory and refuses to overwrite an existing projection.
+
+Earlier development failures, explicitly stopped attempts and preparations remain in the immutable private handoff. The final audit timeout and first kernel child-discovery failure are also exported in full. The terminal result reuses every successful source build, permits only the documented unresolved retries, and does not replace either historical failed result. Public checkpoints and the final review describe their actual disposition. The original baseline's `control_pass: false` is preserved; the two-part acceptance does not rewrite it. The complete private dependency-artifact inventory and compiled objects remain private, while their byte hashes, dependency revisions and exact source identities are retained in the public evidence. The public verification scripts are reviewable execution/evidence source: the projected scripts and logical paths are not a standalone executable copy of the private-custody verifier. Reproducing the mathematical package uses the unchanged Lean sources and pinned Lake configuration described in the README.
+
+The local source rebuild, standard kernel replay, declaration-wide transitive axiom census, semantic mutations, nonauthor review, hosted CI, public byte readback and private custody are separate observations. Existing hosted repository gates do not register or build this new standalone Lean package. No later hosted success can be inferred from the local transcript. An OpenAI subagent review is source-exposed same-provider work, not human or provider-distinct review.
+
+After final evidence is added, the package's static checker verifies all nineteen source identities and configuration mappings, and its controls reject corrupted proof/identity/configuration/audit evidence and prohibited private paths. Exact disclosed agent identifiers are retained as provenance; a token followed by a filesystem path is still rejected. Earlier static checkpoint reports remain explicitly historical. No proof bytes, dependency pin, original target assumption, source owner or shared workflow changes as part of this projection.

frontiers/source_lifetime_realization_20261017/NEXT_TASK.md

@@ -0,0 +1,15 @@
+# Next mathematical join — offered, not claimed
+
+The new constructor supplies the literal smooth Gaussian field and its exact law/covariance interface. A useful next formal unit is a source-bound adapter from the existing compact-Morse/torus geometric hypotheses to the existing ordinary-H0 interval construction. Check current source owners and claims before pickup. This offer does not take over the separately owned elder-module registration study, reopen accepted conventional proofs, or assert that the adapter is already proved.
+
+The boundary-map source cut is Math main `c8ec07034608741585111603f1b506393c340908`, where source packet #475 is merged. Its [interface-boundary map](https://github.com/d6g8k5htny-coder/Math-/blob/c8ec07034608741585111603f1b506393c340908/frontiers/asymmetric_elder_bridge_20261017/provenance/INTERFACE_BOUNDARIES.md) (Git blob `c1f0ae9cb4b7da1bdba68bf1d678b3c39ff476e2`) distinguishes the proved geometric adapter from remaining analytic, compact-Morse, torus and all-bar joins. The map's original no-branch/no-PR wording is historical; current merged source availability is a separate observation, not new execution or alignment credit.
+
+In that source slice, `elderBoundaryDirectSummand` constructs one interval direct summand from explicit closed-domain/frontier-height/inside-ceiling/actual-higher-endpoint-path data. `elderBoundary_death_eq` relates the same Euclidean geometry to the literal C263 death. These are useful proved targets. They do not provide an exhaustive simultaneous barcode decomposition or establish once-counted bar multiplicities merely from one witness.
+
+An eligible next author should first freeze the exact conventional chart and compact-Morse source statements already carried by [the Gaussian source packet](https://github.com/d6g8k5htny-coder/Math-/blob/c8ec07034608741585111603f1b506393c340908/frontiers/gaussian_short_bar_theory_20261017/README.md) and identify the minimum missing formal adapter. Retain their dimension, compactness, distinct-critical-value, coefficient-field, period and source-law hypotheses literally; the present constructor's inclusion of dimension zero does not extend downstream theorems to that dimension. The adapter must derive geometric inputs from those source hypotheses rather than assume a desired death value, interval split, bar count or pairing conclusion.
+
+The finite acceptance boundary should state exactly whether it yields one actual ordinary-H0 summand, an endpoint-preserving bijection, or an exhaustive once-counted barcode statement. Keep elder pairing distinct from branch adjacency and quotient representatives distinct from periodic lifts. A subsequent all-small-bars converse, stochastic field-first sampling transfer or shrinking-region multiple-witness collision estimate needs its own hypotheses and evidence. Global factorial bounds do not supply the regional collision estimate. Parameter/limit order and full normalizers remain source-bound.
+
+No new review, dispatch, lease, institutional alignment or scientific promotion is created by this routing note. Existing source/integration owners and explicit stops remain effective; source-exposed same-provider AI work earns organizational-independence credit zero.
+
+The bounded architecture read through 2026-10-18 00:39:28 UTC records a pause on additional toy-control work after current integrations and directs future finite-window/count comparisons through existing Math193 owners. The actual NUM owner has conditionally adopted the qualitative ideal-law identification while retaining the finite-window, sampler, count-transfer and confidence obligations; its certified full-spectrum moment kernel is separately claimed and must not be duplicated. The proposed original-observable effective remainder is input only, with no proved remainder, assigned adapter or quantitative acceptance. See [owner adoption and retained limits](https://github.com/d6g8k5htny-coder/main/issues/275#issuecomment-6243599816) and [current owner/implementation boundaries](https://github.com/d6g8k5htny-coder/main/issues/275#issuecomment-6243819291). This proposed formal geometric join should serve that same original observable and preserve those owners and stops; it is not an additional toy experiment or a transfer of their scope.

frontiers/source_lifetime_realization_20261017/README.md

@@ -0,0 +1,43 @@
+# Source lifetime realization
+
+This standalone package provides `I4LifetimeField.actualGaussianFieldInterface (d : ℕ) (L : ℝ) (hL : 0 < L) : UniversalLaw.Spec.Lifetime.GaussianFieldInterface d L`, using the actual smooth-source probability law. The target definition and all original source assumptions are unchanged. The constructor has no extra convergence, covariance, Gaussianity, smoothness, or existence premise.
+
+The final local sequence completed on 2026-10-18 with 24 successful phases: all 19 included Lean modules were compiled from an initially empty project output directory, then the five new modules passed standard `leanchecker -v` checks. The builds used the pinned toolchain and pre-existing pinned dependency objects. The kernel checks did not use `--fresh` or an external theorem prover. The final audit inspected 409 declarations across 18 imported source, target, and control modules, including 40 private declarations; every reported transitive axiom was in `{propext, Classical.choice, Quot.sound}`. A subsequent full rehash matched the exact paths and bytes of all 83,897 inventoried dependency artifacts, totaling 8,418,477,755 bytes, with no mismatches. The dependencies themselves were not rebuilt from source.
+
+The evidence retains 26 actual final-run receipts, including two failed attempts. The first final audit hit its 420-second timeout with empty stdout and stderr. A retry of only that unresolved audit, with unchanged proof sources and a 900-second limit, succeeded in 458.501998958 seconds and reported the complete census. The first kernel invocation then failed in 3.943259375 seconds because `leanchecker` could not discover its `lean` child on `PATH`; all 19 compiled objects remained unchanged. Recovery supplied a deterministic `PATH` containing the pinned toolchain directory and four operating-system directories, checked the child executable hash, and completed the five unresolved kernel checks under 420-second limits. No successful source compilation was repeated. Both earlier sequence results and the failed attempts' START records, terminal receipts, stdout, and stderr are preserved alongside `FINAL_SEQUENCE_TERMINAL_RESULT.json`.
+
+Seven source mutations were rejected in their intended diagnostic ranges: a zero field, a shifted field, a zero measure, a hidden positive-dimension premise, doubled raw covariance, the wrong covariance argument, and a negated covariance quadratic form. A separate fixture containing a private unused custom axiom compiled successfully, and the whole-module audit rejected that axiom. The positive baseline compiled successfully; its original wrapper failure caused by proof-print elision remains preserved. A separate probe printed the 21 required local helper references from the original compiled baseline objects, supporting the recorded two-part acceptance. The nonauthor reviewer's read-only terminal-execution verifier passed 579 checks, and the actual mutation-evidence verifier passed 265 checks.
+
+Earlier development evidence remains historical evidence. All five new modules have successful development compile receipts bound to the included source bytes. The development axiom audit completed with exit 0 in 351.246865417 seconds on 2026-10-17 and reported the same 409-declaration, 18-module census. Those development runs used inherited project objects; the subsequent 19-module source rebuild and five kernel checks are recorded separately.
+
+The constructor supplies all eleven fields of the original interface:
+
+| Original field | Supplied realization |
+| --- | --- |
+| `Ω` | The existing `SmoothSample d L` carrier. |
+| `mΩ` | Its existing measurable space. |
+| `P` | The literal existing `smoothLaw d L`. |
+| `isProb` | The source law is a probability measure. |
+| `F` | `smoothSourceField d L` transported through the canonical Euclidean coordinates. |
+| `smooth` | Every sample is `ContDiff ℝ n` for every finite order `n`. |
+| `periodic` | Every sample is invariant under every integer-lattice translation of side length `L`. |
+| `summable` | The exact shifted image-space theta family is summable at every point. |
+| `quad_nonneg` | The exact covariance quadratic form is nonnegative for every finite evaluation family and real coefficient family. |
+| `gaussian` | Every finite real linear combination has exactly the centered Gaussian law with that quadratic-form variance. |
+| `covariance` | The raw product integral equals the original normalized periodic covariance. |
+
+The theta bridge proves the full multidimensional normalization, including the factor `(sqrt (2*pi)/L)^d` and the full zero-lag lattice sum. It uses absolutely convergent complex products before taking real parts. Dimensions `d = 0`, empty evaluation families, repeated points, and cancelling coefficients are retained; no strict positive-variance assumption or division by variance is introduced. The raw covariance identity uses the established zero means.
+
+The 13 source modules and `Lifetime.lean` are byte-identical snapshots in `inputs/`. The five new files are `SourceThetaBridge.lean`, `SourceLifetimeGeometry.lean`, `SourceLifetimeField.lean`, `SourceLifetimeControls.lean`, and `SourceLifetimeAxiomAudit.lean`. `inputs/provenance/FILE_IDENTITIES.json` binds all 19 Lean files and the three preserved original build files by SHA-256 and Git blob identity. The active dependency manifest adapts only the top-level package name; all nine dependency records remain unchanged. Lean is pinned to `leanprover/lean4:v4.34.1`, and Mathlib to `d13f23b723b8a846827a245b89c10fc7d3f11612`.
+
+`C291Inputs` uses `srcDir = "inputs"` with explicit original module roots. The default Lake targets are `C291Inputs`, `SourceLifetimeControls`, and `SourceLifetimeAxiomAudit`. The intended ordinary build command is `lake build` from this directory with the pinned toolchain and dependencies available. That command has not been executed; the local source-build and kernel-replay evidence comes from the recorded direct invocations. A lockfile alone does not make Lake offline: absent checkouts or pinned revisions can cause dependency materialization. The hosted gate status for this new standalone package is `NOT_REGISTERED_NOT_CLAIMED`. Existing repository gates do not automatically build it, and this package adds no workflow.
+
+Run `python3 -B validate_static.py` for source identities, mappings, dependency-lock consistency, direct import classification, receipt bindings, and consistency of the recorded development audit output. Optional `--mathlib-source PATH` and `--lean-source PATH` arguments check direct imported source files in pre-existing pinned source trees. The checker uses a restricted parser for the generated TOML subset; it does not execute the Lake loader or Lean. Run `python3 -B test_static_validator.py` for read-only controls that require corrupted proof bytes, changed dependency pins, missing audit targets/identities, and inconsistent or forbidden-axiom audit output to be rejected. Python optimization is rejected explicitly so assertions cannot silently disappear.
+
+Evidence lives in `evidence/`; exact earlier scaffold reports are preserved under `evidence/history/scaffold-17modules/`, and the later development-checkpoint static reports under `evidence/history/pre-final-export-19modules/`. These historical reports are not current package verification. The final export is in `evidence/final/`, including `FINAL_SEQUENCE_TERMINAL_RESULT.json`, complete run records, dependency-rehash results, negative fixtures and receipts, and the full nonauthor review. `EVIDENCE_EXPORT.md` describes the projection of actual records without machine-specific paths, preserving both original and exported file hashes. The audit's narrower imports are recorded in its exact source identity; the completed runs do not establish that an import change was the sole cause of the earlier timing behavior.
+
+This constructor does not construct critical-point or persistence-bar measures, prove Morse genericity, identify elder pairing with branch adjacency, convert contact integrals into once-counted bars, prove an all-small-bars converse, or close a regional shrinking multiple-witness collision bound. Global factorial estimates do not discharge that regional obligation. The lifetime-density exponent, cumulative short-bar law, and full universality conclusions do not follow from this package alone. No scientific register is promoted by this checkpoint.
+
+The completed nonauthor review accepts the exact literal constructor and observed local formal evidence with verdict `ACCEPT_SCOPED_FORMAL_CONSTRUCTOR`. Its author, OpenAI Codex `/root/c291_nonauthor_review`, read the implementation and actual results without authoring or editing the production Lean sources. This is source-exposed review by the same provider and session lineage: organizational-independence credit is `0`, and scientific effect is `NONE`. The full report is [NONAUTHOR_REVIEW.md](evidence/final/NONAUTHOR_REVIEW.md). Its acceptance excludes publication, hosted CI, private custody, and the final delivery-master gate, which remain separate delivery observations.
+
+The original smooth-source integration remains separately owned and identified by its commit and path; including unchanged snapshots does not change its merge status. The intended package destination is `frontiers/source_lifetime_realization_20261017/`, without modifying existing source paths or workflows. This is delegated AI implementation and packaging work for Dylan Roy, performed by OpenAI Codex agents; no human or provider-distinct review, merge, or scientific acceptance is claimed.