From 1f38a851595bc0664b543aeb59b462817ca3b8f9 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 13 Oct 2026 05:44:07 -0700 Subject: [PATCH] Construct the actual all-order smooth Gaussian source carrier Add the literal source-bound C261A prerequisite and its prospective full-module audit. Preserve the reviewed frozen source and ten exact F7 dependencies. Qualify the new package through one fresh hosted event with durable failed-admission capture; compilation and kernel outcomes remain unrun at commit creation. --- .../workflows/source-smooth-realization.yml | 559 ++++++++++++++++++ .../.gitignore | 1 + .../DESIGN.md | 54 ++ .../GaussianSeriesFoundation.lean | 96 +++ .../SOURCE_MANIFEST.json | 294 +++++++++ .../SOURCE_SHA256SUMS | 20 + .../SourceC4.lean | 141 +++++ .../SourceCovariance.lean | 74 +++ .../SourceFourierSeries.lean | 147 +++++ .../SourceGaussianLaw.lean | 189 ++++++ .../SourceKernel.lean | 112 ++++ .../SourceLattice.lean | 159 +++++ .../SourceSmooth.lean | 253 ++++++++ .../SourceSmoothAxiomAudit.lean | 68 +++ .../SourceSmoothCarrier.lean | 230 +++++++ .../SourceSmoothControls.lean | 67 +++ .../SourceTorus.lean | 111 ++++ .../SourceTorusC4.lean | 134 +++++ .../SpectralWeights.lean | 160 +++++ .../lake-manifest.json | 117 ++++ .../lakefile.toml | 47 ++ .../lean-toolchain | 1 + 22 files changed, 3034 insertions(+) create mode 100644 .github/workflows/source-smooth-realization.yml create mode 100644 frontiers/source_smooth_realization_20261011/.gitignore create mode 100644 frontiers/source_smooth_realization_20261011/DESIGN.md create mode 100644 frontiers/source_smooth_realization_20261011/GaussianSeriesFoundation.lean create mode 100644 frontiers/source_smooth_realization_20261011/SOURCE_MANIFEST.json create mode 100644 frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS create mode 100644 frontiers/source_smooth_realization_20261011/SourceC4.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceCovariance.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceFourierSeries.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceGaussianLaw.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceKernel.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceLattice.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceSmooth.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceSmoothAxiomAudit.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceSmoothCarrier.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceSmoothControls.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceTorus.lean create mode 100644 frontiers/source_smooth_realization_20261011/SourceTorusC4.lean create mode 100644 frontiers/source_smooth_realization_20261011/SpectralWeights.lean create mode 100644 frontiers/source_smooth_realization_20261011/lake-manifest.json create mode 100644 frontiers/source_smooth_realization_20261011/lakefile.toml create mode 100644 frontiers/source_smooth_realization_20261011/lean-toolchain diff --git a/.github/workflows/source-smooth-realization.yml b/.github/workflows/source-smooth-realization.yml new file mode 100644 index 000000000..d65614851 --- /dev/null +++ b/.github/workflows/source-smooth-realization.yml @@ -0,0 +1,559 @@ +# Inert C261A successor under ROOT claim753d8557-c148-4ef8-bfab-1656ab5f0205. No native runtime admission is created by this file. +# Strict first-source guard: 2026-10-13T13:16:47.305Z. +# Documentary target: 2026-10-13T14:06:47.305Z; lease: 2026-10-13T14:16:47.305Z. +# ROOT must declare/read back exact native head/tree/workflow/list and complete diff before ref/PR publication. +# Historical frozen source manifest claim e2f875ef... is provenance, not this current admission. +name: Actual all-orders smooth source carrier hosted qualification + +'on': + pull_request: + types: [opened] + paths: + - 'frontiers/source_smooth_realization_20261011/**' + - '.github/workflows/source-smooth-realization.yml' + +permissions: + contents: read + +concurrency: + group: source-smooth-realization-${{ github.ref }} + cancel-in-progress: false + +jobs: + first-leaf: + runs-on: ubuntu-latest + timeout-minutes: 30 + env: + LEAN_NUM_THREADS: '2' + CLAIM_UUID: '753d8557-c148-4ef8-bfab-1656ab5f0205' + SOURCE_GUARD_UTC: '2026-10-13T13:16:47.305Z' + EXPECTED_HEAD_REF: 'codex/source-smooth-realization-20261013-root01a11cbf' + HISTORICAL_MANIFEST_CLAIM_UUID: 'e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6' + EXPECTED_SOURCE_LIST_SHA256: '0d78987b8baa27ce0917e126945ccff0261af74b3461722ae4f4768f62fb78eb' + EXPECTED_SOURCE_MANIFEST_SHA256: '56acfdbf20fd7645872f2ce3a60beb1186908dc4f7994d14b175ddc93106b65d' + EXPECTED_BASE_SHA: '1a7fc4be83043f2e313927019db85fff61eeac3f' + EXPECTED_BASE_TREE: '3b3c0f16f848712a9eb53bb1b412a06bab787b91' + EXPECTED_BASE_REF: 'codex/compact-cutoff-proper-partial-repair-20261011-root01a11cbf' + defaults: + run: + shell: bash + working-directory: frontiers/source_smooth_realization_20261011 + steps: + - name: Record and guard the first opened event before checkout + id: precheckout + timeout-minutes: 1 + working-directory: ${{ runner.temp }} + env: + EVENT_ACTION: ${{ github.event.action }} + EVENT_NUMBER: ${{ github.event.pull_request.number }} + EVENT_HEAD: ${{ github.event.pull_request.head.sha }} + EVENT_HEAD_REF: ${{ github.event.pull_request.head.ref }} + EVENT_HEAD_REPOSITORY: ${{ github.event.pull_request.head.repo.full_name }} + EVENT_BASE: ${{ github.event.pull_request.base.ref }} + EVENT_BASE_SHA: ${{ github.event.pull_request.base.sha }} + EVENT_WORKFLOW_SHA: ${{ github.workflow_sha }} + run: | + set -u -o pipefail + set +e + evidence_dir="$RUNNER_TEMP/source-smooth-realization-precheckout" + mkdir -p "$evidence_dir" || exit 80 + phase_start=$SECONDS + date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/precheckout-guard-start.txt" + ( + set -euo pipefail + printf 'claim_uuid=%s\nstrict_source_guard=%s\nrun=%s\nattempt=%s\nevent=%s\naction=%s\npr=%s\nref=%s\nevent_head=%s\nevent_head_ref=%s\nevent_head_repository=%s\nevent_base=%s\nevent_base_sha=%s\nexpected_merge_sha=%s\nworkflow_git_sha=%s\nworkflow_content_sha256=UNAVAILABLE_BEFORE_CHECKOUT\nexternal_head_tree_workflow_binding=DECLARED_EXTERNALLY\nthreads=%s\ncheckout_status=NOT_ESTABLISHED\nhistorical_manifest_claim_uuid=%s\nhistorical_manifest_claim_is_current_admission=false\n' "$CLAIM_UUID" "$SOURCE_GUARD_UTC" "$GITHUB_RUN_ID" "$GITHUB_RUN_ATTEMPT" "$GITHUB_EVENT_NAME" "$EVENT_ACTION" "$EVENT_NUMBER" "$GITHUB_REF" "$EVENT_HEAD" "$EVENT_HEAD_REF" "$EVENT_HEAD_REPOSITORY" "$EVENT_BASE" "$EVENT_BASE_SHA" "$GITHUB_SHA" "$EVENT_WORKFLOW_SHA" "$LEAN_NUM_THREADS" "$HISTORICAL_MANIFEST_CLAIM_UUID" > "$evidence_dir/context.txt" + test "$(date -u +%s%3N)" -lt "$(date -u -d "$SOURCE_GUARD_UTC" +%s%3N)" + test "$GITHUB_EVENT_NAME" = pull_request + test "$EVENT_ACTION" = opened + test "$GITHUB_RUN_ATTEMPT" = 1 + test "$EVENT_HEAD_REF" = "$EXPECTED_HEAD_REF" + test "$EVENT_HEAD_REPOSITORY" = d6g8k5htny-coder/Math- + test "$EVENT_BASE" = "$EXPECTED_BASE_REF" + test "$EVENT_BASE_SHA" = "$EXPECTED_BASE_SHA" + [[ "$EVENT_NUMBER" =~ ^[0-9]+$ ]] + [[ "$EVENT_HEAD" =~ ^[0-9a-f]{40}$ ]] + test "$GITHUB_REF" = "refs/pull/$EVENT_NUMBER/merge" + ) > "$evidence_dir/precheckout-guard.stdout" 2> "$evidence_dir/precheckout-guard.stderr" + status=$? + printf '%s\n' "$status" > "$evidence_dir/precheckout-guard-exit.txt" + printf '%s\n' "$((SECONDS-phase_start))" > "$evidence_dir/precheckout-guard-seconds.txt" + date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/precheckout-guard-end.txt" + cat "$evidence_dir/precheckout-guard.stdout" + cat "$evidence_dir/precheckout-guard.stderr" >&2 + exit "$status" + - timeout-minutes: 1 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + id: checkout + with: + fetch-depth: 2 + persist-credentials: false + - name: Validate one fresh admitted source checkout before setup + timeout-minutes: 1 + id: sources + working-directory: ${{ runner.temp }} + env: + EVENT_ACTION: ${{ github.event.action }} + EVENT_NUMBER: ${{ github.event.pull_request.number }} + EVENT_HEAD: ${{ github.event.pull_request.head.sha }} + EVENT_HEAD_REF: ${{ github.event.pull_request.head.ref }} + EVENT_HEAD_REPOSITORY: ${{ github.event.pull_request.head.repo.full_name }} + EVENT_WORKFLOW_SHA: ${{ github.workflow_sha }} + EVENT_BASE: ${{ github.event.pull_request.base.ref }} + EVENT_BASE_SHA: ${{ github.event.pull_request.base.sha }} + run: | + set -u -o pipefail + set +e + evidence_dir="$RUNNER_TEMP/source-smooth-realization-precheckout" + mkdir -p "$evidence_dir" || exit 80 + phase_start=$SECONDS + date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/source-guard-start.txt" + ( + set -euo pipefail + printf 'claim_uuid=%s\nstrict_source_guard=%s\nevent_head_ref=%s\nworkflow_git_sha=%s\nexternal_head_tree_workflow_binding=DECLARED_EXTERNALLY\nhistorical_manifest_claim_uuid=%s\nhistorical_manifest_claim_is_current_admission=false\n' "$CLAIM_UUID" "$SOURCE_GUARD_UTC" "$EVENT_HEAD_REF" "$EVENT_WORKFLOW_SHA" "$HISTORICAL_MANIFEST_CLAIM_UUID" > "$evidence_dir/source-guard-context.txt" + sha256sum "$GITHUB_WORKSPACE/.github/workflows/source-smooth-realization.yml" > "$evidence_dir/workflow-source-guard-actual.sha256" + test ! -L "$GITHUB_WORKSPACE/frontiers" + test ! -L "$GITHUB_WORKSPACE/frontiers/source_smooth_realization_20261011" + cd "$GITHUB_WORKSPACE/frontiers/source_smooth_realization_20261011" + set -euo pipefail + mkdir -p .lake/evidence + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/start-utc.txt + git rev-parse HEAD > .lake/evidence/checkout-sha.txt + git rev-parse HEAD^{tree} > .lake/evidence/checkout-tree.txt + git rev-parse HEAD^1 > .lake/evidence/checkout-base-parent.txt + git rev-parse HEAD^2 > .lake/evidence/checkout-head-parent.txt + printf 'event=%s\naction=%s\npr=%s\nref=%s\nhead=%s\nbase=%s\nbase_sha=%s\nmerge=%s\nrun=%s\nattempt=%s\nthreads=%s\n' "$GITHUB_EVENT_NAME" "$EVENT_ACTION" "$EVENT_NUMBER" "$GITHUB_REF" "$EVENT_HEAD" "$EVENT_BASE" "$EVENT_BASE_SHA" "$GITHUB_SHA" "$GITHUB_RUN_ID" "$GITHUB_RUN_ATTEMPT" "$LEAN_NUM_THREADS" > .lake/evidence/context.txt + test "$(date -u +%s%3N)" -lt "$(date -u -d "$SOURCE_GUARD_UTC" +%s%3N)" + test "$GITHUB_EVENT_NAME" = pull_request + test "$GITHUB_RUN_ATTEMPT" = 1 + test "$EVENT_ACTION" = opened + test "$EVENT_HEAD_REF" = "$EXPECTED_HEAD_REF" + test "$EVENT_HEAD_REPOSITORY" = d6g8k5htny-coder/Math- + [[ "$EVENT_NUMBER" =~ ^[0-9]+$ ]] + test "$GITHUB_REF" = "refs/pull/$EVENT_NUMBER/merge" + test "$EVENT_BASE" = "$EXPECTED_BASE_REF" + test "$EVENT_BASE_SHA" = "$EXPECTED_BASE_SHA" + [[ "$EVENT_HEAD" =~ ^[0-9a-f]{40}$ ]] + [[ "$EVENT_BASE_SHA" =~ ^[0-9a-f]{40}$ ]] + test "$(cat .lake/evidence/checkout-sha.txt)" = "$GITHUB_SHA" + test "$(cat .lake/evidence/checkout-base-parent.txt)" = "$EVENT_BASE_SHA" + test "$(cat .lake/evidence/checkout-head-parent.txt)" = "$EVENT_HEAD" + git rev-parse 'HEAD^1^{tree}' > .lake/evidence/base-tree.txt + git rev-parse 'HEAD^2^{tree}' > .lake/evidence/selected-head-tree.txt + test "$(cat .lake/evidence/base-tree.txt)" = "$EXPECTED_BASE_TREE" + cmp -s .lake/evidence/checkout-tree.txt .lake/evidence/selected-head-tree.txt + git cat-file -p "$EVENT_HEAD" | awk '$1 == "parent" { print $2 }' > .lake/evidence/selected-head-parents.txt + printf '%s\n' "$EXPECTED_BASE_SHA" | cmp -s - .lake/evidence/selected-head-parents.txt + sha256sum "$(git rev-parse --show-toplevel)/.github/workflows/source-smooth-realization.yml" > .lake/evidence/workflow-actual.sha256 + [[ "$EXPECTED_SOURCE_LIST_SHA256" =~ ^[0-9a-f]{64}$ ]] + test ! -e .lake/build + command -v jq timeout sha256sum cmp awk find sort + printf 'leanprover/lean4:v4.34.1\n' | cmp -s - lean-toolchain + test "$(wc -l < SOURCE_SHA256SUMS)" -eq 20 + if grep -Evq '^[0-9a-f]{64} [A-Za-z0-9._/-]+$' SOURCE_SHA256SUMS; then exit 82; fi + cp SOURCE_SHA256SUMS .lake/evidence/SOURCE_SHA256SUMS + sha256sum SOURCE_SHA256SUMS > .lake/evidence/checksum-list-identity-before.txt + test "$(sha256sum SOURCE_SHA256SUMS | cut -d' ' -f1)" = "$EXPECTED_SOURCE_LIST_SHA256" + test "$(sha256sum SOURCE_MANIFEST.json | cut -d' ' -f1)" = "$EXPECTED_SOURCE_MANIFEST_SHA256" + jq -e '.package == "frontiers/source_smooth_realization_20261011" and .source_claim.uuid == "e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6" and .parent.commit == "1a7fc4be83043f2e313927019db85fff61eeac3f" and .parent.tree == "3b3c0f16f848712a9eb53bb1b412a06bab787b91" and (.files | length) == 19 and ([.files[].bytes] | add) == 96872' SOURCE_MANIFEST.json > .lake/evidence/source-manifest-contract.txt + cp SOURCE_MANIFEST.json .lake/evidence/SOURCE_MANIFEST.json + cp SourceSmoothAxiomAudit.lean .lake/evidence/SourceSmoothAxiomAudit.lean + awk '{ print $2 }' SOURCE_SHA256SUMS | LC_ALL=C sort > .lake/evidence/list-members.txt + jq -r '.files[].path' SOURCE_MANIFEST.json > .lake/evidence/payload-members.txt + { cat .lake/evidence/payload-members.txt; printf '%s\n' SOURCE_MANIFEST.json; } | LC_ALL=C sort > .lake/evidence/manifest-and-payload-members.txt + cmp -s .lake/evidence/list-members.txt .lake/evidence/manifest-and-payload-members.txt + { cat .lake/evidence/list-members.txt; printf '%s\n' SOURCE_SHA256SUMS; } | LC_ALL=C sort > .lake/evidence/package-members-required.txt + test "$(wc -l < .lake/evidence/package-members-required.txt)" -eq 21 + git ls-files -- . | LC_ALL=C sort > .lake/evidence/package-members-tracked.txt + cmp -s .lake/evidence/package-members-required.txt .lake/evidence/package-members-tracked.txt + find . -path './.lake' -prune -o -type f -printf '%P\n' | LC_ALL=C sort > .lake/evidence/package-members-filesystem.txt + cmp -s .lake/evidence/package-members-required.txt .lake/evidence/package-members-filesystem.txt + while IFS= read -r file; do test -f "$file"; test ! -L "$file"; done < .lake/evidence/package-members-required.txt + grep -Fxq '#print axioms I4Smooth.sourceField_smooth_ae' SourceSmoothAxiomAudit.lean + grep -Fxq '#print axioms I4SmoothCarrier.sampleInclusion_map' SourceSmoothAxiomAudit.lean + grep -Fxq '#print axioms I4SmoothCarrier.smoothLaw_isProbabilityMeasure' SourceSmoothAxiomAudit.lean + grep -Fxq '#print axioms I4SmoothCarrier.smoothSourceField_finiteVector_hasGaussianLaw' SourceSmoothAxiomAudit.lean + grep -Fxq '#print axioms I4SmoothCarrier.smoothTorusSourceField_smooth' SourceSmoothAxiomAudit.lean + sha256sum -c SOURCE_SHA256SUMS | tee .lake/evidence/sources-before.txt + while IFS= read -r line; do + file="${line#* }" + test "$file" != "$line" + sha256sum -- "$file" + done < SOURCE_SHA256SUMS > .lake/evidence/sources-actual-before.sha256 + sha256sum SOURCE_SHA256SUMS >> .lake/evidence/sources-actual-before.sha256 + git diff --exit-code + ) > "$evidence_dir/source-guard.stdout" 2> "$evidence_dir/source-guard.stderr" + status=$? + printf '%s\n' "$status" > "$evidence_dir/source-guard-exit.txt" + printf '%s\n' "$((SECONDS-phase_start))" > "$evidence_dir/source-guard-seconds.txt" + date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/source-guard-end.txt" + cat "$evidence_dir/source-guard.stdout" + cat "$evidence_dir/source-guard.stderr" >&2 + exit "$status" + - name: Install pinned Lean and retrieve qualified Mathlib cache + timeout-minutes: 3 + id: setup + uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 + with: + lake-package-directory: frontiers/source_smooth_realization_20261011 + auto-config: 'false' + build: 'false' + test: 'false' + lint: 'false' + use-mathlib-cache: 'true' + use-github-cache: 'false' + - name: Check hosted versions pins and actual post-setup source hashes + timeout-minutes: 1 + id: pincheck + run: | + set -euo pipefail + lean --version | tee .lake/evidence/lean-version.txt + grep -Eq '^Lean \(version 4\.34\.1([, ]|\))' .lake/evidence/lean-version.txt + lake --version | tee .lake/evidence/lake-version.txt + grep -Fxq 'Lake version 5.0.0-src+5045d00 (Lean version 4.34.1)' .lake/evidence/lake-version.txt + jq --version > .lake/evidence/jq-version.txt + uname -a > .lake/evidence/platform.txt + cp lake-manifest.json .lake/evidence/lake-manifest.json + sha256sum lake-manifest.json > .lake/evidence/manifest-identity.txt + sha256sum SOURCE_SHA256SUMS > .lake/evidence/checksum-list-identity-after-setup.txt + cmp -s .lake/evidence/checksum-list-identity-before.txt .lake/evidence/checksum-list-identity-after-setup.txt + sha256sum -c SOURCE_SHA256SUMS > .lake/evidence/sources-after-setup.txt + while IFS= read -r line; do + file="${line#* }" + test "$file" != "$line" + sha256sum -- "$file" + done < SOURCE_SHA256SUMS > .lake/evidence/sources-actual-after-setup.sha256 + sha256sum SOURCE_SHA256SUMS >> .lake/evidence/sources-actual-after-setup.sha256 + cmp -s .lake/evidence/sources-actual-before.sha256 .lake/evidence/sources-actual-after-setup.sha256 + jq -r '.packages[] | [.name, .rev] | @tsv' lake-manifest.json > .lake/evidence/dependency-expected.tsv + test "$(wc -l < .lake/evidence/dependency-expected.tsv)" -eq 9 + cat > .lake/evidence/dependency-pins-required.tsv <<'PINS' + plausible 118aa17ee84656b8bd727fef7c458ee8c833385c + LeanSearchClient ddf04cf3949fa556442341e87d47f9f6e6074707 + importGraph e928b72544873815af278d38681b31c0293588e3 + proofwidgets 106ff4fafc74ef4ac99d81dbf3ab399118f497a5 + aesop 355695d523e41d0554926416cba2a2b3544fbbc9 + Qq 6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259 + batteries f2effa3d803fda822b1f97b806c47cf2adfbcbc2 + Cli e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204 + mathlib d13f23b723b8a846827a245b89c10fc7d3f11612 + PINS + cmp -s .lake/evidence/dependency-pins-required.tsv .lake/evidence/dependency-expected.tsv + while IFS=$'\t' read -r package revision; do + actual=$(git -C ".lake/packages/$package" rev-parse HEAD) + printf '%s\t%s\t%s\n' "$package" "$revision" "$actual" >> .lake/evidence/dependency-actual.tsv + test "$actual" = "$revision" + done < .lake/evidence/dependency-expected.tsv + git diff --exit-code + - name: Build all ten literal F7 baseline source modules once + timeout-minutes: 10 + id: predecessor + run: | + set -euo pipefail + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/predecessor-start.txt + phase_start=$SECONDS + set +e + timeout --signal=TERM --kill-after=15s 540s lake build GaussianSeriesFoundation SpectralWeights SourceFourierSeries SourceC4 SourceGaussianLaw SourceLattice SourceKernel SourceCovariance SourceTorus SourceTorusC4 > .lake/evidence/predecessor.stdout 2> .lake/evidence/predecessor.stderr + status=$? + set -e + printf '%s\n' "$status" > .lake/evidence/predecessor-exit.txt + printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/predecessor-seconds.txt + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/predecessor-end.txt + cat .lake/evidence/predecessor.stdout + cat .lake/evidence/predecessor.stderr >&2 + exit "$status" + - name: Compile both smooth source proof modules once and propagate actual exit + timeout-minutes: 2 + id: proof + run: | + set -euo pipefail + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/proof-start.txt + phase_start=$SECONDS + set +e + timeout --signal=TERM --kill-after=15s 90s lake build SourceSmooth SourceSmoothCarrier > .lake/evidence/proof.stdout 2> .lake/evidence/proof.stderr + status=$? + set -e + printf '%s\n' "$status" > .lake/evidence/proof-exit.txt + printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/proof-seconds.txt + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/proof-end.txt + cat .lake/evidence/proof.stdout + cat .lake/evidence/proof.stderr >&2 + exit "$status" + - name: Compile smooth source controls once and propagate actual exit + timeout-minutes: 2 + id: controls + run: | + set -euo pipefail + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/controls-start.txt + phase_start=$SECONDS + set +e + timeout --signal=TERM --kill-after=15s 90s lake build SourceSmoothControls > .lake/evidence/controls.stdout 2> .lake/evidence/controls.stderr + status=$? + set -e + printf '%s\n' "$status" > .lake/evidence/controls-exit.txt + printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/controls-seconds.txt + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/controls-end.txt + cat .lake/evidence/controls.stdout + cat .lake/evidence/controls.stderr >&2 + exit "$status" + - name: Recheck all three new compiled modules with the standalone kernel checker + id: kernel + timeout-minutes: 2 + run: | + set -euo pipefail + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/kernel-start.txt + phase_start=$SECONDS + set +e + timeout --signal=TERM --kill-after=15s 90s bash -c 'set -euo pipefail; printf "KERNEL_MODULE SourceSmooth\n"; lake env leanchecker SourceSmooth; printf "KERNEL_MODULE SourceSmoothCarrier\n"; lake env leanchecker SourceSmoothCarrier; printf "KERNEL_MODULE SourceSmoothControls\n"; lake env leanchecker SourceSmoothControls' > .lake/evidence/kernel.stdout 2> .lake/evidence/kernel.stderr + status=$? + set -e + printf '%s\n' "$status" > .lake/evidence/kernel-exit.txt + printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/kernel-seconds.txt + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/kernel-end.txt + cat .lake/evidence/kernel.stdout + cat .lake/evidence/kernel.stderr >&2 + exit "$status" + - name: Audit complete actual thirteen-module declarations and four private guards + timeout-minutes: 2 + id: audit + run: | + set -euo pipefail + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/audit-start.txt + phase_start=$SECONDS + set +e + timeout --signal=TERM --kill-after=15s 90s lake env lean SourceSmoothAxiomAudit.lean > .lake/evidence/audit.stdout 2> .lake/evidence/audit.stderr + status=$? + set -e + printf '%s\n' "$status" > .lake/evidence/audit-exit.txt + printf '%s\n' "$((SECONDS-phase_start))" > .lake/evidence/audit-seconds.txt + date -u +%Y-%m-%dT%H:%M:%SZ > .lake/evidence/audit-end.txt + cat .lake/evidence/audit.stdout + cat .lake/evidence/audit.stderr >&2 + exit "$status" + - name: Retain checkout and phase outcomes even if checkout fails + timeout-minutes: 1 + if: always() + working-directory: ${{ runner.temp }} + env: + PRECHECKOUT_OUTCOME: ${{ steps.precheckout.outcome }} + CHECKOUT_OUTCOME: ${{ steps.checkout.outcome }} + SOURCE_OUTCOME: ${{ steps.sources.outcome }} + SETUP_OUTCOME: ${{ steps.setup.outcome }} + PINCHECK_OUTCOME: ${{ steps.pincheck.outcome }} + PREDECESSOR_OUTCOME: ${{ steps.predecessor.outcome }} + PROOF_OUTCOME: ${{ steps.proof.outcome }} + CONTROLS_OUTCOME: ${{ steps.controls.outcome }} + KERNEL_OUTCOME: ${{ steps.kernel.outcome }} + AUDIT_OUTCOME: ${{ steps.audit.outcome }} + run: | + set -euo pipefail + evidence_dir="$RUNNER_TEMP/source-smooth-realization-precheckout" + mkdir -p "$evidence_dir" + date -u +%Y-%m-%dT%H:%M:%SZ > "$evidence_dir/end-utc.txt" + printf 'precheckout=%s\ncheckout=%s\nsources=%s\nsetup=%s\npincheck=%s\npredecessor=%s\nproof=%s\ncontrols=%s\nkernel=%s\naudit=%s\nscientific_effect=NONE\n' "$PRECHECKOUT_OUTCOME" "$CHECKOUT_OUTCOME" "$SOURCE_OUTCOME" "$SETUP_OUTCOME" "$PINCHECK_OUTCOME" "$PREDECESSOR_OUTCOME" "$PROOF_OUTCOME" "$CONTROLS_OUTCOME" "$KERNEL_OUTCOME" "$AUDIT_OUTCOME" > "$evidence_dir/outcomes.txt" + - name: Capture every available final identity before evaluating failure + id: finalcapture + timeout-minutes: 1 + if: always() + working-directory: ${{ runner.temp }} + run: | + set -u -o pipefail + set +e + final_dir="$RUNNER_TEMP/source-smooth-realization-final" + package_dir="$GITHUB_WORKSPACE/frontiers/source_smooth_realization_20261011" + mkdir -p "$final_dir/literal-source-copies" || exit 90 + date -u +%Y-%m-%dT%H:%M:%SZ > "$final_dir/start-utc.txt" + final_start=$SECONDS + capture_failed=0 + capture() { + local label="$1" status start + shift + start=$SECONDS + date -u +%Y-%m-%dT%H:%M:%SZ > "$final_dir/$label-start.txt" + "$@" > "$final_dir/$label.stdout" 2> "$final_dir/$label.stderr" + status=$? + printf '%s\n' "$status" > "$final_dir/$label-exit.txt" + printf '%s\n' "$((SECONDS-start))" > "$final_dir/$label-seconds.txt" + date -u +%Y-%m-%dT%H:%M:%SZ > "$final_dir/$label-end.txt" + if test "$status" -ne 0; then capture_failed=1; fi + printf '%s\t%s\n' "$label" "$status" >> "$final_dir/capture-results.tsv" + return 0 + } + safe_package() { + if test ! -d "$package_dir" || test -L "$GITHUB_WORKSPACE/frontiers" || test -L "$package_dir"; then + printf 'UNAVAILABLE_OR_SYMLINK_PACKAGE %s\n' "$package_dir" >&2 + return 91 + fi + } + safe_file() { + if test ! -f "$1" || test -L "$1"; then + printf 'UNAVAILABLE_OR_SYMLINK_FILE %s\n' "$1" >&2 + return 92 + fi + } + relative_hash() { + safe_package || return $? + safe_file "$package_dir/$1" || return $? + (cd "$package_dir" && sha256sum -- "$1") + } + literal_hashes_and_copies() { + local file status=0 + safe_package || return $? + while IFS= read -r file; do + if safe_file "$package_dir/$file"; then + relative_hash "$file" || status=1 + cp -- "$package_dir/$file" "$final_dir/literal-source-copies/$file" || status=1 + else + printf 'UNAVAILABLE_OR_SYMLINK_LITERAL %s\n' "$file" + status=1 + fi + done < "$final_dir/package-members-required-literal.txt" + return "$status" + } + package_tracked_members() { + safe_package || return $? + git -C "$package_dir" ls-files -- . | LC_ALL=C sort + } + package_filesystem_members() { + safe_package || return $? + find "$package_dir" -path "$package_dir/.lake" -prune -o -type f -printf '%P\n' | LC_ALL=C sort + } + package_filesystem_entries() { + safe_package || return $? + find "$package_dir" -path "$package_dir/.lake" -prune -o -printf '%y %P\n' | LC_ALL=C sort + } + literal_contents() { + safe_package || return $? + safe_file "$package_dir/$1" || return $? + cat -- "$package_dir/$1" + } + workflow_identity() { + local workflow="$GITHUB_WORKSPACE/.github/workflows/source-smooth-realization.yml" + if test -L "$GITHUB_WORKSPACE/.github" || test -L "$GITHUB_WORKSPACE/.github/workflows"; then + printf 'UNAVAILABLE_SYMLINK_WORKFLOW_DIRECTORY\n' >&2 + return 93 + fi + safe_file "$workflow" || return $? + sha256sum -- "$workflow" || return $? + cp -- "$workflow" "$final_dir/workflow-actual.yml" + } + trusted_checksum_list() { + safe_package || return $? + safe_file "$package_dir/SOURCE_SHA256SUMS" || return $? + local actual + actual=$(sha256sum -- "$package_dir/SOURCE_SHA256SUMS") || return $? + actual=${actual%% *} + if test "$actual" != "$EXPECTED_SOURCE_LIST_SHA256"; then + printf 'UNTRUSTED_LIST_PATHS_NOT_FOLLOWED expected=%s actual=%s\n' "$EXPECTED_SOURCE_LIST_SHA256" "$actual" >&2 + return 94 + fi + } + expected_list_identity() { + trusted_checksum_list + } + expected_manifest_identity() { + safe_package || return $? + safe_file "$package_dir/SOURCE_MANIFEST.json" || return $? + local actual + actual=$(sha256sum -- "$package_dir/SOURCE_MANIFEST.json") || return $? + actual=${actual%% *} + if test "$actual" != "$EXPECTED_SOURCE_MANIFEST_SHA256"; then + printf 'MANIFEST_IDENTITY_MISMATCH expected=%s actual=%s\n' "$EXPECTED_SOURCE_MANIFEST_SHA256" "$actual" >&2 + return 95 + fi + } + expected_source_checks() { + trusted_checksum_list || return $? + local file + while IFS= read -r line; do + file=${line#* } + safe_file "$package_dir/$file" || return $? + done < "$package_dir/SOURCE_SHA256SUMS" + (cd "$package_dir" && sha256sum -c SOURCE_SHA256SUMS) + } + actual_hashes_in_trusted_list_order() { + trusted_checksum_list || return $? + local file status=0 + while IFS= read -r line; do + file=${line#* } + relative_hash "$file" || status=1 + done < "$package_dir/SOURCE_SHA256SUMS" + relative_hash SOURCE_SHA256SUMS || status=1 + return "$status" + } + compare_available() { + safe_file "$1" || return $? + safe_file "$2" || return $? + cmp -s -- "$1" "$2" + } + cat > "$final_dir/package-members-required-literal.txt" <<'LITERAL_SOURCE_FILES' + .gitignore + DESIGN.md + GaussianSeriesFoundation.lean + SOURCE_MANIFEST.json + SOURCE_SHA256SUMS + SourceC4.lean + SourceCovariance.lean + SourceFourierSeries.lean + SourceGaussianLaw.lean + SourceKernel.lean + SourceLattice.lean + SourceSmooth.lean + SourceSmoothAxiomAudit.lean + SourceSmoothCarrier.lean + SourceSmoothControls.lean + SourceTorus.lean + SourceTorusC4.lean + SpectralWeights.lean + lake-manifest.json + lakefile.toml + lean-toolchain + LITERAL_SOURCE_FILES + printf 'claim_uuid=%s\nstrict_source_guard=%s\nsource_package=%s\nexpected_list_sha256=%s\nexpected_manifest_sha256=%s\nhistorical_manifest_claim_uuid=%s\nhistorical_manifest_claim_is_current_admission=false\nexternal_head_tree_workflow_binding=ROOT_PREPUBLICATION_RECORD_REQUIRED\nfilesystem_scope=package_outside_generated_dot_lake\nscientific_effect=NONE\n' "$CLAIM_UUID" "$SOURCE_GUARD_UTC" "$package_dir" "$EXPECTED_SOURCE_LIST_SHA256" "$EXPECTED_SOURCE_MANIFEST_SHA256" "$HISTORICAL_MANIFEST_CLAIM_UUID" > "$final_dir/context.txt" + # Fixed literal paths are collected independently before trusting current list contents. + capture literal-source-whole-hashes literal_hashes_and_copies + capture source-list-identity relative_hash SOURCE_SHA256SUMS + capture source-manifest-identity relative_hash SOURCE_MANIFEST.json + capture source-list-current literal_contents SOURCE_SHA256SUMS + capture source-manifest-current literal_contents SOURCE_MANIFEST.json + capture package-members-tracked package_tracked_members + capture package-members-filesystem package_filesystem_members + capture package-filesystem-all-entry-types package_filesystem_entries + capture repository-members-tracked git -C "$GITHUB_WORKSPACE" ls-files + capture repository-tracked-tree git -C "$GITHUB_WORKSPACE" ls-tree -r HEAD + capture workflow-identity workflow_identity + capture checkout-sha git -C "$GITHUB_WORKSPACE" rev-parse HEAD + capture checkout-tree git -C "$GITHUB_WORKSPACE" rev-parse 'HEAD^{tree}' + capture checkout-parents git -C "$GITHUB_WORKSPACE" show -s --format=%P HEAD + capture selected-head-tree git -C "$GITHUB_WORKSPACE" rev-parse 'HEAD^2^{tree}' + capture selected-head-source-diff git -C "$GITHUB_WORKSPACE" diff --raw "$EXPECTED_BASE_SHA" HEAD^2 + capture tracked-tree-diff git -C "$GITHUB_WORKSPACE" diff --exit-code + capture tracked-tree-index-diff git -C "$GITHUB_WORKSPACE" diff --cached --exit-code + capture repository-status git -C "$GITHUB_WORKSPACE" status --porcelain --untracked-files=all + # Identity mismatch refuses list traversal; expected checks still receive durable actual exits. + capture expected-list-identity expected_list_identity + capture expected-manifest-identity expected_manifest_identity + capture expected-source-checks expected_source_checks + capture actual-final-hashes-in-list-order actual_hashes_in_trusted_list_order + # Historical before-files may be absent. Missing labels/exit92 are retained after complete collection. + capture compare-checksum-list-before compare_available "$package_dir/.lake/evidence/checksum-list-identity-before.txt" "$final_dir/source-list-identity.stdout" + capture compare-source-hashes-before compare_available "$package_dir/.lake/evidence/sources-actual-before.sha256" "$final_dir/actual-final-hashes-in-list-order.stdout" + capture compare-literal-tracked-members compare_available "$final_dir/package-members-required-literal.txt" "$final_dir/package-members-tracked.stdout" + capture compare-literal-filesystem-members compare_available "$final_dir/package-members-required-literal.txt" "$final_dir/package-members-filesystem.stdout" + printf '%s\n' "$capture_failed" > "$final_dir/final-capture-exit.txt" + printf '%s\n' "$((SECONDS-final_start))" > "$final_dir/final-capture-seconds.txt" + date -u +%Y-%m-%dT%H:%M:%SZ > "$final_dir/end-utc.txt" + cat "$final_dir/capture-results.tsv" + exit "$capture_failed" + - name: Preserve complete phase logs on success or failure + timeout-minutes: 1 + if: always() + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a + with: + name: source-smooth-realization-${{ github.run_id }}-${{ github.run_attempt }} + path: | + frontiers/source_smooth_realization_20261011/.lake/evidence/ + ${{ runner.temp }}/source-smooth-realization-precheckout/ + ${{ runner.temp }}/source-smooth-realization-final/ + include-hidden-files: true + if-no-files-found: error + retention-days: 90 diff --git a/frontiers/source_smooth_realization_20261011/.gitignore b/frontiers/source_smooth_realization_20261011/.gitignore new file mode 100644 index 000000000..01f8cdb63 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/frontiers/source_smooth_realization_20261011/DESIGN.md b/frontiers/source_smooth_realization_20261011/DESIGN.md new file mode 100644 index 000000000..b07ad4998 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/DESIGN.md @@ -0,0 +1,54 @@ +The first C261 Stage A construction supplies a smooth probability-one carrier for +the existing infinite Gaussian Fourier field. It preserves the exact product +coefficient law under inclusion and hence the existing finite Gaussian field +laws and spectral covariance. The represented samples must satisfy every finite +smoothness order, on one explicit measurable event. The source remains the full +Fourier sum with the same normalized weights and period, at every point. + +The new module SourceSmooth derives order-indexed summable majorants from the +existing summable_decay_pow theorem, bounds every iterated derivative of each +mode, and proves smoothness on the countable intersection of weighted absolute +summability events. SourceSmoothCarrier proves that event is measurable, gives +its actual full-measure subtype and comap probability measure, and transports +the existing source laws through the literal inclusion. SourceSmoothControls +will distinguish this result from the old order-four theorem and verify law and +sample identities, including higher orders and finite-coordinate changes. + +Dependencies are literal source copies from F7 head +1a7fc4be83043f2e313927019db85fff61eeac3f, tree +3b3c0f16f848712a9eb53bb1b412a06bab787b91. SourceFreeze SHA-256 is +3b7d85ab24e872b1afe4c52e7cd69d596a247141449519e2074d4a95af3c7e28. +That baseline is a qualified draft stack, not Math- main. The observed current +Math- main is 298b26319cff27cc22db5ca8ec545c70ba6cc92e. PR419's statement +source is 873c6c01b768acf66c8968e5fb8b734e2d8d61d0. The incidental R17 WE1890 +notes phrase "native Main1a?" is a placeholder with no identity effect; these +exact identities control it. Historical claim bytes are preserved. + +ROOT holds source claim e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6, +2026-10-11T20:58:16.222Z through 2026-10-11T22:58:16.223Z. Its actual native +discussion is Math- PR419 comment6113682633; its R17 Work Events1890 claim was +read back in all14 literal/effective/format fields before material source edits. +These cooperative claims do not exclude unregistered writers. ROOT authors +SourceSmooth; f3 authors SourceSmoothCarrier; f5 independently reviews the exact +new sources. All are OpenAI/Codex, source-exposed and not organizationally +independent. No human mathematical review is inferred. + +Only this subconstruction is allocated. No Field or Lifetime nominal type, +Claude-owned adapter, C262–C264 source/gate, or existing workflow is changed. +Euclidean coordinate transport, theta/Poisson covariance identification, +first-jet rank, the canonical fixed-pin conditional kernel, fixed-fiber +genericity, full weighted global elder probability and count/density remain +separate C261 Stage A/B/C obligations. Neither a generic ratio identity nor an +assumed realization record can close them. + +Every new proof is UNCOMPILED until a fresh, exact-source hosted qualification +with meaningful controls and kernel/axiom audit. Local project execution, +Lean/Lake/Python imports/tests and old run retries remain excluded by the current +HOSTED_ONLY boundary. No native ref, runtime slot, workflow or run has been +created by this source preparation. A prospective initial hosted plan needs +separate complete source/resource/trigger review before source publication. + +This advances an essential actual-field prerequisite. It does not close the +universality exponent, marked point-process convergence, global uniqueness, +higher homology, coefficient, blind50 numerical validation, publications, or +scientific/community uptake. Scientific effect NONE; full goal ACTIVE_UNMET. diff --git a/frontiers/source_smooth_realization_20261011/GaussianSeriesFoundation.lean b/frontiers/source_smooth_realization_20261011/GaussianSeriesFoundation.lean new file mode 100644 index 000000000..93651da7f --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/GaussianSeriesFoundation.lean @@ -0,0 +1,96 @@ +import Mathlib.Probability.Distributions.Gaussian.Real +import Mathlib.Probability.Independence.InfinitePi +import Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum +import Mathlib.MeasureTheory.Function.LpSeminorm.SMul + +/-! The actual product law and the almost-sure absolute-series foundation. +This does not assert a Fourier covariance, sample smoothness or finite-jet rank. -/ + +noncomputable section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace I4Foundation + +/-- The same actual probability measure used for every coefficient and series assertion. -/ +def coefficientLaw (ι : Type*) : Measure (ι → ℝ) := + Measure.infinitePi (fun _ : ι => gaussianReal 0 1) + +instance coefficientLaw_isProbabilityMeasure (ι : Type*) : + IsProbabilityMeasure (coefficientLaw ι) := by + unfold coefficientLaw + infer_instance + +theorem coordinate_measurePreserving {ι : Type*} (i : ι) : + MeasurePreserving (fun ω : ι → ℝ => ω i) (coefficientLaw ι) + (gaussianReal 0 1) := by + exact measurePreserving_eval_infinitePi (fun _ : ι => gaussianReal 0 1) i + +theorem coordinate_marginal {ι : Type*} (i : ι) : + (coefficientLaw ι).map (fun ω => ω i) = gaussianReal 0 1 := by + exact (coordinate_measurePreserving i).map_eq + +theorem coordinates_independent (ι : Type*) : + iIndepFun (fun i (ω : ι → ℝ) => ω i) (coefficientLaw ι) := by + exact iIndepFun_infinitePi (P := fun _ : ι => gaussianReal 0 1) + (X := fun _ : ι => id) (fun _ => measurable_id) + +theorem coordinate_memLp {ι : Type*} (i : ι) (p : ℝ≥0∞) (hp : p ≠ ∞) : + MemLp (fun ω : ι → ℝ => ω i) p (coefficientLaw ι) := by + exact (memLp_id_gaussianReal' p hp).comp_measurePreserving + (coordinate_measurePreserving i) + +theorem coordinate_integrable {ι : Type*} (i : ι) : + Integrable (fun ω : ι → ℝ => ω i) (coefficientLaw ι) := by + exact memLp_one_iff_integrable.mp (coordinate_memLp i 1 (by simp)) + +theorem coordinate_abs_integrable {ι : Type*} (i : ι) : + Integrable (fun ω : ι → ℝ => |ω i|) (coefficientLaw ι) := by + simpa only [Real.norm_eq_abs] using (coordinate_integrable i).norm + +theorem weighted_abs_summable_ae {ι : Type*} [Countable ι] + (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hs : Summable a) : + ∀ᵐ ω ∂coefficientLaw ι, Summable (fun i => a i * |ω i|) := by + let C := eLpNorm id 1 (gaussianReal 0 1) + have hC : C < ∞ := (memLp_id_gaussianReal' 1 (by simp)).eLpNorm_lt_top + have hcoord (i : ι) : + eLpNorm (fun ω : ι → ℝ => ω i) 1 (coefficientLaw ι) = C := by + exact eLpNorm_comp_measurePreserving + (memLp_id_gaussianReal' 1 (by simp)).aestronglyMeasurable + (coordinate_measurePreserving i) + have hnorm (i : ι) : + eLpNorm (fun ω : ι → ℝ => a i * ω i) 1 (coefficientLaw ι) = + ENNReal.ofReal (a i) * C := by + change eLpNorm (a i • (fun ω : ι → ℝ => ω i)) 1 (coefficientLaw ι) = _ + rw [eLpNorm_const_smul, Real.enorm_eq_ofReal (ha i), hcoord] + have hsum : (∑' i, eLpNorm (fun ω : ι → ℝ => a i * ω i) 1 + (coefficientLaw ι)) ≠ ∞ := by + simp_rw [hnorm] + rw [ENNReal.tsum_mul_right] + exact ENNReal.mul_ne_top hs.tsum_ofReal_ne_top hC.ne + have h := summable_norm_of_tsum_eLpNorm_ne_top (p := 1) (le_refl 1) hsum + filter_upwards [h] with ω hω + simpa only [Real.norm_eq_abs, abs_mul, abs_of_nonneg (ha _)] using hω + +/-- The actual scalar sum; its convergence is proved separately on the product law. -/ +def scalarSeries {ι : Type*} (a : ι → ℝ) (ω : ι → ℝ) : ℝ := + ∑' i, a i * ω i + +theorem scalarSeries_measurable {ι : Type*} [Countable ι] (a : ι → ℝ) : + Measurable (scalarSeries a) := by + unfold scalarSeries + apply Measurable.tsum + intro i + exact measurable_const.mul (measurable_pi_apply i) + +theorem scalarSeries_hasSum_ae {ι : Type*} [Countable ι] + (a : ι → ℝ) (hs : Summable a) : + ∀ᵐ ω ∂coefficientLaw ι, HasSum (fun i => a i * ω i) (scalarSeries a ω) := by + filter_upwards [weighted_abs_summable_ae (fun i => |a i|) + (fun i => abs_nonneg _) hs.abs] with ω hω + have hnorm : Summable (fun i => ‖a i * ω i‖) := by + simpa only [Real.norm_eq_abs, abs_mul] using hω + exact hnorm.of_norm.hasSum + +end I4Foundation diff --git a/frontiers/source_smooth_realization_20261011/SOURCE_MANIFEST.json b/frontiers/source_smooth_realization_20261011/SOURCE_MANIFEST.json new file mode 100644 index 000000000..1da007cd7 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SOURCE_MANIFEST.json @@ -0,0 +1,294 @@ +{ + "schema_version": 1, + "package": "frontiers/source_smooth_realization_20261011", + "prepared_at_utc": "2026-10-11T21:08:01.480Z", + "status": "MATHEMATICAL_SOURCE_REVIEW_PASS_UNCOMPILED", + "source_claim": { + "uuid": "e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6", + "native": "https://github.com/d6g8k5htny-coder/Math-/pull/419#issuecomment-6113682633", + "r17_work_events_row": 1890, + "lease_until": "2026-10-11T22:58:16.223Z" + }, + "parent": { + "commit": "1a7fc4be83043f2e313927019db85fff61eeac3f", + "tree": "3b3c0f16f848712a9eb53bb1b412a06bab787b91", + "source_freeze_sha256": "3b7d85ab24e872b1afe4c52e7cd69d596a247141449519e2074d4a95af3c7e28", + "qualified_draft_not_main": true + }, + "toolchain": "leanprover/lean4:v4.34.1", + "dependencies": [ + { + "name": "plausible", + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "LeanSearchClient", + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "importGraph", + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e928b72544873815af278d38681b31c0293588e3", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "proofwidgets", + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "name": "aesop", + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Qq", + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "batteries", + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Cli", + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "mathlib", + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "manifestFile": "lake-manifest.json", + "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "inherited": false, + "configFile": "lakefile.lean" + } + ], + "files": [ + { + "path": ".gitignore", + "bytes": 7, + "sha256": "fde850d24186b6e99c8c0debd641fb3ab85198b109eb66f71a1fea02bd6ea1b3", + "git_blob_sha1": "01f8cdb637da2370fa79960e25efa59dd8cffd6d", + "role": "SOURCE_DESCRIPTOR" + }, + { + "path": "DESIGN.md", + "bytes": 3557, + "sha256": "18f486b9a1e94d449ab078fccdb5bfaec7bad0075c3a8e8d26f96775b68e10f7", + "git_blob_sha1": "b07ad499826e8e9dc9ce11bf3fd683539ab247c5", + "role": "SOURCE_DESCRIPTOR" + }, + { + "path": "GaussianSeriesFoundation.lean", + "bytes": 4262, + "sha256": "feea566d5aeba58459bd4a1f20f070bdcd80ee30712817324cdd594e3e232c95", + "git_blob_sha1": "93651da7fcfbc834661c795f0ec8b08383d86887", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceC4.lean", + "bytes": 6438, + "sha256": "b15e53b825c2e2d6af2af18182da227d8794dddcc3e1b29611a913f89a889397", + "git_blob_sha1": "f5188d51c29b8c639019bab2e6bf51e0cff5bc15", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceCovariance.lean", + "bytes": 3925, + "sha256": "30560009582659a100637b5510c657cf1fa762f68a37bae8fab42c1eeee6aee5", + "git_blob_sha1": "50aa85f304c7e6b93a9cd84d555ba9c32112f9fd", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceFourierSeries.lean", + "bytes": 6524, + "sha256": "5f145e8e8693bfe4d1554092c8258dbda4f17f8e078c503029e4e8ff2c018014", + "git_blob_sha1": "e4cdec9e62faf6b20312294d4eccb14f16aa948c", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceGaussianLaw.lean", + "bytes": 8984, + "sha256": "a60ab6099d3cef0eeecaefa9e35d95ec14ec54ffd6c89e42dfcf6170907166e8", + "git_blob_sha1": "bb8450b5a8029614f4456bb527f2a7bbde16e852", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceKernel.lean", + "bytes": 5293, + "sha256": "5fa3abc8fb0db0c14c67b4ee840e659cdf80f7d22c9fd4cb5e6c1c7b204fbd21", + "git_blob_sha1": "5d5602ac787f1580214afc49e5d4da6f5e158ac2", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceLattice.lean", + "bytes": 6284, + "sha256": "c644305a426bc876f609c055ce999b8008f028c67a1091639d919f4122981b7b", + "git_blob_sha1": "9c1e0557c352066535be4e67fba698adf7a91e04", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceSmooth.lean", + "bytes": 11231, + "sha256": "2108f00c98e9b91fae34e9e1abefdd1cb42d250c864c0fd076bfb238977e9028", + "git_blob_sha1": "dee9dd9a5906cac042f7359772fa122327354194", + "role": "NEW_UNCOMPILED_MATHEMATICAL_SOURCE" + }, + { + "path": "SourceSmoothAxiomAudit.lean", + "bytes": 3399, + "sha256": "4dfa901029fab71d127c9f4c8cf30c937607f4444e6af64f429890d9d141d591", + "git_blob_sha1": "e22ec44e59ca5a14de9107349d5061e6a81de616", + "role": "PROSPECTIVE_FULL_MODULE_AXIOM_AUDIT" + }, + { + "path": "SourceSmoothCarrier.lean", + "bytes": 11195, + "sha256": "519cb2e4e07dddb5ae939a187c7e5b127bdc49efb9a62b1a9b0ea84bf46a9106", + "git_blob_sha1": "733328a3ec1b9df9e84271649762ab5583c6c496", + "role": "NEW_UNCOMPILED_MATHEMATICAL_SOURCE" + }, + { + "path": "SourceSmoothControls.lean", + "bytes": 3257, + "sha256": "8eca5ecdb5e2a0c1cb786468b340e4516df653468f958e535f156baafef088b4", + "git_blob_sha1": "febe52a42d099844d02c59b728ca86417587b3e2", + "role": "NEW_UNCOMPILED_MATHEMATICAL_SOURCE" + }, + { + "path": "SourceTorus.lean", + "bytes": 5182, + "sha256": "02857b44552ab0e51a756b3b095c4ba43f8168ac332b069acb5bc8146d337eef", + "git_blob_sha1": "b9fe497521f930a19c1ab355d776af6d32c85775", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SourceTorusC4.lean", + "bytes": 6081, + "sha256": "b67b13030389dea4521e8e2afcac30ea44f84abd65c374bf208067b288fc64a1", + "git_blob_sha1": "30cfb670f953aab16b4fe1fa6a26476f10443afc", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "SpectralWeights.lean", + "bytes": 6924, + "sha256": "92af14a2d83304de3f8576ee10b3d376587e93c4464f8c715b8d2e32360f44b0", + "git_blob_sha1": "191a22f14382fb05a520717b7de544019c8566d5", + "role": "LITERAL_F7_DEPENDENCY" + }, + { + "path": "lake-manifest.json", + "bytes": 3558, + "sha256": "4cc60e1f98fc3a46bccafe6b8315445d950ca1db55ceba26fdebe3a45eafe59a", + "git_blob_sha1": "9fe1332352893f5f89e74b550a25ee187b871ed3", + "role": "SOURCE_DESCRIPTOR" + }, + { + "path": "lakefile.toml", + "bytes": 746, + "sha256": "7782dd2fef85bf956a0ccc76e4e6420b8818eabb3bc133cade7252ea7d1d92e6", + "git_blob_sha1": "695cbbf56eaed49dd113b9ecdb76e4fcd4e1d0c6", + "role": "SOURCE_DESCRIPTOR" + }, + { + "path": "lean-toolchain", + "bytes": 25, + "sha256": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b", + "git_blob_sha1": "ba8ebf2dbaf6a668cd2a0e086186d6d569b69ff5", + "role": "SOURCE_DESCRIPTOR" + } + ], + "review": { + "reviewer": "/root/f5_controls_source_review", + "source_exposed": true, + "same_provider": true, + "organization_independence": 0, + "verdict": "PASS_EXACT_UNCOMPILED_MATHEMATICAL_SPECIFICATION", + "md_sha256": "f9ab19fcee66717b2149a6ca850e788fd34deaea6eb1ff2466c999ff5888196a", + "json_sha256": "2f1c070bc09cf169ea1f68fd01a1f2732ae9cfa7cce891b958cd133c10c5ef18" + }, + "scope": "Actual all-order smooth carrier for the identical infinite Gaussian Fourier source and literal inclusion-law preservation; first C261 StageA prerequisite only.", + "compilation": "NOT_RUN", + "kernel": "NOT_RUN", + "actual_axiom_census": "NOT_RUN", + "hosted_slot": "UNALLOCATED", + "new_native_branch_commit_pr": null, + "scientific_effect": "NONE", + "full_goal": "ACTIVE_UNMET", + "open_obligations": [ + "Euclidean nominal coordinate transport", + "theta/Poisson covariance identity", + "C2-valued random element", + "derivative observation Gaussian/rank laws", + "canonical every-target full-field regression kernel", + "Field/Lifetime adapter (Claude-owned)", + "fixed-fiber genericity", + "weighted global elder law", + "count/density", + "global uniqueness/Hk/marked convergence", + "universality/local-jet coefficient/numerical50/publications/uptake" + ] +} diff --git a/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS b/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS new file mode 100644 index 000000000..6562c5f05 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS @@ -0,0 +1,20 @@ +fde850d24186b6e99c8c0debd641fb3ab85198b109eb66f71a1fea02bd6ea1b3 .gitignore +18f486b9a1e94d449ab078fccdb5bfaec7bad0075c3a8e8d26f96775b68e10f7 DESIGN.md +feea566d5aeba58459bd4a1f20f070bdcd80ee30712817324cdd594e3e232c95 GaussianSeriesFoundation.lean +4cc60e1f98fc3a46bccafe6b8315445d950ca1db55ceba26fdebe3a45eafe59a lake-manifest.json +7782dd2fef85bf956a0ccc76e4e6420b8818eabb3bc133cade7252ea7d1d92e6 lakefile.toml +d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b lean-toolchain +56acfdbf20fd7645872f2ce3a60beb1186908dc4f7994d14b175ddc93106b65d SOURCE_MANIFEST.json +b15e53b825c2e2d6af2af18182da227d8794dddcc3e1b29611a913f89a889397 SourceC4.lean +30560009582659a100637b5510c657cf1fa762f68a37bae8fab42c1eeee6aee5 SourceCovariance.lean +5f145e8e8693bfe4d1554092c8258dbda4f17f8e078c503029e4e8ff2c018014 SourceFourierSeries.lean +a60ab6099d3cef0eeecaefa9e35d95ec14ec54ffd6c89e42dfcf6170907166e8 SourceGaussianLaw.lean +5fa3abc8fb0db0c14c67b4ee840e659cdf80f7d22c9fd4cb5e6c1c7b204fbd21 SourceKernel.lean +c644305a426bc876f609c055ce999b8008f028c67a1091639d919f4122981b7b SourceLattice.lean +2108f00c98e9b91fae34e9e1abefdd1cb42d250c864c0fd076bfb238977e9028 SourceSmooth.lean +4dfa901029fab71d127c9f4c8cf30c937607f4444e6af64f429890d9d141d591 SourceSmoothAxiomAudit.lean +519cb2e4e07dddb5ae939a187c7e5b127bdc49efb9a62b1a9b0ea84bf46a9106 SourceSmoothCarrier.lean +8eca5ecdb5e2a0c1cb786468b340e4516df653468f958e535f156baafef088b4 SourceSmoothControls.lean +02857b44552ab0e51a756b3b095c4ba43f8168ac332b069acb5bc8146d337eef SourceTorus.lean +b67b13030389dea4521e8e2afcac30ea44f84abd65c374bf208067b288fc64a1 SourceTorusC4.lean +92af14a2d83304de3f8576ee10b3d376587e93c4464f8c715b8d2e32360f44b0 SpectralWeights.lean diff --git a/frontiers/source_smooth_realization_20261011/SourceC4.lean b/frontiers/source_smooth_realization_20261011/SourceC4.lean new file mode 100644 index 000000000..f5188d51c --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceC4.lean @@ -0,0 +1,141 @@ +import SourceFourierSeries +import Mathlib.Analysis.Calculus.SmoothSeries +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv + +/-! Actual same-sample C4 of the canonical normalized Fourier lift. +Covariance identification, Gaussian field/jet laws and pin regression are separate. -/ + +noncomputable section +open I4Foundation I4Weights I4Source MeasureTheory ProbabilityTheory +open scoped BigOperators + +namespace I4C4 + +def phaseCLM (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : (Fin d → ℝ) →L[ℝ] ℝ := + ∑ i, (sourceC L * (k i : ℝ)) • ContinuousLinearMap.proj i + +theorem phaseCLM_apply (d : ℕ) (L : ℝ) (k : Fin d → ℤ) (x : Fin d → ℝ) : + phaseCLM d L k x = phase d L k x := by + simp [phaseCLM, phase] + +theorem phaseCLM_norm_le (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : + ‖phaseCLM d L k‖ ≤ ∑ i, |sourceC L * (k i : ℝ)| := by + apply ContinuousLinearMap.opNorm_le_bound _ + (Finset.sum_nonneg (fun i _ => abs_nonneg _)) + intro x + rw [phaseCLM_apply] + calc + ‖phase d L k x‖ ≤ ∑ i, ‖sourceC L * (k i : ℝ) * x i‖ := norm_sum_le _ _ + _ ≤ ∑ i, |sourceC L * (k i : ℝ)| * ‖x‖ := by + apply Finset.sum_le_sum + intro i _ + rw [norm_mul, Real.norm_eq_abs] + exact mul_le_mul_of_nonneg_left (norm_le_pi_norm x i) (abs_nonneg _) + _ = (∑ i, |sourceC L * (k i : ℝ)|) * ‖x‖ := by rw [Finset.sum_mul] + +theorem modeCoefficient_iteratedFDeriv_bound (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (m : SourceMode d) (j : ℕ) (hj : j ≤ 4) (x : Fin d → ℝ) : + ‖iteratedFDeriv ℝ j (modeCoefficient d L m) x‖ ≤ modeMajorant d L m := by + classical + cases m with + | none => + cases j with + | zero => + simpa only [norm_iteratedFDeriv_zero, Real.norm_eq_abs] using + modeCoefficient_bound d hL none x + | succ j => + change ‖iteratedFDeriv ℝ (j + 1) + (fun _ : Fin d → ℝ => Real.sqrt (1 / sourceZ d L)) x‖ ≤ Real.sqrt (1 / sourceZ d L) + rw [iteratedFDeriv_succ_const] + simp only [Pi.zero_apply, norm_zero] + exact Real.sqrt_nonneg _ + | some p => + rcases p with ⟨k, b⟩ + let A := Real.sqrt (2 * sourceWeight d L k / sourceZ d L) + let P := ∏ i, (1 + |sourceC L * (k.1 i : ℝ)|) + let g : ℝ → ℝ := if b then Real.sin else Real.cos + let ell := phaseCLM d L k + have hg : ContDiff ℝ j g := by + cases b <;> simp only [g, Bool.false_eq_true, ite_false, ite_true] <;> fun_prop + have hgc : ContDiff ℝ j (g ∘ ell) := hg.comp_continuousLinearMap + have hgn : ‖iteratedFDeriv ℝ j g (ell x)‖ ≤ 1 := by + cases b with + | false => + simpa only [g, Bool.false_eq_true, ite_false, + norm_iteratedFDeriv_eq_norm_iteratedDeriv, Real.norm_eq_abs] using + Real.abs_iteratedDeriv_cos_le_one j (ell x) + | true => + simpa only [g, ite_true, norm_iteratedFDeriv_eq_norm_iteratedDeriv, + Real.norm_eq_abs] using Real.abs_iteratedDeriv_sin_le_one j (ell x) + have hP : 1 ≤ P := by + apply Finset.one_le_prod₀ + intro i _ + linarith [abs_nonneg (sourceC L * (k.1 i : ℝ))] + have hl : ‖ell‖ ≤ P := by + calc + ‖ell‖ ≤ ∑ i, |sourceC L * (k.1 i : ℝ)| := phaseCLM_norm_le d L k + _ ≤ 1 + ∑ i, |sourceC L * (k.1 i : ℝ)| := by linarith + _ ≤ P := frequency_l1_le_product d _ (fun i => abs_nonneg _) + have hpow : ‖ell‖ ^ j ≤ P ^ 4 := by + calc + ‖ell‖ ^ j ≤ P ^ j := by gcongr + _ ≤ P ^ 4 := pow_le_pow_right₀ hP hj + have hder : ‖iteratedFDeriv ℝ j (g ∘ ell) x‖ ≤ ‖ell‖ ^ j := by + rw [ell.iteratedFDeriv_comp_right hg x le_rfl] + calc + _ ≤ ‖iteratedFDeriv ℝ j g (ell x)‖ * ∏ _i : Fin j, ‖ell‖ := + (iteratedFDeriv ℝ j g (ell x)).norm_compContinuousLinearMap_le (fun _ => ell) + _ ≤ 1 * ∏ _i : Fin j, ‖ell‖ := + mul_le_mul_of_nonneg_right hgn (Finset.prod_nonneg (fun _ _ => norm_nonneg _)) + _ = ‖ell‖ ^ j := by simp + have heq : modeCoefficient d L (some (k, b)) = A • (g ∘ ell) := by + funext y + cases b <;> simp [modeCoefficient, A, g, Function.comp_apply, Pi.smul_apply, + smul_eq_mul, ell, phaseCLM_apply] + rw [heq, iteratedFDeriv_const_smul_apply hgc.contDiffAt, norm_smul, + Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] + calc + _ ≤ A * P ^ 4 := mul_le_mul_of_nonneg_left (hder.trans hpow) (Real.sqrt_nonneg _) + _ = modeMajorant d L (some (k, b)) := by + rw [modeMajorant, pairedBound_eq_amplitude d hL k] + simp only [A, P, Finset.prod_pow] + +theorem sourceField_contDiff_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, ContDiff ℝ 4 (sourceField d L ω) := by + have hc (m : SourceMode d) : ContDiff ℝ 4 (modeCoefficient d L m) := by + cases m with + | none => + change ContDiff ℝ 4 (fun _ : Fin d → ℝ => Real.sqrt (1 / sourceZ d L)) + fun_prop + | some p => + rcases p with ⟨k, b⟩ + change ContDiff ℝ 4 (fun x : Fin d → ℝ => + Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + (if b then Real.sin (phase d L k x) else Real.cos (phase d L k x))) + cases b <;> simp [phase] <;> fun_prop + filter_upwards [sourceMajorant_ae d hL] with ω hω + change ContDiff ℝ 4 (fun x => ∑' m, modeCoefficient d L m x * ω m) + apply contDiff_tsum (v := fun _ m => modeMajorant d L m * |ω m|) + · intro m + exact (hc m).mul contDiff_const + · intro j hj + exact hω + · intro j m x hj + have hj' : j ≤ 4 := by exact_mod_cast hj + have hcj : ContDiff ℝ j (modeCoefficient d L m) := + (hc m).of_le (by exact_mod_cast hj') + have heq : (fun y => modeCoefficient d L m y * ω m) = ω m • modeCoefficient d L m := by + funext y + simp [smul_eq_mul, mul_comm] + rw [heq, iteratedFDeriv_const_smul_apply hcj.contDiffAt, norm_smul, Real.norm_eq_abs] + simpa only [mul_comm] using mul_le_mul_of_nonneg_left + (modeCoefficient_iteratedFDeriv_bound d hL m j hj' x) (abs_nonneg (ω m)) + +theorem sourceField_contDiff_affine_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, ∀ (T : (Fin d → ℝ) →L[ℝ] (Fin d → ℝ)) (a : Fin d → ℝ), + ContDiff ℝ 4 (fun x => sourceField d L ω (a + T x)) := by + filter_upwards [sourceField_contDiff_ae d hL] with ω hω + intro T a + exact hω.comp (contDiff_const.add T.contDiff) + +end I4C4 diff --git a/frontiers/source_smooth_realization_20261011/SourceCovariance.lean b/frontiers/source_smooth_realization_20261011/SourceCovariance.lean new file mode 100644 index 000000000..50aa85f30 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceCovariance.lean @@ -0,0 +1,74 @@ +import SourceKernel +import SourceGaussianLaw +import Mathlib.Probability.Moments.Covariance +import Mathlib.Probability.Moments.Variance + +noncomputable section +open I4Foundation I4Weights I4Source I4Kernel I4SourceGaussian MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal NNReal +namespace I4SourceCovariance + +variable {ι : Type*} [Countable ι] + +theorem scalarSeries_covariance (a b : ι → ℝ) (ha : Summable a) (hb : Summable b) : + cov[scalarSeries a, scalarSeries b; coefficientLaw ι] = ∑' i, a i * b i := by + have hsq (f : ι → ℝ) (hf : Summable f) : Summable (fun i => f i ^ 2) := by + have hp := summable_mul_of_summable_norm hf.norm hf.norm + simpa only [Function.comp_def, pow_two] using hp.comp_injective + (show Function.Injective (fun i : ι => (i,i)) from + fun i j h => congrArg Prod.fst h) + have hprod : Summable (fun i => a i * b i) := by + have hp := summable_mul_of_summable_norm ha.norm hb.norm + simpa only [Function.comp_def] using hp.comp_injective + (show Function.Injective (fun i : ι => (i,i)) from + fun i j h => congrArg Prod.fst h) + have hLp (f : ι → ℝ) (hf : Summable f) : + MemLp (scalarSeries f) 2 (coefficientLaw ι) := by + have h : MemLp id 2 ((coefficientLaw ι).map (scalarSeries f)) := by + rw [scalarSeries_map_gaussian f hf] + exact memLp_id_gaussianReal' 2 (by norm_num) + simpa only [Function.comp_def, Function.id_def] using + h.comp_of_map (scalarSeries_measurable f).aemeasurable + have heq : scalarSeries (a + b) =ᵐ[coefficientLaw ι] + (fun ω => scalarSeries a ω + scalarSeries b ω) := by + filter_upwards [scalarSeries_hasSum_ae a ha, scalarSeries_hasSum_ae b hb, + scalarSeries_hasSum_ae (a+b) (ha.add hb)] with ω haω hbω habω + exact habω.unique (by simpa only [Pi.add_apply, add_mul] using haω.add hbω) + have hts : (∑' i, (a i + b i)^2) = + (∑' i, a i ^ 2) + 2 * (∑' i, a i * b i) + (∑' i, b i ^ 2) := by + calc + _ = ∑' i, (a i ^ 2 + 2 * (a i * b i) + b i ^ 2) := by + exact tsum_congr (fun i => by ring) + _ = _ := by + rw [((hsq a ha).add (hprod.mul_left 2)).tsum_add (hsq b hb), + (hsq a ha).tsum_add (hprod.mul_left 2), tsum_mul_left] + have hv := variance_fun_add (hLp a ha) (hLp b hb) + rw [← variance_congr heq, scalarSeries_variance (a+b) (ha.add hb), + scalarSeries_variance a ha, scalarSeries_variance b hb] at hv + change (∑' i, (a i+b i)^2) = _ at hv + rw [hts] at hv + linarith + +theorem sourceField_integral_zero (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x : Fin d → ℝ) : + ∫ ω, sourceField d L ω x ∂sourceLaw d = 0 := by + have hc : Summable (fun m => modeCoefficient d L m x) := + (modeMajorant_summable d hL).of_norm_bounded (fun m => by + simpa only [Real.norm_eq_abs] using modeCoefficient_bound d hL m x) + exact scalarSeries_integral_zero (fun m => modeCoefficient d L m x) hc + +theorem sourceField_covariance (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x y : Fin d → ℝ) : + cov[fun ω => sourceField d L ω x, fun ω => sourceField d L ω y; sourceLaw d] = + sourceSpectralKernel d L (x - y) := by + have hc (z : Fin d → ℝ) : Summable (fun m => modeCoefficient d L m z) := + (modeMajorant_summable d hL).of_norm_bounded (fun m => by + simpa only [Real.norm_eq_abs] using modeCoefficient_bound d hL m z) + change cov[scalarSeries (fun m => modeCoefficient d L m x), + scalarSeries (fun m => modeCoefficient d L m y); coefficientLaw (SourceMode d)] = _ + rw [scalarSeries_covariance _ _ (hc x) (hc y), coefficientKernel_eq_fullLattice d hL x y] + +theorem sourceField_variance_one (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x : Fin d → ℝ) : + Var[fun ω => sourceField d L ω x; sourceLaw d] = 1 := by + rw [← covariance_self (sourceField_eval_measurable d L x).aemeasurable, + sourceField_covariance d hL x x, sub_self, spectralKernel_zero d hL] + +end I4SourceCovariance diff --git a/frontiers/source_smooth_realization_20261011/SourceFourierSeries.lean b/frontiers/source_smooth_realization_20261011/SourceFourierSeries.lean new file mode 100644 index 000000000..e4cdec9e6 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceFourierSeries.lean @@ -0,0 +1,147 @@ +import GaussianSeriesFoundation +import SpectralWeights +import Mathlib.Logic.Equiv.Option +import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn + +/-! Actual canonical real Fourier series and a shared-event uniform convergence bridge. +The half-lattice partition, covariance, sample C4 and finite-jet law require separate proofs. -/ + +noncomputable section +open MeasureTheory ProbabilityTheory I4Foundation I4Weights +open scoped BigOperators ENNReal + +namespace I4Source + +/-- The representative whose first nonzero coordinate is positive. -/ +def halfLattice (d : ℕ) : Set (Fin d → ℤ) := + {k | ∃ i, 0 < k i ∧ ∀ j, j < i → k j = 0} + +abbrev SourceMode (d : ℕ) := Option (↥(halfLattice d) × Bool) + +/-- The actual common law, with independent variance-one real coefficients. -/ +abbrev sourceLaw (d : ℕ) : Measure (SourceMode d → ℝ) := + coefficientLaw (SourceMode d) + +def phase (d : ℕ) (L : ℝ) (k : Fin d → ℤ) (x : Fin d → ℝ) : ℝ := + ∑ i, sourceC L * (k i : ℝ) * x i + +/-- False is the cosine coefficient and true the independent sine coefficient. -/ +def modeCoefficient (d : ℕ) (L : ℝ) (m : SourceMode d) (x : Fin d → ℝ) : ℝ := + match m with + | none => Real.sqrt (1 / sourceZ d L) + | some (k, b) => Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + if b then Real.sin (phase d L k x) else Real.cos (phase d L k x) + +def modeMajorant (d : ℕ) (L : ℝ) (m : SourceMode d) : ℝ := + match m with + | none => Real.sqrt (1 / sourceZ d L) + | some (k, _) => pairedBound d L k + +/-- Literal normalized real Fourier sum on the common coefficient samples. -/ +def sourceField (d : ℕ) (L : ℝ) (ω : SourceMode d → ℝ) (x : Fin d → ℝ) : ℝ := + scalarSeries (fun m => modeCoefficient d L m x) ω + +theorem modeMajorant_nonneg (d : ℕ) (L : ℝ) (m : SourceMode d) : + 0 ≤ modeMajorant d L m := by + cases m with + | none => exact Real.sqrt_nonneg _ + | some p => + change 0 ≤ pairedBound d L p.1 + unfold pairedBound productBound coordinateBound decay + positivity + +theorem modeMajorant_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + Summable (modeMajorant d L) := by + classical + have hs := pairedBound_subtype_summable d hL (halfLattice d) + have hb : Summable (fun _ : Bool => (1 : ℝ)) := (hasSum_fintype _).summable + have hp : Summable (fun p : ↥(halfLattice d) × Bool => pairedBound d L p.1) := by + simpa only [mul_one] using hs.mul_of_nonneg hb + (fun k => modeMajorant_nonneg d L (some (k, false))) (fun _ => zero_le_one) + let e := Equiv.optionEquivSumPUnit.{0, 0} (↥(halfLattice d) × Bool) + apply e.symm.summable_iff.mp + apply Summable.sum (fun q => modeMajorant d L (e.symm q)) + · simpa [e, Function.comp_def, modeMajorant] using hp + · exact (hasSum_fintype _).summable + +theorem modeCoefficient_bound (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (m : SourceMode d) (x : Fin d → ℝ) : + |modeCoefficient d L m x| ≤ modeMajorant d L m := by + cases m with + | none => + exact (abs_of_nonneg (Real.sqrt_nonneg _)).le + | some p => + rcases p with ⟨k, b⟩ + have hprod : 1 ≤ ∏ i, (1 + |sourceC L * (k.val i : ℝ)|) ^ 4 := by + apply Finset.one_le_prod₀ + intro i _ + apply one_le_pow₀ + linarith [abs_nonneg (sourceC L * (k.val i : ℝ))] + have hamp : Real.sqrt (2 * sourceWeight d L k / sourceZ d L) ≤ + pairedBound d L k := by + rw [pairedBound_eq_amplitude d hL k] + simpa only [mul_one] using mul_le_mul_of_nonneg_left hprod + (Real.sqrt_nonneg (2 * sourceWeight d L k / sourceZ d L)) + change |Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + (if b then Real.sin (phase d L k x) else Real.cos (phase d L k x))| ≤ _ + rw [abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] + have ht : |if b then Real.sin (phase d L k x) else Real.cos (phase d L k x)| ≤ 1 := by + cases b with + | false => exact Real.abs_cos_le_one _ + | true => exact Real.abs_sin_le_one _ + have hbase : Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + |if b then Real.sin (phase d L k x) else Real.cos (phase d L k x)| ≤ + Real.sqrt (2 * sourceWeight d L k / sourceZ d L) := by + simpa only [mul_one] using mul_le_mul_of_nonneg_left ht + (Real.sqrt_nonneg (2 * sourceWeight d L k / sourceZ d L)) + exact hbase.trans hamp + +theorem sourceField_eval_measurable (d : ℕ) (L : ℝ) (x : Fin d → ℝ) : + Measurable (fun ω => sourceField d L ω x) := by + exact scalarSeries_measurable _ + +theorem sourceMajorant_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, Summable (fun m => modeMajorant d L m * |ω m|) := by + exact weighted_abs_summable_ae _ (modeMajorant_nonneg d L) (modeMajorant_summable d hL) + +theorem sourceAbs_uniform_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, + HasSumUniformly (fun m x => |modeCoefficient d L m x * ω m|) + (fun x => ∑' m, |modeCoefficient d L m x * ω m|) := by + filter_upwards [sourceMajorant_ae d hL] with ω hω + apply hasSumUniformly_iff_tendstoUniformly.mpr + apply tendstoUniformly_tsum hω + intro m x + simp only [Real.norm_eq_abs, abs_abs, abs_mul] + exact mul_le_mul_of_nonneg_right (modeCoefficient_bound d hL m x) (abs_nonneg _) + +theorem sourceField_uniform_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, + HasSumUniformly (fun m x => modeCoefficient d L m x * ω m) + (sourceField d L ω) := by + filter_upwards [sourceMajorant_ae d hL] with ω hω + apply hasSumUniformly_iff_tendstoUniformly.mpr + apply tendstoUniformly_tsum hω + intro m x + simp only [Real.norm_eq_abs, abs_mul] + exact mul_le_mul_of_nonneg_right (modeCoefficient_bound d hL m x) (abs_nonneg _) + +theorem sourceField_continuous_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, Continuous (sourceField d L ω) := by + filter_upwards [sourceMajorant_ae d hL] with ω hω + change Continuous (fun x => ∑' m, modeCoefficient d L m x * ω m) + have hcont (m : SourceMode d) : + Continuous (fun x : Fin d → ℝ => modeCoefficient d L m x * ω m) := by + cases m with + | none => + change Continuous (fun _ : Fin d → ℝ => Real.sqrt (1 / sourceZ d L) * ω none) + exact continuous_const + | some p => + rcases p with ⟨k, b⟩ + cases b <;> simp [modeCoefficient, phase] <;> fun_prop + apply continuous_tsum hcont hω + intro m x + simp only [Real.norm_eq_abs, abs_mul] + exact mul_le_mul_of_nonneg_right (modeCoefficient_bound d hL m x) (abs_nonneg _) + +end I4Source diff --git a/frontiers/source_smooth_realization_20261011/SourceGaussianLaw.lean b/frontiers/source_smooth_realization_20261011/SourceGaussianLaw.lean new file mode 100644 index 000000000..bb8450b5a --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceGaussianLaw.lean @@ -0,0 +1,189 @@ +import SourceFourierSeries +import Mathlib.MeasureTheory.Integral.DominatedConvergence +import Mathlib.Probability.Independence.CharacteristicFunction +import Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence +import Mathlib.Analysis.Normed.Ring.InfiniteSum +import Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def + +/-! Actual Gaussian laws of summable coefficient series and finite evaluation combinations. +No covariance/source-kernel, torus, derivative-jet, or pinned-law conclusion is assumed. -/ + +noncomputable section +open I4Foundation I4Weights I4Source MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal NNReal Topology + +namespace I4SourceGaussian + +variable {ι : Type*} + +private theorem summable_square (a : ι → ℝ) (ha : Summable a) : + Summable (fun i => a i ^ 2) := by + have h := summable_mul_of_summable_norm ha.norm ha.norm + simpa only [Function.comp_def, pow_two] using h.comp_injective + (show Function.Injective (fun i : ι => (i, i)) from + fun i j hij => congrArg Prod.fst hij) + +variable [Countable ι] + +omit [Countable ι] in +private theorem partial_charFun (a : ι → ℝ) (s : Finset ι) (t : ℝ) : + charFun ((coefficientLaw ι).map (fun ω => ∑ i ∈ s, a i * ω i)) t = + Complex.exp (-((∑ i ∈ s, a i ^ 2 : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2) := by + classical + have hi : iIndepFun (fun i (ω : ι → ℝ) => a i * ω i) (coefficientLaw ι) := + (coordinates_independent ι).comp (fun i y => a i * y) (fun _ => by fun_prop) + have hm (i : ι) : Measurable (fun ω : ι → ℝ => a i * ω i) := + measurable_const.mul (measurable_pi_apply i) + have hchar (i : ι) : charFun ((coefficientLaw ι).map + (fun ω : ι → ℝ => a i * ω i)) t = + Complex.exp (-((a i : ℂ) * (t : ℂ)) ^ 2 / 2) := by + rw [charFun_map_mul_comp (f := fun ω : ι → ℝ => ω i) + (measurable_pi_apply i).aemeasurable, coordinate_marginal, charFun_gaussianReal] + simp only [Complex.ofReal_mul, mul_zero, Complex.ofReal_zero, zero_mul, + NNReal.coe_one, Complex.ofReal_one, one_mul, zero_sub] + congr 1 + ring + rw [(hi.restrict s).charFun_map_fun_finsetSum_eq_prod (fun i _ => (hm i).aemeasurable)] + simp only [Finset.prod_apply] + simp_rw [hchar] + rw [← Complex.exp_sum] + congr 1 + push_cast + simp only [mul_pow] + rw [← Finset.sum_div, Finset.sum_neg_distrib, ← Finset.sum_mul] + rw [neg_mul] + +private theorem charFun_partial_tendsto (a : ι → ℝ) (ha : Summable a) (t : ℝ) : + Filter.Tendsto + (fun s : Finset ι => charFun ((coefficientLaw ι).map + (fun ω => ∑ i ∈ s, a i * ω i)) t) + Filter.atTop (𝓝 (charFun ((coefficientLaw ι).map (scalarSeries a)) t)) := by + classical + have hm (s : Finset ι) : Measurable (fun ω : ι → ℝ => ∑ i ∈ s, a i * ω i) := + Finset.measurable_sum s (fun i _ => measurable_const.mul (measurable_pi_apply i)) + have heq (s : Finset ι) : + charFun ((coefficientLaw ι).map (fun ω => ∑ i ∈ s, a i * ω i)) t = + ∫ ω, Complex.exp (((t * ∑ i ∈ s, a i * ω i : ℝ) : ℂ) * Complex.I) + ∂coefficientLaw ι := by + rw [charFun_apply_real, integral_map (hm s).aemeasurable (by fun_prop)] + push_cast + rfl + have heq' : charFun ((coefficientLaw ι).map (scalarSeries a)) t = + ∫ ω, Complex.exp (((t * scalarSeries a ω : ℝ) : ℂ) * Complex.I) + ∂coefficientLaw ι := by + rw [charFun_apply_real, integral_map (scalarSeries_measurable a).aemeasurable + (by fun_prop)] + push_cast + rfl + simp_rw [heq, heq'] + apply tendsto_integral_filter_of_norm_le_const + · filter_upwards with s + have hc : Continuous (fun q : ℝ => Complex.exp (((t * q : ℝ) : ℂ) * Complex.I)) := + by fun_prop + exact (hc.measurable.comp (hm s)).aestronglyMeasurable + · refine ⟨1, Filter.Eventually.of_forall (fun s => ?_)⟩ + filter_upwards with ω + rw [Complex.norm_exp_ofReal_mul_I] + · filter_upwards [scalarSeries_hasSum_ae a ha] with ω hω + exact ((by fun_prop : Continuous (fun q : ℝ => + Complex.exp (((t * q : ℝ) : ℂ) * Complex.I))).tendsto _).comp hω + +theorem scalarSeries_map_gaussian (a : ι → ℝ) (ha : Summable a) : + (coefficientLaw ι).map (scalarSeries a) = + gaussianReal 0 (∑' i, a i ^ 2).toNNReal := by + apply Measure.ext_of_charFun + funext t + have h1 := charFun_partial_tendsto a ha t + have h2 : Filter.Tendsto (fun s : Finset ι => + charFun ((coefficientLaw ι).map (fun ω => ∑ i ∈ s, a i * ω i)) t) + Filter.atTop (𝓝 (Complex.exp (-((∑' i, a i ^ 2 : ℝ) : ℂ) * (t : ℂ)^2 / 2))) := by + simp_rw [partial_charFun] + exact ((by fun_prop : Continuous (fun q : ℝ => + Complex.exp (-(q : ℂ) * (t : ℂ)^2 / 2))).tendsto _).comp + (summable_square a ha).hasSum + rw [tendsto_nhds_unique h1 h2, charFun_gaussianReal] + rw [Real.coe_toNNReal _ (tsum_nonneg (fun i => sq_nonneg (a i)))] + congr 1 + push_cast + ring + +theorem scalarSeries_integral_zero (a : ι → ℝ) (ha : Summable a) : + ∫ ω, scalarSeries a ω ∂coefficientLaw ι = 0 := by + have h := integral_id_gaussianReal (μ := 0) (v := (∑' i, a i ^ 2).toNNReal) + rw [← scalarSeries_map_gaussian a ha, + integral_map (scalarSeries_measurable a).aemeasurable (by fun_prop)] at h + exact h + +theorem scalarSeries_variance (a : ι → ℝ) (ha : Summable a) : + Var[scalarSeries a; coefficientLaw ι] = ∑' i, a i ^ 2 := by + rw [← variance_id_map (scalarSeries_measurable a).aemeasurable, + scalarSeries_map_gaussian a ha, variance_id_gaussianReal] + exact Real.coe_toNNReal _ (tsum_nonneg (fun i => sq_nonneg (a i))) + +theorem source_linearCombination_hasGaussianLaw (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (n : ℕ) (x : Fin n → (Fin d → ℝ)) (c : Fin n → ℝ) : + HasGaussianLaw (fun ω => ∑ j, c j * sourceField d L ω (x j)) (sourceLaw d) := by + classical + have hc (j : Fin n) : Summable (fun m => modeCoefficient d L m (x j)) := + (modeMajorant_summable d hL).of_norm_bounded (fun m => by + simpa only [Real.norm_eq_abs] using modeCoefficient_bound d hL m (x j)) + let a : SourceMode d → ℝ := fun m => ∑ j, c j * modeCoefficient d L m (x j) + have ha : Summable a := by + exact summable_sum (fun j _ => (hc j).mul_left (c j)) + have hG : HasGaussianLaw (scalarSeries a) (sourceLaw d) := by + constructor + · exact (scalarSeries_measurable a).aemeasurable + · change IsGaussian ((coefficientLaw (SourceMode d)).map (scalarSeries a)) + rw [scalarSeries_map_gaussian a ha] + infer_instance + apply hG.congr + filter_upwards [ae_all_iff.2 (fun j : Fin n => + scalarSeries_hasSum_ae (fun m => modeCoefficient d L m (x j)) (hc j)), + scalarSeries_hasSum_ae a ha] with ω hω hsum + have h : HasSum (fun m => ∑ j, c j * modeCoefficient d L m (x j) * ω m) + (∑ j, c j * sourceField d L ω (x j)) := by + simpa only [sourceField, mul_assoc] using hasSum_sum (fun j _ => (hω j).mul_left (c j)) + exact hsum.unique (by simpa only [a, Finset.sum_mul] using h) + +theorem source_finiteVector_hasGaussianLaw (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (n : ℕ) (x : Fin n → (Fin d → ℝ)) : + HasGaussianLaw (fun ω j => sourceField d L ω (x j)) (sourceLaw d) := by + classical + have hm : Measurable (fun ω j => sourceField d L ω (x j)) := + Measurable.of_eval (fun j => sourceField_eval_measurable d L (x j)) + refine ⟨hm.aemeasurable, ?_⟩ + apply isGaussian_of_map_eq_gaussianReal + intro ell + let c : Fin n → ℝ := fun j => ell (Pi.single j 1) + have hrep (v : Fin n → ℝ) : ell v = ∑ j, c j * v j := by + rw [← LinearMap.sum_single_apply (fun _ : Fin n => ℝ) v, map_sum] + apply Finset.sum_congr rfl + intro j _ + have hs : Pi.single j (v j) = v j • Pi.single j (1 : ℝ) := by + rw [← Pi.single_smul, smul_eq_mul, mul_one] + rw [hs, map_smul] + simp [c, smul_eq_mul, mul_comm] + have hg : HasGaussianLaw (fun ω => ell (fun j => sourceField d L ω (x j))) + (sourceLaw d) := + (source_linearCombination_hasGaussianLaw d hL n x c).congr + (Filter.Eventually.of_forall (fun ω => (hrep _).symm)) + refine ⟨(sourceLaw d)[fun ω => ell (fun j => sourceField d L ω (x j))], + Var[fun ω => ell (fun j => sourceField d L ω (x j)); sourceLaw d].toNNReal, ?_⟩ + rw [Measure.map_map ell.continuous.measurable hm] + exact hg.map_eq_gaussianReal + +theorem sourceField_isGaussianProcess (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + IsGaussianProcess (fun x ω => sourceField d L ω x) (sourceLaw d) := by + classical + constructor + intro I + let e : ↥I ≃ Fin (Fintype.card ↥I) := Fintype.equivFin ↥I + let x : Fin (Fintype.card ↥I) → (Fin d → ℝ) := fun j => (e.symm j).1 + let R : (Fin (Fintype.card ↥I) → ℝ) →L[ℝ] (↥I → ℝ) := + ContinuousLinearMap.pi (fun i => ContinuousLinearMap.proj (e i)) + apply ((source_finiteVector_hasGaussianLaw d hL _ x).map_fun R).congr + filter_upwards with ω + funext i + simp [R, x] + +end I4SourceGaussian diff --git a/frontiers/source_smooth_realization_20261011/SourceKernel.lean b/frontiers/source_smooth_realization_20261011/SourceKernel.lean new file mode 100644 index 000000000..5d5602ac7 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceKernel.lean @@ -0,0 +1,112 @@ +import SourceLattice +import Mathlib.Analysis.Normed.Ring.InfiniteSum + +noncomputable section +open I4Foundation I4Weights I4Source I4Lattice MeasureTheory +open scoped BigOperators +namespace I4Kernel + +def frequencyEquiv (d : ℕ) : SourceMode d ≃ (Fin d → ℤ) := + Equiv.ofBijective (latticeFrequency d) (latticeFrequency_bijective d) + +/-- The prescribed normalized full-lattice real Fourier kernel; image/Poisson linkage is separate. -/ +def sourceSpectralKernel (d : ℕ) (L : ℝ) (z : Fin d → ℝ) : ℝ := + ∑' k : Fin d → ℤ, sourceWeight d L k / sourceZ d L * Real.cos (phase d L k z) + +private theorem tsum_mode (d : ℕ) (f : SourceMode d → ℝ) (hf : Summable f) : + (∑' m, f m) = f none + ∑' k : ↥(halfLattice d), + (f (some (k,false)) + f (some (k,true))) := by + classical + let e := Equiv.optionEquivSumPUnit.{0,0} (↥(halfLattice d) × Bool) + have hp : Summable (fun p : ↥(halfLattice d) × Bool => f (some p)) := + hf.comp_injective (Option.some_injective (↥(halfLattice d) × Bool)) + calc + (∑' m, f m) = ∑' q, f (e.symm q) := (e.symm.tsum_eq f).symm + _ = (∑' p : ↥(halfLattice d) × Bool, f (some p)) + f none := by + rw [Summable.tsum_sum (by simpa [e, Function.comp_def] using hp) + (hasSum_fintype _).summable] + simp [e] + _ = _ := by + rw [hp.tsum_prod] + simp_rw [tsum_bool] + ring + +theorem modeProduct_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x y : Fin d → ℝ) : + Summable (fun m => modeCoefficient d L m x * modeCoefficient d L m y) := by + have hc (z : Fin d → ℝ) : Summable (fun m => modeCoefficient d L m z) := by + apply Summable.of_norm_bounded (modeMajorant_summable d hL) + intro m + simpa only [Real.norm_eq_abs] using modeCoefficient_bound d hL m z + have hp : Summable (fun p : SourceMode d × SourceMode d => + modeCoefficient d L p.1 x * modeCoefficient d L p.2 y) := + summable_mul_of_summable_norm (hc x).norm (hc y).norm + simpa only [Function.comp_def] using hp.comp_injective + (show Function.Injective (fun m : SourceMode d => (m,m)) from + fun a b h => congrArg Prod.fst h) + +theorem spectralKernel_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) (z : Fin d → ℝ) : + Summable (fun k : Fin d → ℤ => + sourceWeight d L k / sourceZ d L * Real.cos (phase d L k z)) := by + have hz := sourceZ_pos d hL + apply Summable.of_norm_bounded ((sourceWeight_summable d hL).div_const (sourceZ d L)) + intro k + have hq : 0 ≤ sourceWeight d L k / sourceZ d L := by + rw [sourceWeight_eq_physical] + exact div_nonneg (Real.exp_pos _).le hz.le + rw [norm_mul, Real.norm_eq_abs, abs_of_nonneg hq, Real.norm_eq_abs] + simpa only [mul_one] using mul_le_mul_of_nonneg_left (Real.abs_cos_le_one _) hq + +theorem coefficientKernel_eq_fullLattice (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x y : Fin d → ℝ) : + (∑' m, modeCoefficient d L m x * modeCoefficient d L m y) = + sourceSpectralKernel d L (x - y) := by + classical + let g : (Fin d → ℤ) → ℝ := fun k => + sourceWeight d L k / sourceZ d L * Real.cos (phase d L k (x - y)) + have hg : Summable g := spectralKernel_summable d hL (x - y) + have hneg (k : Fin d → ℤ) : g (-k) = g k := by + have hp : phase d L (-k) (x - y) = -phase d L k (x - y) := by + simp [phase, Finset.sum_neg_distrib] + simp only [g, sourceWeight_neg, hp, Real.cos_neg] + have hzero : g 0 = 1 / sourceZ d L := by + simp [g, sourceWeight_eq_physical, phase] + have hc0 : modeCoefficient d L none x * modeCoefficient d L none y = 1 / sourceZ d L := by + simp only [modeCoefficient] + exact Real.mul_self_sqrt (one_div_nonneg.mpr (sourceZ_pos d hL).le) + have hpair (k : ↥(halfLattice d)) : + modeCoefficient d L (some (k,false)) x * modeCoefficient d L (some (k,false)) y + + modeCoefficient d L (some (k,true)) x * modeCoefficient d L (some (k,true)) y = 2 * g k := by + have h := pairedCoefficient_kernel d hL k x y + rw [Fintype.sum_bool] at h + calc + _ = modeCoefficient d L (some (k,true)) x * modeCoefficient d L (some (k,true)) y + + modeCoefficient d L (some (k,false)) x * modeCoefficient d L (some (k,false)) y := add_comm _ _ + _ = _ := h + _ = 2 * g k := by dsimp [g]; ring + have hleft : (∑' m, modeCoefficient d L m x * modeCoefficient d L m y) = + 1 / sourceZ d L + ∑' k : ↥(halfLattice d), 2 * g k := by + rw [tsum_mode d _ (modeProduct_summable d hL x y), hc0] + congr 1 + exact tsum_congr hpair + have hm : Summable (fun m => g (frequencyEquiv d m)) := (frequencyEquiv d).summable_iff.mpr hg + have hright : sourceSpectralKernel d L (x - y) = + 1 / sourceZ d L + ∑' k : ↥(halfLattice d), 2 * g k := by + change (∑' k, g k) = _ + rw [← (frequencyEquiv d).tsum_eq g, tsum_mode d _ hm] + change g 0 + (∑' k : ↥(halfLattice d), (g k.1 + g (-k.1))) = _ + rw [hzero] + congr 1 + apply tsum_congr + intro k + rw [hneg] + ring + exact hleft.trans hright.symm + +theorem spectralKernel_zero (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + sourceSpectralKernel d L 0 = 1 := by + unfold sourceSpectralKernel + simp only [phase, Pi.zero_apply, mul_zero, Finset.sum_const_zero, Real.cos_zero, mul_one] + rw [tsum_div_const] + change sourceZ d L / sourceZ d L = 1 + exact div_self (sourceZ_pos d hL).ne' + +end I4Kernel diff --git a/frontiers/source_smooth_realization_20261011/SourceLattice.lean b/frontiers/source_smooth_realization_20261011/SourceLattice.lean new file mode 100644 index 000000000..9c1e0557c --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceLattice.lean @@ -0,0 +1,159 @@ +import SourceFourierSeries +import Mathlib.Data.Finset.Max + +noncomputable section +open I4Foundation I4Weights I4Source MeasureTheory +open scoped BigOperators +namespace I4Lattice + +def latticeFrequency (d : ℕ) (m : SourceMode d) : Fin d → ℤ := + match m with + | none => 0 + | some (k, b) => if b then -k.1 else k.1 + +theorem halfLattice_ne_zero (d : ℕ) {k : Fin d → ℤ} (hk : k ∈ halfLattice d) : + k ≠ 0 := by + rcases hk with ⟨i, hi, _⟩ + intro h + have : k i = 0 := congrFun h i + omega + +theorem halfLattice_partition (d : ℕ) {k : Fin d → ℤ} (hk : k ≠ 0) : + (k ∈ halfLattice d ∨ -k ∈ halfLattice d) ∧ + ¬ (k ∈ halfLattice d ∧ -k ∈ halfLattice d) := by + classical + have hex : ∃ i, k i ≠ 0 := by + by_contra h + push Not at h + exact hk (funext h) + let s : Finset (Fin d) := Finset.univ.filter (fun i => k i ≠ 0) + have hs : s.Nonempty := by + obtain ⟨i, hi⟩ := hex + exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ i, hi⟩⟩ + let i := s.min' hs + have hi : k i ≠ 0 := (Finset.mem_filter.mp (Finset.min'_mem s hs)).2 + have hbefore (j : Fin d) (hj : j < i) : k j = 0 := by + by_contra hn + have hle := Finset.min'_le s j (Finset.mem_filter.mpr ⟨Finset.mem_univ j, hn⟩) + exact (not_le_of_gt hj) hle + constructor + · rcases lt_or_gt_of_ne hi with hneg | hpos + · right + refine ⟨i, ?_, ?_⟩ + · change 0 < -k i + omega + · intro j hj + change -k j = 0 + rw [hbefore j hj, neg_zero] + · exact Or.inl ⟨i, hpos, hbefore⟩ + · rintro ⟨⟨i, hi, hib⟩, ⟨j, hj, hjb⟩⟩ + change 0 < -k j at hj + rcases lt_trichotomy i j with hij | heq | hji + · have h0 := hjb i hij + change -k i = 0 at h0 + omega + · subst j + omega + · have h0 := hib j hji + omega + +theorem sourceWeight_neg (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : + sourceWeight d L (-k) = sourceWeight d L k := by + rw [sourceWeight_eq_physical, sourceWeight_eq_physical] + simp only [Pi.neg_apply, Int.cast_neg, mul_neg, neg_sq] + +theorem phase_lattice_shift (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (k n : Fin d → ℤ) (x : Fin d → ℝ) : + phase d L k (fun i => x i + L * (n i : ℝ)) = + phase d L k x + ((∑ i, k i * n i : ℤ) : ℝ) * (2 * Real.pi) := by + have he (i : Fin d) : sourceC L * (k i : ℝ) * (x i + L * (n i : ℝ)) = + sourceC L * (k i : ℝ) * x i + ((k i * n i : ℤ) : ℝ) * (2 * Real.pi) := by + simp only [Int.cast_mul] + unfold sourceC + field_simp + unfold phase + simp_rw [he] + rw [Finset.sum_add_distrib, ← Finset.sum_mul] + simp only [Int.cast_sum] + +theorem modeCoefficient_lattice_shift (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (m : SourceMode d) (n : Fin d → ℤ) (x : Fin d → ℝ) : + modeCoefficient d L m (fun i => x i + L * (n i : ℝ)) = + modeCoefficient d L m x := by + cases m with + | none => rfl + | some p => + rcases p with ⟨k,b⟩ + cases b <;> simp only [modeCoefficient, Bool.false_eq_true, ite_false, ite_true] + · rw [phase_lattice_shift d hL, Real.cos_add_int_mul_two_pi] + · rw [phase_lattice_shift d hL, Real.sin_add_int_mul_two_pi] + +theorem sourceField_lattice_shift (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SourceMode d → ℝ) (n : Fin d → ℤ) (x : Fin d → ℝ) : + sourceField d L ω (fun i => x i + L * (n i : ℝ)) = sourceField d L ω x := by + unfold sourceField scalarSeries + apply tsum_congr + intro m + change modeCoefficient d L m (fun i => x i + L * (n i : ℝ)) * ω m = + modeCoefficient d L m x * ω m + rw [modeCoefficient_lattice_shift d hL] + +theorem pairedCoefficient_kernel (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (k : ↥(halfLattice d)) (x y : Fin d → ℝ) : + (∑ b : Bool, modeCoefficient d L (some (k,b)) x * + modeCoefficient d L (some (k,b)) y) = + (2 * sourceWeight d L k / sourceZ d L) * Real.cos (phase d L k (x - y)) := by + have hphase : phase d L k (x - y) = phase d L k x - phase d L k y := by + simp [phase, mul_sub, Finset.sum_sub_distrib] + have hz : 0 ≤ 2 * sourceWeight d L k / sourceZ d L := by + rw [sourceWeight_eq_physical] + exact div_nonneg (mul_nonneg (by norm_num) (Real.exp_pos _).le) (sourceZ_pos d hL).le + rw [Fintype.sum_bool] + simp only [modeCoefficient, ite_true, Bool.false_eq_true, ite_false] + rw [hphase, Real.cos_sub] + calc + _ = (Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + Real.sqrt (2 * sourceWeight d L k / sourceZ d L)) * + (Real.cos (phase d L k x) * Real.cos (phase d L k y) + + Real.sin (phase d L k x) * Real.sin (phase d L k y)) := by ring + _ = _ := by rw [Real.mul_self_sqrt hz] + +theorem latticeFrequency_bijective (d : ℕ) : Function.Bijective (latticeFrequency d) := by + classical + constructor + · intro m n he + cases m with + | none => + cases n with + | none => rfl + | some p => + rcases p with ⟨k,b⟩ + have hk := halfLattice_ne_zero d k.property + cases b <;> simp [latticeFrequency] at he <;> exact (hk (by first | exact he | exact he.symm)).elim + | some p => + rcases p with ⟨k,b⟩ + cases n with + | none => + have hk := halfLattice_ne_zero d k.property + cases b <;> simp [latticeFrequency] at he <;> exact (hk he).elim + | some q => + rcases q with ⟨l,c⟩ + cases b <;> cases c <;> simp only [latticeFrequency, Bool.false_eq_true, ite_false, ite_true] at he + · have hkl : k = l := Subtype.ext he + subst l + rfl + · have hn : -k.1 ∈ halfLattice d := by simpa only [he, neg_neg] using l.property + exact ((halfLattice_partition d (halfLattice_ne_zero d k.property)).2 ⟨k.property,hn⟩).elim + · have hn : -k.1 ∈ halfLattice d := he.symm ▸ l.property + exact ((halfLattice_partition d (halfLattice_ne_zero d k.property)).2 ⟨k.property,hn⟩).elim + · have hkl : k = l := Subtype.ext (neg_inj.mp he) + subst l + rfl + · intro k + by_cases hk : k = 0 + · exact ⟨none, by simpa [latticeFrequency] using hk.symm⟩ + · rcases (halfLattice_partition d hk).1 with hp | hn + · exact ⟨some (⟨k,hp⟩,false), by simp [latticeFrequency]⟩ + · exact ⟨some (⟨-k,hn⟩,true), by simp [latticeFrequency]⟩ + +end I4Lattice diff --git a/frontiers/source_smooth_realization_20261011/SourceSmooth.lean b/frontiers/source_smooth_realization_20261011/SourceSmooth.lean new file mode 100644 index 000000000..dee9dd9a5 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceSmooth.lean @@ -0,0 +1,253 @@ +import SourceC4 +import Mathlib.Data.Nat.Choose.Sum + +/-! +# All-order smoothness of the actual infinite Gaussian Fourier source + +This module extends the source-derived polynomial majorant from order four to +every natural order. It uses the same SourceMode, sourceLaw and sourceField as +the qualified F7 dependency; no finite-mode approximation or new field is used. +The good sample predicate is a single countable intersection of explicit +coefficient summability conditions. Its measurability and probability-law +restriction are proved in SourceSmoothCarrier. + +This is a C261 Stage A prerequisite. It does not identify the spectral covariance +with Lifetime's theta sum, construct a conditional kernel, or discharge a +weighted elder, Morse, count/density, or universality conclusion. +-/ + +noncomputable section +open I4Foundation I4Weights I4Source I4C4 MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal + +namespace I4Smooth + +def orderCoordinateBound (n : ℕ) (a c : ℝ) (k : ℤ) : ℝ := + decay a k * (1 + |c * (k : ℝ)|) ^ n + +def orderProductBound (n d : ℕ) (a c : ℝ) (k : Fin d → ℤ) : ℝ := + ∏ i, orderCoordinateBound n a c (k i) + +def orderPairedBound (n d : ℕ) (L : ℝ) (k : Fin d → ℤ) : ℝ := + Real.sqrt (2 / sourceZ d L) * orderProductBound n d (sourceA L) (sourceC L) k + +def orderModeBound (n d : ℕ) (L : ℝ) (m : SourceMode d) : ℝ := + match m with + | none => Real.sqrt (1 / sourceZ d L) + | some (k, _) => orderPairedBound n d L k + +theorem orderCoordinateBound_summable (n : ℕ) {a c : ℝ} (ha : 0 < a) : + Summable (orderCoordinateBound n a c) := by + classical + let f (r : ℕ) (k : ℤ) : ℝ := + ((n.choose r : ℝ) * |c| ^ (n - r)) * (decay a k * |(k : ℝ)| ^ (n - r)) + have hf (r : ℕ) : Summable (f r) := + (summable_decay_pow ha (n - r)).mul_left _ + have hsum (s : Finset ℕ) : Summable (fun k : ℤ => ∑ r ∈ s, f r k) := by + induction s using Finset.induction_on with + | empty => simpa using (summable_zero : Summable (fun _ : ℤ => (0 : ℝ))) + | @insert r s hr ih => + simpa only [Finset.sum_insert hr] using (hf r).add ih + convert hsum (Finset.range (n + 1)) using 1 + funext k + unfold orderCoordinateBound + rw [add_pow, Finset.mul_sum] + apply Finset.sum_congr rfl + intro r _ + simp only [one_pow, one_mul, abs_mul, mul_pow, f] + ring + +theorem orderProductBound_summable (n d : ℕ) {a c : ℝ} (ha : 0 < a) : + Summable (orderProductBound n d a c) := by + exact finite_product_summable (orderCoordinateBound_summable n ha) + (fun k => by unfold orderCoordinateBound decay; positivity) d + +theorem orderPairedBound_summable (n d : ℕ) {L : ℝ} (hL : L ≠ 0) : + Summable (orderPairedBound n d L) := by + exact (orderProductBound_summable n d (sourceA_pos hL)).mul_left _ + +theorem orderPairedBound_eq_amplitude (n d : ℕ) {L : ℝ} (hL : L ≠ 0) + (k : Fin d → ℤ) : + orderPairedBound n d L k = + Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + ∏ i, (1 + |sourceC L * (k i : ℝ)|) ^ n := by + have hsqrt : Real.sqrt (sourceWeight d L k) = productDecay d (sourceA L) k := by + have hw : sourceWeight d L k = (productDecay d (sourceA L) k) ^ 2 := by + rw [sourceWeight, productDecay_eq_exp, productDecay_eq_exp, pow_two, ← Real.exp_add] + congr 1 + ring + rw [hw, Real.sqrt_sq_eq_abs, abs_of_nonneg] + unfold productDecay decay + positivity + have hamp : Real.sqrt (2 * sourceWeight d L k / sourceZ d L) = + Real.sqrt (2 / sourceZ d L) * productDecay d (sourceA L) k := by + have he : 2 * sourceWeight d L k / sourceZ d L = + (2 / sourceZ d L) * sourceWeight d L k := by ring + rw [he, Real.sqrt_mul (by have := sourceZ_pos d hL; positivity), hsqrt] + have hp : orderProductBound n d (sourceA L) (sourceC L) k = + productDecay d (sourceA L) k * ∏ i, (1 + |sourceC L * (k i : ℝ)|) ^ n := by + exact Finset.prod_mul_distrib + rw [orderPairedBound, hp, hamp] + ring + +theorem orderModeBound_nonneg (n d : ℕ) (L : ℝ) (m : SourceMode d) : + 0 ≤ orderModeBound n d L m := by + cases m with + | none => exact Real.sqrt_nonneg _ + | some p => + unfold orderModeBound orderPairedBound orderProductBound orderCoordinateBound decay + positivity + +theorem orderModeBound_summable (n d : ℕ) {L : ℝ} (hL : L ≠ 0) : + Summable (orderModeBound n d L) := by + classical + have hs := (orderPairedBound_summable n d hL).subtype (halfLattice d) + have hb : Summable (fun _ : Bool => (1 : ℝ)) := (hasSum_fintype _).summable + have hp : Summable (fun p : ↥(halfLattice d) × Bool => orderPairedBound n d L p.1) := by + simpa only [mul_one] using hs.mul_of_nonneg hb + (fun k => orderModeBound_nonneg n d L (some (k, false))) (fun _ => zero_le_one) + let e := Equiv.optionEquivSumPUnit.{0, 0} (↥(halfLattice d) × Bool) + apply e.symm.summable_iff.mp + apply Summable.sum (fun q => orderModeBound n d L (e.symm q)) + · simpa [e, Function.comp_def, orderModeBound] using hp + · exact (hasSum_fintype _).summable + +theorem orderModeBound_four (d : ℕ) (L : ℝ) (m : SourceMode d) : + orderModeBound 4 d L m = modeMajorant d L m := by + cases m <;> rfl + +theorem modeCoefficient_iteratedFDeriv_order_bound (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (m : SourceMode d) (j : ℕ) (x : Fin d → ℝ) : + ‖iteratedFDeriv ℝ j (modeCoefficient d L m) x‖ ≤ orderModeBound j d L m := by + classical + cases m with + | none => + cases j with + | zero => + simpa only [norm_iteratedFDeriv_zero, Real.norm_eq_abs, orderModeBound] using + modeCoefficient_bound d hL none x + | succ j => + change ‖iteratedFDeriv ℝ (j + 1) + (fun _ : Fin d → ℝ => Real.sqrt (1 / sourceZ d L)) x‖ ≤ Real.sqrt (1 / sourceZ d L) + rw [iteratedFDeriv_succ_const] + simp only [Pi.zero_apply, norm_zero] + exact Real.sqrt_nonneg _ + | some p => + rcases p with ⟨k, b⟩ + let A := Real.sqrt (2 * sourceWeight d L k / sourceZ d L) + let P := ∏ i, (1 + |sourceC L * (k.1 i : ℝ)|) + let g : ℝ → ℝ := if b then Real.sin else Real.cos + let ell := phaseCLM d L k + have hg : ContDiff ℝ j g := by + cases b <;> simp only [g, Bool.false_eq_true, ite_false, ite_true] <;> fun_prop + have hgc : ContDiff ℝ j (g ∘ ell) := hg.comp_continuousLinearMap + have hgn : ‖iteratedFDeriv ℝ j g (ell x)‖ ≤ 1 := by + cases b with + | false => + simpa only [g, Bool.false_eq_true, ite_false, + norm_iteratedFDeriv_eq_norm_iteratedDeriv, Real.norm_eq_abs] using + Real.abs_iteratedDeriv_cos_le_one j (ell x) + | true => + simpa only [g, ite_true, norm_iteratedFDeriv_eq_norm_iteratedDeriv, + Real.norm_eq_abs] using Real.abs_iteratedDeriv_sin_le_one j (ell x) + have hl : ‖ell‖ ≤ P := by + calc + ‖ell‖ ≤ ∑ i, |sourceC L * (k.1 i : ℝ)| := phaseCLM_norm_le d L k + _ ≤ 1 + ∑ i, |sourceC L * (k.1 i : ℝ)| := by linarith + _ ≤ P := frequency_l1_le_product d _ (fun i => abs_nonneg _) + have hpow : ‖ell‖ ^ j ≤ P ^ j := by gcongr + have hder : ‖iteratedFDeriv ℝ j (g ∘ ell) x‖ ≤ ‖ell‖ ^ j := by + rw [ell.iteratedFDeriv_comp_right hg x le_rfl] + calc + _ ≤ ‖iteratedFDeriv ℝ j g (ell x)‖ * ∏ _i : Fin j, ‖ell‖ := + (iteratedFDeriv ℝ j g (ell x)).norm_compContinuousLinearMap_le (fun _ => ell) + _ ≤ 1 * ∏ _i : Fin j, ‖ell‖ := + mul_le_mul_of_nonneg_right hgn (Finset.prod_nonneg (fun _ _ => norm_nonneg _)) + _ = ‖ell‖ ^ j := by simp + have heq : modeCoefficient d L (some (k, b)) = A • (g ∘ ell) := by + funext y + cases b <;> simp [modeCoefficient, A, g, Function.comp_apply, Pi.smul_apply, + smul_eq_mul, ell, phaseCLM_apply] + rw [heq, iteratedFDeriv_const_smul_apply hgc.contDiffAt, norm_smul, + Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] + calc + _ ≤ A * P ^ j := mul_le_mul_of_nonneg_left (hder.trans hpow) (Real.sqrt_nonneg _) + _ = orderModeBound j d L (some (k, b)) := by + rw [orderModeBound, orderPairedBound_eq_amplitude j d hL k] + simp only [A, P, Finset.prod_pow] + +/-- One explicit coefficient event, shared by every derivative order. -/ +def goodSample (d : ℕ) (L : ℝ) (ω : SourceMode d → ℝ) : Prop := + ∀ n : ℕ, Summable (fun m => orderModeBound n d L m * |ω m|) + +theorem goodSample_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, goodSample d L ω := by + apply ae_all_iff.mpr + intro n + exact weighted_abs_summable_ae _ (orderModeBound_nonneg n d L) + (orderModeBound_summable n d hL) + +theorem sourceField_smooth_of_goodSample (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SourceMode d → ℝ) (hω : goodSample d L ω) : + ∀ n : ℕ, ContDiff ℝ n (sourceField d L ω) := by + intro n + have hc (m : SourceMode d) : ContDiff ℝ n (modeCoefficient d L m) := by + cases m with + | none => + change ContDiff ℝ n (fun _ : Fin d → ℝ => Real.sqrt (1 / sourceZ d L)) + fun_prop + | some p => + rcases p with ⟨k, b⟩ + change ContDiff ℝ n (fun x : Fin d → ℝ => + Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + (if b then Real.sin (phase d L k x) else Real.cos (phase d L k x))) + cases b <;> simp [phase] <;> fun_prop + change ContDiff ℝ n (fun x => ∑' m, modeCoefficient d L m x * ω m) + apply contDiff_tsum (v := fun j m => orderModeBound j d L m * |ω m|) + · intro m + exact (hc m).mul contDiff_const + · intro j _ + exact hω j + · intro j m x hj + have hcj : ContDiff ℝ j (modeCoefficient d L m) := + (hc m).of_le (by exact_mod_cast hj) + have heq : (fun y => modeCoefficient d L m y * ω m) = + ω m • modeCoefficient d L m := by + funext y + simp [smul_eq_mul, mul_comm] + rw [heq, iteratedFDeriv_const_smul_apply hcj.contDiffAt, norm_smul, Real.norm_eq_abs] + simpa only [mul_comm] using mul_le_mul_of_nonneg_left + (modeCoefficient_iteratedFDeriv_order_bound d hL m j x) (abs_nonneg (ω m)) + +theorem sourceField_smooth_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, ∀ n : ℕ, ContDiff ℝ n (sourceField d L ω) := by + filter_upwards [goodSample_ae d hL] with ω hω + exact sourceField_smooth_of_goodSample d hL ω hω + +/-- The carrier depends only on the coefficient tail; finite coordinate changes +cannot destroy any derivative-order summability condition. -/ +theorem goodSample_congr_cofinite (d : ℕ) (L : ℝ) + (ω η : SourceMode d → ℝ) (hωη : ω =ᶠ[Filter.cofinite] η) : + goodSample d L ω ↔ goodSample d L η := by + constructor + · intro hω n + apply (hω n).congr_cofinite + filter_upwards [hωη] with m hm + rw [hm] + · intro hη n + apply (hη n).congr_cofinite + filter_upwards [hωη.symm] with m hm + rw [hm] + +theorem goodSample_finite_change_iff (d : ℕ) (L : ℝ) + (ω η : SourceMode d → ℝ) (s : Finset (SourceMode d)) + (hωη : ∀ m ∉ s, ω m = η m) : + goodSample d L ω ↔ goodSample d L η := by + apply goodSample_congr_cofinite d L ω η + apply Filter.eventually_cofinite.mpr + apply s.finite_toSet.subset + intro m hm + by_contra hms + exact hm (hωη m hms) + +end I4Smooth diff --git a/frontiers/source_smooth_realization_20261011/SourceSmoothAxiomAudit.lean b/frontiers/source_smooth_realization_20261011/SourceSmoothAxiomAudit.lean new file mode 100644 index 000000000..e22ec44e5 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceSmoothAxiomAudit.lean @@ -0,0 +1,68 @@ +import SourceSmoothControls +import Lean + +#print axioms I4Smooth.sourceField_smooth_ae +#print axioms I4SmoothCarrier.sampleInclusion_map +#print axioms I4SmoothCarrier.smoothLaw_isProbabilityMeasure +#print axioms I4SmoothCarrier.smoothSourceField_finiteVector_hasGaussianLaw +#print axioms I4SmoothCarrier.smoothTorusSourceField_smooth + +-- Actual imported module identities select every environment constant, including +-- generated declarations and private helpers. Endpoint lines do not define coverage. +open Lean Elab Command in +run_cmd do + let env := (← getEnv).setExporting false + let allowed : Array Name := #[`propext, `Classical.choice, `Quot.sound] + let modules : Array Name := #[ + `GaussianSeriesFoundation, `SpectralWeights, `SourceFourierSeries, + `SourceC4, `SourceGaussianLaw, `SourceLattice, `SourceKernel, + `SourceCovariance, `SourceTorus, `SourceTorusC4, + `SourceSmooth, `SourceSmoothCarrier, `SourceSmoothControls] + let some carrierIdx := env.getModuleIdx? `SourceSmoothCarrier + | throwError "missing carrier module for private-helper guards" + let mut allNames : Array Name := #[] + for modName in modules do + let some idx := env.getModuleIdx? modName + | throwError "missing audited module: {modName}" + let names := (env.constants.toList.filterMap fun (name, _) => + if env.getModuleIdxFor? name == some idx then some name else none).toArray.qsort Name.lt + if names.isEmpty then + throwError "empty declaration inventory for audited module: {modName}" + logInfo m!"SMOOTH_AUDIT_MODULE {modName} COUNT {names.size}" + for name in names do + if (env.checked.get.find? name).isNone then + throwError "missing kernel declaration: {name}" + let axs ← Lean.collectAxioms name + logInfo m!"SMOOTH_AUDIT_DECL {name} AXIOMS {axs}" + for ax in axs do + unless allowed.contains ax do + throwError "forbidden transitive axiom {ax} in {name}" + allNames := allNames.push name + let required : Array Name := #[ + `I4Foundation.coefficientLaw, + `I4SourceGaussian.source_finiteVector_hasGaussianLaw, + `I4SourceCovariance.sourceField_variance_one, + `I4Smooth.goodSample, `I4Smooth.goodSample_ae, + `I4Smooth.sourceField_smooth_of_goodSample, + `I4Smooth.goodSample_finite_change_iff, + `I4SmoothCarrier.goodSet_measurable, `I4SmoothCarrier.sampleInclusion_map, + `I4SmoothCarrier.smoothLaw_isProbabilityMeasure, + `I4SmoothCarrier.observation_map_eq, + `I4SmoothCarrier.smoothSourceField_finiteVector_hasGaussianLaw, + `I4SmoothCarrier.smoothSourceField_covariance, + `I4SmoothCarrier.smoothTorusSourceField_smooth, + `I4SmoothControls.old_four_does_not_fill_all_orders, + `I4SmoothControls.field_variance_one] + for name in required do + unless allNames.contains name do + throwError "required source-law declaration omitted from audit: {name}" + let privateHelpers : Array Name := #[ + `I4SmoothCarrier.orderAbsNN, `I4SmoothCarrier.orderAbsTotal, + `I4SmoothCarrier.orderAbsTotal_ne_top_iff, + `I4SmoothCarrier.orderAbsTotal_measurable] + for helper in privateHelpers do + unless allNames.any (fun name => + env.getModuleIdxFor? name == some carrierIdx && + Lean.privateToUserName? name == some helper) do + throwError "required carrier-private helper omitted from audit: {helper}" + logInfo m!"SMOOTH_AUDIT_STANDARD_ONLY_PASS COUNT {allNames.size}" diff --git a/frontiers/source_smooth_realization_20261011/SourceSmoothCarrier.lean b/frontiers/source_smooth_realization_20261011/SourceSmoothCarrier.lean new file mode 100644 index 000000000..733328a3e --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceSmoothCarrier.lean @@ -0,0 +1,230 @@ +import SourceSmooth +import SourceGaussianLaw +import SourceCovariance +import SourceTorusC4 +import Mathlib.MeasureTheory.Measure.Restrict +import Mathlib.MeasureTheory.Measure.Typeclasses.Probability +import Mathlib.MeasureTheory.Constructions.BorelSpace.Real + +/-! +# A measurable smooth carrier for the actual source law + +The carrier consists of the coefficient samples satisfying every explicit +order-weighted absolute summability condition from SourceSmooth. Its measure is +the pullback of the existing product Gaussian sourceLaw under literal subtype +inclusion. Inclusion pushes this measure back to exactly sourceLaw, so finite +coefficient observations, field evaluation laws, and covariance are unchanged. + +The construction concerns the same literal Fourier source, for fixed d and L. +It does not identify the spectral kernel with a periodized theta kernel, define +a conditional kernel or a smooth-function-space law, or discharge a Lifetime +Field adapter, Morse, elder, counting, density, or universality conclusion. +-/ + +noncomputable section +open I4Foundation I4Source I4Smooth I4SourceGaussian I4SourceCovariance I4Kernel +open I4Torus I4TorusC4 MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal Manifold ContDiff Topology + +namespace I4SmoothCarrier + +/-- The actual common coefficient event, with no smoothness premise added. -/ +def goodSet (d : ℕ) (L : ℝ) : Set (SourceMode d → ℝ) := + {ω | goodSample d L ω} + +private def orderAbsNN (n d : ℕ) (L : ℝ) (ω : SourceMode d → ℝ) + (m : SourceMode d) : ℝ≥0 := + ⟨orderModeBound n d L m * |ω m|, + mul_nonneg (orderModeBound_nonneg n d L m) (abs_nonneg _)⟩ + +private def orderAbsTotal (n d : ℕ) (L : ℝ) (ω : SourceMode d → ℝ) : ℝ≥0∞ := + ∑' m, (orderAbsNN n d L ω m : ℝ≥0∞) + +private theorem orderAbsTotal_ne_top_iff (n d : ℕ) (L : ℝ) + (ω : SourceMode d → ℝ) : + orderAbsTotal n d L ω ≠ ∞ ↔ + Summable (fun m => orderModeBound n d L m * |ω m|) := by + simpa only [orderAbsTotal, orderAbsNN] using + (ENNReal.tsum_coe_ne_top_iff_summable_coe (f := orderAbsNN n d L ω)) + +private theorem orderAbsTotal_measurable (n d : ℕ) (L : ℝ) : + Measurable (orderAbsTotal n d L) := by + unfold orderAbsTotal + simp_rw [ENNReal.tsum_eq_iSup_sum] + apply Measurable.iSup + intro s + apply s.measurable_fun_sum + intro m _ + have hm : Measurable (fun ω : SourceMode d → ℝ => orderAbsNN n d L ω m) := by + unfold orderAbsNN + exact (measurable_const.mul (measurable_pi_apply m).abs).nnreal_mk + exact hm.coe_nnreal_ennreal + +theorem goodSet_measurable (d : ℕ) (L : ℝ) : MeasurableSet (goodSet d L) := by + have heq : goodSet d L = + ⋂ n : ℕ, {ω : SourceMode d → ℝ | orderAbsTotal n d L ω ≠ ∞} := by + ext ω + simp only [goodSet, Set.mem_setOf_eq, Set.mem_iInter, goodSample] + exact forall_congr' fun n => (orderAbsTotal_ne_top_iff n d L ω).symm + rw [heq] + apply MeasurableSet.iInter + intro n + convert ((orderAbsTotal_measurable n d L) (measurableSet_singleton ∞)).compl using 1 + ext ω + simp + +theorem goodSet_ae (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, ω ∈ goodSet d L := + goodSample_ae d hL + +theorem goodSet_measure_one (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + sourceLaw d (goodSet d L) = 1 := by + exact (mem_ae_iff_prob_eq_one (goodSet_measurable d L)).mp (goodSet_ae d hL) + +/-- A coefficient sample on the explicit all-order summability carrier. -/ +abbrev SmoothSample (d : ℕ) (L : ℝ) := ↥(goodSet d L) + +/-- Literal inclusion, retaining every coefficient of the original sample. -/ +def sampleInclusion (d : ℕ) (L : ℝ) : SmoothSample d L → (SourceMode d → ℝ) := + Subtype.val + +theorem sampleInclusion_measurable (d : ℕ) (L : ℝ) : + Measurable (sampleInclusion d L) := + measurable_subtype_coe + +/-- Pull back the original product law; no normalization or new law is chosen. -/ +def smoothLaw (d : ℕ) (L : ℝ) : Measure (SmoothSample d L) := + (sourceLaw d).comap (sampleInclusion d L) + +theorem sampleInclusion_map (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + (smoothLaw d L).map (sampleInclusion d L) = sourceLaw d := by + change ((sourceLaw d).comap ((↑) : SmoothSample d L → (SourceMode d → ℝ))).map + ((↑) : SmoothSample d L → (SourceMode d → ℝ)) = sourceLaw d + rw [map_comap_subtype_coe (goodSet_measurable d L), + Measure.restrict_eq_self_of_ae_mem (goodSet_ae d hL)] + +theorem sampleInclusion_measurePreserving (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + MeasurePreserving (sampleInclusion d L) (smoothLaw d L) (sourceLaw d) := + ⟨sampleInclusion_measurable d L, sampleInclusion_map d hL⟩ + +theorem smoothLaw_isProbabilityMeasure (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + IsProbabilityMeasure (smoothLaw d L) := by + apply (MeasurableEmbedding.subtype_coe (goodSet_measurable d L)).isProbabilityMeasure_comap + simpa only [Subtype.range_coe] using goodSet_ae d hL + +/-- Every measurable observation has exactly its original pushforward law. -/ +theorem observation_map_eq (d : ℕ) {L : ℝ} (hL : L ≠ 0) + {E : Type*} [MeasurableSpace E] (X : (SourceMode d → ℝ) → E) (hX : Measurable X) : + (smoothLaw d L).map (fun ω => X (sampleInclusion d L ω)) = (sourceLaw d).map X := by + change (smoothLaw d L).map (X ∘ sampleInclusion d L) = (sourceLaw d).map X + rw [← Measure.map_map hX (sampleInclusion_measurable d L), sampleInclusion_map d hL] + +theorem coordinate_marginal (d : ℕ) {L : ℝ} (hL : L ≠ 0) (m : SourceMode d) : + (smoothLaw d L).map (fun ω => sampleInclusion d L ω m) = gaussianReal 0 1 := by + rw [observation_map_eq d hL (fun ω => ω m) (measurable_pi_apply m)] + exact I4Foundation.coordinate_marginal m + +theorem finiteCoordinate_map_eq (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (n : ℕ) (m : Fin n → SourceMode d) : + (smoothLaw d L).map (fun ω j => sampleInclusion d L ω (m j)) = + (sourceLaw d).map (fun ω j => ω (m j)) := by + exact observation_map_eq d hL _ (Measurable.of_eval (fun j => measurable_pi_apply (m j))) + +/-- The unchanged literal real-cover field, evaluated on the carrier. -/ +def smoothSourceField (d : ℕ) (L : ℝ) (ω : SmoothSample d L) (x : Fin d → ℝ) : ℝ := + sourceField d L (sampleInclusion d L ω) x + +theorem smoothSourceField_contDiff (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SmoothSample d L) (n : ℕ) : ContDiff ℝ n (smoothSourceField d L ω) := + sourceField_smooth_of_goodSample d hL (sampleInclusion d L ω) ω.property n + +theorem smoothSourceField_smooth (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SmoothSample d L) : ContDiff ℝ ∞ (smoothSourceField d L ω) := + contDiff_infty.mpr (smoothSourceField_contDiff d hL ω) + +theorem smoothSourceField_finiteVector_map_eq (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (n : ℕ) (x : Fin n → (Fin d → ℝ)) : + (smoothLaw d L).map (fun ω j => smoothSourceField d L ω (x j)) = + (sourceLaw d).map (fun ω j => sourceField d L ω (x j)) := by + exact observation_map_eq d hL _ + (Measurable.of_eval (fun j => sourceField_eval_measurable d L (x j))) + +theorem smoothSourceField_finiteVector_hasGaussianLaw (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (n : ℕ) (x : Fin n → (Fin d → ℝ)) : + HasGaussianLaw (fun ω j => smoothSourceField d L ω (x j)) (smoothLaw d L) := by + have hm : Measurable (fun ω j => smoothSourceField d L ω (x j)) := + (Measurable.of_eval (fun j => sourceField_eval_measurable d L (x j))).comp + (sampleInclusion_measurable d L) + refine ⟨hm.aemeasurable, ?_⟩ + rw [smoothSourceField_finiteVector_map_eq d hL n x] + exact (source_finiteVector_hasGaussianLaw d hL n x).isGaussian_map + +theorem covariance_comp_inclusion (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (X Y : (SourceMode d → ℝ) → ℝ) (hX : Measurable X) (hY : Measurable Y) : + cov[fun ω => X (sampleInclusion d L ω), fun ω => Y (sampleInclusion d L ω); smoothLaw d L] = + cov[X, Y; sourceLaw d] := by + have h := covariance_map_fun (μ := smoothLaw d L) (Z := sampleInclusion d L) + (X := X) (Y := Y) hX.aestronglyMeasurable hY.aestronglyMeasurable + (sampleInclusion_measurable d L).aemeasurable + rw [sampleInclusion_map d hL] at h + exact h.symm + +theorem smoothSourceField_covariance (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (x y : Fin d → ℝ) : + cov[fun ω => smoothSourceField d L ω x, fun ω => smoothSourceField d L ω y; smoothLaw d L] = + sourceSpectralKernel d L (x - y) := by + calc + _ = cov[fun ω => sourceField d L ω x, fun ω => sourceField d L ω y; sourceLaw d] := + covariance_comp_inclusion d hL _ _ (sourceField_eval_measurable d L x) + (sourceField_eval_measurable d L y) + _ = _ := sourceField_covariance d hL x y + +/-- The unchanged literal torus descent of the same coefficient sample. -/ +def smoothTorusSourceField (d : ℕ) (L : ℝ) [Fact (0 < L)] + (ω : SmoothSample d L) (q : SourceTorus d L) : ℝ := + torusSourceField d L (sampleInclusion d L ω) q + +attribute [local instance] actualChartedSpace + +theorem smoothTorusSourceField_smooth (d : ℕ) (L : ℝ) [Fact (0 < L)] + (ω : SmoothSample d L) : + ContMDiff 𝓘(ℝ, Fin d → ℝ) 𝓘(ℝ) ∞ (smoothTorusSourceField d L ω) := by + let _ := torus_isManifold d L + have hs := smoothSourceField_smooth d (Fact.out : 0 < L).ne' ω + intro q + rw [contMDiffAt_iff_source] + have heq : smoothTorusSourceField d L ω ∘ (extChartAt 𝓘(ℝ, Fin d → ℝ) q).symm = + smoothSourceField d L ω := by + funext x + change torusSourceField d L (sampleInclusion d L ω) + ((quotientChart d L (chartCenter d L q)).symm x) = _ + rw [quotientChart_symm] + exact torusSourceField_pullback d L (sampleInclusion d L ω) x + rw [heq, contMDiffWithinAt_iff_contDiffWithinAt] + exact hs.contDiffAt.contDiffWithinAt + +theorem smoothTorusSourceField_finiteVector_hasGaussianLaw (d : ℕ) (L : ℝ) + [Fact (0 < L)] (n : ℕ) (q : Fin n → SourceTorus d L) : + HasGaussianLaw (fun ω j => smoothTorusSourceField d L ω (q j)) (smoothLaw d L) := by + have hm : Measurable (fun ω j => smoothTorusSourceField d L ω (q j)) := + (Measurable.of_eval (fun j => torusSourceField_eval_measurable d L (q j))).comp + (sampleInclusion_measurable d L) + refine ⟨hm.aemeasurable, ?_⟩ + change IsGaussian ((smoothLaw d L).map + (fun ω j => torusSourceField d L (sampleInclusion d L ω) (q j))) + rw [observation_map_eq d (Fact.out : 0 < L).ne' _ + (Measurable.of_eval (fun j => torusSourceField_eval_measurable d L (q j)))] + exact (torusSourceField_finiteVector_hasGaussianLaw d L n q).isGaussian_map + +theorem smoothTorusSourceField_covariance (d : ℕ) (L : ℝ) [Fact (0 < L)] + (q p : SourceTorus d L) : + cov[fun ω => smoothTorusSourceField d L ω q, fun ω => smoothTorusSourceField d L ω p; + smoothLaw d L] = + sourceSpectralKernel d L (torusRepresentative d L q - torusRepresentative d L p) := by + calc + _ = cov[fun ω => torusSourceField d L ω q, fun ω => torusSourceField d L ω p; sourceLaw d] := + covariance_comp_inclusion d (Fact.out : 0 < L).ne' _ _ + (torusSourceField_eval_measurable d L q) (torusSourceField_eval_measurable d L p) + _ = _ := torusSourceField_covariance d L q p + +end I4SmoothCarrier diff --git a/frontiers/source_smooth_realization_20261011/SourceSmoothControls.lean b/frontiers/source_smooth_realization_20261011/SourceSmoothControls.lean new file mode 100644 index 000000000..febe52a42 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceSmoothControls.lean @@ -0,0 +1,67 @@ +import SourceSmoothCarrier + +/-! Discriminating controls for the actual smooth-source construction. +These controls are proof obligations, not observed runtime outcomes. They require +orders above four, a common coefficient event, literal source inclusion and exact +law preservation. They make no conditional-law or theta-kernel claim. -/ + +noncomputable section +open I4Source I4Smooth I4SmoothCarrier I4Kernel MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal + +namespace I4SmoothControls + +/-- The old a.e. order-four theorem cannot fill the all-orders goal. -/ +theorem old_four_does_not_fill_all_orders (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + ∀ᵐ ω ∂sourceLaw d, ∀ n : ℕ, ContDiff ℝ n (sourceField d L ω) := by + fail_if_success exact I4C4.sourceField_contDiff_ae d hL + exact sourceField_smooth_ae d hL + +theorem represented_sample_order_five (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SmoothSample d L) : ContDiff ℝ 5 (smoothSourceField d L ω) := + smoothSourceField_contDiff d hL ω 5 + +theorem represented_sample_order_thirtyseven (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SmoothSample d L) : ContDiff ℝ 37 (smoothSourceField d L ω) := + smoothSourceField_contDiff d hL ω 37 + +/-- Both higher orders hold for every sample of the very same carrier. -/ +theorem one_carrier_for_both_orders (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SmoothSample d L) : + ContDiff ℝ 5 (smoothSourceField d L ω) ∧ + ContDiff ℝ 37 (smoothSourceField d L ω) := + ⟨represented_sample_order_five d hL ω, represented_sample_order_thirtyseven d hL ω⟩ + +theorem literal_field_everywhere (d : ℕ) (L : ℝ) (ω : SmoothSample d L) + (x : Fin d → ℝ) : + smoothSourceField d L ω x = sourceField d L (sampleInclusion d L ω) x := rfl + +theorem entire_coefficient_law_preserved (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + (smoothLaw d L).map (sampleInclusion d L) = sourceLaw d := + sampleInclusion_map d hL + +theorem arbitrary_observation_law_preserved (d : ℕ) {L : ℝ} (hL : L ≠ 0) + {E : Type*} [MeasurableSpace E] (X : (SourceMode d → ℝ) → E) (hX : Measurable X) : + (smoothLaw d L).map (fun ω => X (sampleInclusion d L ω)) = (sourceLaw d).map X := + observation_map_eq d hL X hX + +/-- Arbitrarily large changes on a finite block leave the actual carrier intact. -/ +theorem finite_block_changes_preserve_carrier (d : ℕ) (L : ℝ) + (ω η : SourceMode d → ℝ) (s : Finset (SourceMode d)) + (hωη : ∀ m ∉ s, ω m = η m) : + goodSample d L ω ↔ goodSample d L η := + goodSample_finite_change_iff d L ω η s hωη + +/-- The restricted field keeps variance one, which excludes a zero-field substitution. -/ +theorem field_variance_one (d : ℕ) {L : ℝ} (hL : L ≠ 0) (x : Fin d → ℝ) : + cov[fun ω => smoothSourceField d L ω x, + fun ω => smoothSourceField d L ω x; smoothLaw d L] = 1 := by + rw [smoothSourceField_covariance d hL x x, sub_self, spectralKernel_zero d hL] + +/-- The underlying restricted measure has total mass one, without conditioning +on a finite pin event or normalizing by a weight. -/ +theorem carrier_probability (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + IsProbabilityMeasure (smoothLaw d L) := + smoothLaw_isProbabilityMeasure d hL + +end I4SmoothControls diff --git a/frontiers/source_smooth_realization_20261011/SourceTorus.lean b/frontiers/source_smooth_realization_20261011/SourceTorus.lean new file mode 100644 index 000000000..b9fe49752 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceTorus.lean @@ -0,0 +1,111 @@ +import SourceCovariance +import Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic +import Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic + +/-! Literal descent of the existing real-cover field to a product of additive circles. +The sample law remains sourceLaw. Smooth torus and Banach-valued laws are separate. -/ +noncomputable section +open I4Foundation I4Weights I4Source I4Lattice I4Kernel I4SourceGaussian I4SourceCovariance +open MeasureTheory ProbabilityTheory +open scoped BigOperators ENNReal NNReal + +namespace I4Torus + +abbrev SourceTorus (d : ℕ) (L : ℝ) := Fin d → AddCircle L + +def torusProjection (d : ℕ) (L : ℝ) (x : Fin d → ℝ) : SourceTorus d L := + fun i => (x i : AddCircle L) + +def torusRepresentative (d : ℕ) (L : ℝ) [Fact (0 < L)] + (q : SourceTorus d L) : Fin d → ℝ := + fun i => (AddCircle.equivIco L 0 (q i)).1 + +def torusSourceField (d : ℕ) (L : ℝ) [Fact (0 < L)] + (ω : SourceMode d → ℝ) (q : SourceTorus d L) : ℝ := + sourceField d L ω (torusRepresentative d L q) + +theorem torusProjection_measurable (d : ℕ) (L : ℝ) : Measurable (torusProjection d L) := by + exact Measurable.of_eval (fun i => AddCircle.measurable_mk'.comp (measurable_pi_apply i)) + +theorem torusRepresentative_measurable (d : ℕ) (L : ℝ) [Fact (0 < L)] : + Measurable (torusRepresentative d L) := by + exact Measurable.of_eval (fun i => measurable_subtype_coe.comp + ((AddCircle.measurableEquivIco L 0).measurable.comp (measurable_pi_apply i))) + +theorem torusProjection_representative (d : ℕ) (L : ℝ) [Fact (0 < L)] + (q : SourceTorus d L) : torusProjection d L (torusRepresentative d L q) = q := by + funext i + exact AddCircle.coe_equivIco (p := L) (a := 0) (y := q i) + +theorem sourceField_eq_of_torusProjection_eq (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (ω : SourceMode d → ℝ) (x y : Fin d → ℝ) + (h : torusProjection d L x = torusProjection d L y) : + sourceField d L ω x = sourceField d L ω y := by + classical + have hz (i : Fin d) : ∃ n : ℤ, n • L = y i - x i := by + apply (AddCircle.coe_eq_zero_iff (p := L)).mp + rw [AddCircle.coe_sub] + exact sub_eq_zero.mpr (congrFun h i).symm + choose n hn using hz + have he : y = fun i => x i + L * (n i : ℝ) := by + funext i + have hi := hn i + rw [zsmul_eq_mul] at hi + linarith + rw [he] + exact (sourceField_lattice_shift d hL ω n x).symm + +theorem torusSourceField_pullback (d : ℕ) (L : ℝ) [Fact (0 < L)] + (ω : SourceMode d → ℝ) (x : Fin d → ℝ) : + torusSourceField d L ω (torusProjection d L x) = sourceField d L ω x := by + exact sourceField_eq_of_torusProjection_eq d (Fact.out : 0 < L).ne' ω + (torusRepresentative d L (torusProjection d L x)) x + (torusProjection_representative d L (torusProjection d L x)) + +theorem torusSourceField_eval_measurable (d : ℕ) (L : ℝ) [Fact (0 < L)] + (q : SourceTorus d L) : Measurable (fun ω => torusSourceField d L ω q) := by + exact sourceField_eval_measurable d L (torusRepresentative d L q) + +theorem torusSourceField_joint_measurable (d : ℕ) (L : ℝ) [Fact (0 < L)] : + Measurable (fun p : (SourceMode d → ℝ) × SourceTorus d L => + torusSourceField d L p.1 p.2) := by + unfold torusSourceField sourceField scalarSeries + apply Measurable.tsum + intro m + have hm : Continuous (fun x : Fin d → ℝ => modeCoefficient d L m x) := by + cases m with + | none => simp only [modeCoefficient]; fun_prop + | some p => + rcases p with ⟨k,b⟩ + cases b <;> simp only [modeCoefficient, Bool.false_eq_true, ite_false, ite_true] <;> + unfold phase <;> fun_prop + exact (hm.measurable.comp ((torusRepresentative_measurable d L).comp measurable_snd)).mul + ((measurable_pi_apply m).comp measurable_fst) + +theorem torusSourceField_finiteVector_hasGaussianLaw (d : ℕ) (L : ℝ) [Fact (0 < L)] + (n : ℕ) (q : Fin n → SourceTorus d L) : + HasGaussianLaw (fun ω j => torusSourceField d L ω (q j)) (sourceLaw d) := by + exact source_finiteVector_hasGaussianLaw d (Fact.out : 0 < L).ne' n + (fun j => torusRepresentative d L (q j)) + +theorem torusSourceField_isGaussianProcess (d : ℕ) (L : ℝ) [Fact (0 < L)] : + IsGaussianProcess (fun q ω => torusSourceField d L ω q) (sourceLaw d) := by + exact (sourceField_isGaussianProcess d (Fact.out : 0 < L).ne').comp_right + (torusRepresentative d L) + +theorem torusSourceField_covariance (d : ℕ) (L : ℝ) [Fact (0 < L)] + (q p : SourceTorus d L) : + cov[fun ω => torusSourceField d L ω q, fun ω => torusSourceField d L ω p; sourceLaw d] = + sourceSpectralKernel d L (torusRepresentative d L q - torusRepresentative d L p) := by + exact sourceField_covariance d (Fact.out : 0 < L).ne' + (torusRepresentative d L q) (torusRepresentative d L p) + +theorem torusSourceField_covariance_pullback (d : ℕ) (L : ℝ) [Fact (0 < L)] + (x y : Fin d → ℝ) : + cov[fun ω => torusSourceField d L ω (torusProjection d L x), + fun ω => torusSourceField d L ω (torusProjection d L y); sourceLaw d] = + sourceSpectralKernel d L (x - y) := by + simp_rw [torusSourceField_pullback] + exact sourceField_covariance d (Fact.out : 0 < L).ne' x y + +end I4Torus diff --git a/frontiers/source_smooth_realization_20261011/SourceTorusC4.lean b/frontiers/source_smooth_realization_20261011/SourceTorusC4.lean new file mode 100644 index 000000000..30cfb670f --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceTorusC4.lean @@ -0,0 +1,134 @@ +import SourceC4 +import SourceTorus +import Mathlib.Topology.OpenPartialHomeomorph.Constructions +import Mathlib.Geometry.Manifold.ContMDiff.Basic +import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace +import Mathlib.Topology.LocallyConstant.Basic + +noncomputable section +open I4Foundation I4Weights I4Source I4C4 I4Torus MeasureTheory +open scoped Manifold ContDiff Topology +namespace I4TorusC4 + +def quotientChart (d : ℕ) (L : ℝ) [Fact (0 < L)] (a : Fin d → ℝ) : + OpenPartialHomeomorph (SourceTorus d L) (Fin d → ℝ) := + (OpenPartialHomeomorph.pi (fun i : Fin d => AddCircle.openPartialHomeomorphCoe L (a i))).symm + +def chartCenter (d : ℕ) (L : ℝ) [Fact (0 < L)] (q : SourceTorus d L) : Fin d → ℝ := + fun i => torusRepresentative d L q i - L / 2 + +theorem quotientChart_symm (d : ℕ) (L : ℝ) [Fact (0 < L)] (a : Fin d → ℝ) : + (quotientChart d L a).symm = torusProjection d L := by + rfl + +theorem centered_chart_covers (d : ℕ) (L : ℝ) [Fact (0 < L)] (q : SourceTorus d L) : + q ∈ (quotientChart d L (chartCenter d L q)).source := by + let e := OpenPartialHomeomorph.pi + (fun i : Fin d => AddCircle.openPartialHomeomorphCoe L (chartCenter d L q i)) + have hs : torusRepresentative d L q ∈ e.source := by + change torusRepresentative d L q ∈ Set.pi Set.univ + (fun i => Set.Ioo (chartCenter d L q i) (chartCenter d L q i + L)) + intro i _ + change chartCenter d L q i < torusRepresentative d L q i ∧ + torusRepresentative d L q i < chartCenter d L q i + L + have hL : 0 < L := Fact.out + dsimp [chartCenter] + constructor <;> linarith + have he : e (torusRepresentative d L q) = q := + torusProjection_representative d L q + have ht := e.map_source hs + rw [he] at ht + exact ht + +@[instance_reducible] def actualChartedSpace (d : ℕ) (L : ℝ) [Fact (0 < L)] : + ChartedSpace (Fin d → ℝ) (SourceTorus d L) where + atlas := Set.range (quotientChart d L) + chartAt := fun q => quotientChart d L (chartCenter d L q) + mem_chart_source := centered_chart_covers d L + chart_mem_atlas := fun q => ⟨chartCenter d L q, rfl⟩ + +attribute [local instance] actualChartedSpace + +theorem chart_transition_contDiff (d : ℕ) (L : ℝ) [Fact (0 < L)] (a b : Fin d → ℝ) : + ContDiffOn ℝ ∞ ((quotientChart d L a).symm.trans (quotientChart d L b)) + ((quotientChart d L a).symm.trans (quotientChart d L b)).source := by + let ea := quotientChart d L a + let eb := quotientChart d L b + let T := ea.symm.trans eb + let S := T.source + have hproj (x : S) : torusProjection d L (T x) = torusProjection d L x := by + have hb : ea.symm (x : Fin d → ℝ) ∈ eb.source := x.property.2 + have hi := eb.left_inv hb + simpa only [T, ea, eb, OpenPartialHomeomorph.trans_apply, quotientChart_symm] using hi + have hlat (x : S) (i : Fin d) : T x i - (x : Fin d → ℝ) i ∈ + AddSubgroup.zmultiples L := by + apply AddSubgroup.mem_zmultiples_iff.mpr + apply (AddCircle.coe_eq_zero_iff (p := L)).mp + rw [AddCircle.coe_sub] + exact sub_eq_zero.mpr (congrFun (hproj x) i) + let delta : S → Fin d → AddSubgroup.zmultiples L := + fun x i => ⟨T x i - (x : Fin d → ℝ) i, hlat x i⟩ + have hd : Continuous delta := by + apply continuous_pi + intro i + apply Continuous.subtype_mk + exact ((continuous_apply i).comp T.continuousOn.domRestrict).sub + ((continuous_apply i).comp continuous_subtype_val) + have hlc : IsLocallyConstant delta := + (IsLocallyConstant.iff_continuous delta).mpr hd + apply T.open_source.contDiffOn_iff.mpr + intro x hx + let x0 : S := ⟨x, hx⟩ + let c : Fin d → ℝ := fun i => (delta x0 i : ℝ) + have hsub : ∀ᶠ y : S in 𝓝 x0, T y = (y : Fin d → ℝ) + c := by + filter_upwards [hlc.eventually_eq x0] with y hy + funext i + have hi := congrArg (fun z : Fin d → AddSubgroup.zmultiples L => (z i : ℝ)) hy + change T y i - (y : Fin d → ℝ) i = c i at hi + change T y i = (y : Fin d → ℝ) i + c i + linarith + have hamb : (fun y => T y) =ᶠ[𝓝 x] (fun y => y + c) := by + have hm : ∀ᶠ y in Filter.map ((↑) : S → (Fin d → ℝ)) (𝓝 x0), T y = y + c := + Filter.eventually_map.mpr hsub + have hmap : Filter.map ((↑) : S → (Fin d → ℝ)) (𝓝 x0) = 𝓝 x := + map_nhds_subtype_coe_eq_nhds hx (T.open_source.mem_nhds hx) + rw [hmap] at hm + exact hm + exact (contDiff_id.add contDiff_const).contDiffAt.congr_of_eventuallyEq hamb + +theorem torus_isManifold (d : ℕ) (L : ℝ) [Fact (0 < L)] : + IsManifold 𝓘(ℝ, Fin d → ℝ) ∞ (SourceTorus d L) := by + apply isManifold_of_contDiffOn + intro e e' he he' + change e ∈ Set.range (quotientChart d L) at he + change e' ∈ Set.range (quotientChart d L) at he' + rcases he with ⟨a, rfl⟩ + rcases he' with ⟨b, rfl⟩ + simpa only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm, + Function.comp_id, Function.id_comp, Set.preimage_id, Set.range_id, Set.inter_univ] using + chart_transition_contDiff d L a b + +theorem torusSourceField_contMDiff_ae (d : ℕ) (L : ℝ) [Fact (0 < L)] : + ∀ᵐ sample ∂sourceLaw d, + ContMDiff 𝓘(ℝ, Fin d → ℝ) 𝓘(ℝ) 4 (torusSourceField d L sample) := by + let _ := torus_isManifold d L + filter_upwards [sourceField_contDiff_ae d (Fact.out : 0 < L).ne'] with sample hs + intro q + rw [contMDiffAt_iff_source] + have heq : torusSourceField d L sample ∘ (extChartAt 𝓘(ℝ, Fin d → ℝ) q).symm = + sourceField d L sample := by + funext x + change torusSourceField d L sample ((quotientChart d L (chartCenter d L q)).symm x) = _ + rw [quotientChart_symm] + exact torusSourceField_pullback d L sample x + rw [heq, contMDiffWithinAt_iff_contDiffWithinAt] + exact hs.contDiffAt.contDiffWithinAt + +theorem torusSourceField_weakSuperlevel_closed_ae (d : ℕ) (L : ℝ) [Fact (0 < L)] : + ∀ᵐ sample ∂sourceLaw d, ∀ h : ℝ, + IsClosed {q : SourceTorus d L | h ≤ torusSourceField d L sample q} := by + filter_upwards [torusSourceField_contMDiff_ae d L] with sample hs + intro h + exact isClosed_Ici.preimage hs.continuous + +end I4TorusC4 diff --git a/frontiers/source_smooth_realization_20261011/SpectralWeights.lean b/frontiers/source_smooth_realization_20261011/SpectralWeights.lean new file mode 100644 index 000000000..191a22f14 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SpectralWeights.lean @@ -0,0 +1,160 @@ +import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable +import Mathlib.Analysis.Normed.Ring.InfiniteSum +import Mathlib.Data.Fin.Tuple.Basic +import Mathlib.Algebra.BigOperators.Fin + +/-! Concrete square-root Gaussian spectral majorants for the required I4 bridge. +The product majorant dominates the l1 frequency norm for the default Pi sup norm. +This file alone proves neither a Gaussian field law nor sample smoothness. -/ + +noncomputable section +open Real +open scoped BigOperators +namespace I4Weights + +def decay (a : ℝ) (k : ℤ) : ℝ := exp (-a * (k : ℝ) ^ 2) +def coordinateBound (a c : ℝ) (k : ℤ) : ℝ := + decay a k * (1 + |c * (k : ℝ)|) ^ 4 +def productDecay (d : ℕ) (a : ℝ) (k : Fin d → ℤ) : ℝ := + ∏ i, decay a (k i) +def productBound (d : ℕ) (a c : ℝ) (k : Fin d → ℤ) : ℝ := + ∏ i, coordinateBound a c (k i) +def sourceA (L : ℝ) : ℝ := π ^ 2 / L ^ 2 +def sourceC (L : ℝ) : ℝ := 2 * π / L +def sourceWeight (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : ℝ := + productDecay d (2 * sourceA L) k +def sourceZ (d : ℕ) (L : ℝ) : ℝ := ∑' k, sourceWeight d L k +def pairedBound (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : ℝ := + Real.sqrt (2 / sourceZ d L) * productBound d (sourceA L) (sourceC L) k + +theorem summable_decay_pow {a : ℝ} (ha : 0 < a) (n : ℕ) : + Summable (fun k : ℤ => decay a k * |(k : ℝ)| ^ n) := by + have hb := summable_pow_mul_jacobiTheta₂_term_bound 0 + (show 0 < a / π by positivity) n + have he (k : ℤ) : -π * (a / π * (k : ℝ) ^ 2 - 2 * 0 * |(k : ℝ)|) = + -a * (k : ℝ) ^ 2 := by + field_simp + ring + simp_rw [Int.cast_abs, he] at hb + simpa [decay, mul_comm] using hb + +theorem coordinateBound_summable {a c : ℝ} (ha : 0 < a) : + Summable (coordinateBound a c) := by + have hs := summable_decay_pow ha + convert ((((hs 0).add ((hs 1).mul_left (4 * |c|))).add + ((hs 2).mul_left (6 * |c| ^ 2))).add + ((hs 3).mul_left (4 * |c| ^ 3))).add ((hs 4).mul_left (|c| ^ 4)) using 1 + funext k + simp only [coordinateBound, abs_mul] + ring + +set_option maxHeartbeats 800000 in +theorem finite_product_summable {f : ℤ → ℝ} (hf : Summable f) (hn : ∀ k, 0 ≤ f k) + (d : ℕ) : Summable (fun k : Fin d → ℤ => ∏ i, f (k i)) := by + classical + induction d with + | zero => exact (hasSum_fintype _).summable + | succ d ih => + have hp : Summable (fun p : ℤ × (Fin d → ℤ) => f p.1 * ∏ i, f (p.2 i)) := + Summable.mul_of_nonneg (ι := ℤ) (ι' := Fin d → ℤ) + (f := f) (g := fun k : Fin d → ℤ => ∏ i, f (k i)) + hf ih hn (fun k => Finset.prod_nonneg (fun i _ => hn (k i))) + have heq : + ((fun k : Fin (d + 1) → ℤ => ∏ i, f (k i)) ∘ + (Fin.consEquiv (fun _ : Fin (d + 1) => ℤ))) = + (fun p : ℤ × (Fin d → ℤ) => f p.1 * ∏ i, f (p.2 i)) := by + funext p + simp only [Function.comp_apply, Fin.consEquiv_apply, Fin.prod_univ_succ, + Fin.cons_zero, Fin.cons_succ] + apply (Fin.consEquiv (fun _ : Fin (d + 1) => ℤ)).summable_iff.mp + rw [heq] + exact hp + +theorem productBound_summable {a c : ℝ} (ha : 0 < a) (d : ℕ) : + Summable (productBound d a c) := by + exact finite_product_summable (coordinateBound_summable ha) + (fun k => by unfold coordinateBound decay; positivity) d + +theorem productDecay_eq_exp (d : ℕ) (a : ℝ) (k : Fin d → ℤ) : + productDecay d a k = exp (-a * ∑ i, (k i : ℝ) ^ 2) := by + unfold productDecay decay + rw [← Real.exp_sum, ← Finset.mul_sum] + +theorem frequency_l1_le_product (d : ℕ) (v : Fin d → ℝ) (hv : ∀ i, 0 ≤ v i) : + 1 + ∑ i, v i ≤ ∏ i, (1 + v i) := by + classical + have H (s : Finset (Fin d)) : 1 + ∑ i ∈ s, v i ≤ ∏ i ∈ s, (1 + v i) := by + induction s using Finset.induction_on with + | empty => simp + | @insert i s hi ih => + rw [Finset.sum_insert hi, Finset.prod_insert hi] + have hsum : 0 ≤ ∑ j ∈ s, v j := Finset.sum_nonneg (fun j _ => hv j) + calc + 1 + (v i + ∑ j ∈ s, v j) ≤ (1 + v i) * (1 + ∑ j ∈ s, v j) := by + nlinarith [mul_nonneg (hv i) hsum] + _ ≤ (1 + v i) * ∏ j ∈ s, (1 + v j) := + mul_le_mul_of_nonneg_left ih (by linarith [hv i]) + exact H Finset.univ + +theorem sourceA_pos {L : ℝ} (hL : L ≠ 0) : 0 < sourceA L := by + unfold sourceA + positivity + +theorem sourceWeight_eq_physical (d : ℕ) (L : ℝ) (k : Fin d → ℤ) : + sourceWeight d L k = exp (-(∑ i, (sourceC L * (k i : ℝ)) ^ 2) / 2) := by + have hc : sourceC L ^ 2 = 4 * sourceA L := by + unfold sourceC sourceA + ring + have hs : (∑ i, (sourceC L * (k i : ℝ)) ^ 2) = + 4 * sourceA L * ∑ i, (k i : ℝ) ^ 2 := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro i _ + rw [mul_pow, hc] + rw [sourceWeight, productDecay_eq_exp, hs] + congr 1 + ring + +theorem sourceWeight_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + Summable (sourceWeight d L) := by + have ha : 0 < 2 * sourceA L := mul_pos (by norm_num) (sourceA_pos hL) + have hs : Summable (decay (2 * sourceA L)) := by + simpa using summable_decay_pow ha 0 + exact finite_product_summable hs (fun k => (Real.exp_pos _).le) d + +theorem sourceZ_pos (d : ℕ) {L : ℝ} (hL : L ≠ 0) : 0 < sourceZ d L := by + apply (sourceWeight_summable d hL).tsum_pos + (fun k => by unfold sourceWeight productDecay decay; positivity) (fun _ => 0) + simp [sourceWeight, productDecay, decay] + +theorem pairedBound_eq_amplitude (d : ℕ) {L : ℝ} (hL : L ≠ 0) (k : Fin d → ℤ) : + pairedBound d L k = Real.sqrt (2 * sourceWeight d L k / sourceZ d L) * + ∏ i, (1 + |sourceC L * (k i : ℝ)|) ^ 4 := by + have hsqrt : Real.sqrt (sourceWeight d L k) = productDecay d (sourceA L) k := by + have hw : sourceWeight d L k = (productDecay d (sourceA L) k) ^ 2 := by + rw [sourceWeight, productDecay_eq_exp, productDecay_eq_exp, pow_two, ← Real.exp_add] + congr 1 + ring + rw [hw, Real.sqrt_sq_eq_abs, abs_of_nonneg] + unfold productDecay decay + positivity + have hamp : Real.sqrt (2 * sourceWeight d L k / sourceZ d L) = + Real.sqrt (2 / sourceZ d L) * productDecay d (sourceA L) k := by + have he : 2 * sourceWeight d L k / sourceZ d L = + (2 / sourceZ d L) * sourceWeight d L k := by ring + rw [he, Real.sqrt_mul (by have := sourceZ_pos d hL; positivity), hsqrt] + have hp : productBound d (sourceA L) (sourceC L) k = + productDecay d (sourceA L) k * ∏ i, (1 + |sourceC L * (k i : ℝ)|) ^ 4 := by + exact Finset.prod_mul_distrib + rw [pairedBound, hp, hamp] + ring + +theorem pairedBound_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) : + Summable (pairedBound d L) := by + exact (productBound_summable (sourceA_pos hL) d).mul_left _ + +theorem pairedBound_subtype_summable (d : ℕ) {L : ℝ} (hL : L ≠ 0) + (S : Set (Fin d → ℤ)) : Summable (fun k : S => pairedBound d L k) := by + exact (pairedBound_summable d hL).subtype S + +end I4Weights diff --git a/frontiers/source_smooth_realization_20261011/lake-manifest.json b/frontiers/source_smooth_realization_20261011/lake-manifest.json new file mode 100644 index 000000000..9fe133235 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/lake-manifest.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "name": "plausible", + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "LeanSearchClient", + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "importGraph", + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e928b72544873815af278d38681b31c0293588e3", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "proofwidgets", + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "name": "aesop", + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Qq", + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "batteries", + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Cli", + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "mathlib", + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "manifestFile": "lake-manifest.json", + "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "inherited": false, + "configFile": "lakefile.lean" + } + ], + "name": "source_smooth_realization", + "lakeDir": ".lake", + "fixedToolchain": true +} diff --git a/frontiers/source_smooth_realization_20261011/lakefile.toml b/frontiers/source_smooth_realization_20261011/lakefile.toml new file mode 100644 index 000000000..695cbbf56 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/lakefile.toml @@ -0,0 +1,47 @@ +name = "source_smooth_realization" +version = "0.1.0" +defaultTargets = ["SourceSmoothControls"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "d13f23b723b8a846827a245b89c10fc7d3f11612" + +[[lean_lib]] +name = "GaussianSeriesFoundation" + +[[lean_lib]] +name = "SourceC4" + +[[lean_lib]] +name = "SourceCovariance" + +[[lean_lib]] +name = "SourceFourierSeries" + +[[lean_lib]] +name = "SourceGaussianLaw" + +[[lean_lib]] +name = "SourceKernel" + +[[lean_lib]] +name = "SourceLattice" + +[[lean_lib]] +name = "SourceTorus" + +[[lean_lib]] +name = "SourceTorusC4" + +[[lean_lib]] +name = "SpectralWeights" + +[[lean_lib]] +name = "SourceSmooth" + +[[lean_lib]] +name = "SourceSmoothCarrier" + +[[lean_lib]] +name = "SourceSmoothControls" diff --git a/frontiers/source_smooth_realization_20261011/lean-toolchain b/frontiers/source_smooth_realization_20261011/lean-toolchain new file mode 100644 index 000000000..ba8ebf2db --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1