From 6723c0fcabec105cfd47d2959e459ac865eff248 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Thu, 15 Oct 2026 20:57:56 -0500 Subject: [PATCH] Publish the source-bound smooth carrier successor on current Math main Preserve all nineteen exact locally qualified source payloads and nine dependency pins. Add the source manifest, checksum closure and original-opened qualification workflow with a fresh externally bound admission contract. Source owner and adopter: OpenAI Codex ROOT01a11cbf. Complete two-file repair advisory: Anthropic Claude 01Cz, Math451 comment6154293277. Existing source, term, result and freeze reviews retain their actual scoped lineages. This candidate has no runtime admission until the exact external declaration is published and fully read back before triggering branch or PR creation. No original451 source, failed run, workflow guard or scientific status changes. --- .../workflows/source-smooth-realization.yml | 579 ++++++++++++++++++ .../.gitignore | 1 + .../DESIGN.md | 54 ++ .../GaussianSeriesFoundation.lean | 96 +++ .../SOURCE_MANIFEST.json | 300 +++++++++ .../SOURCE_SHA256SUMS | 20 + .../SourceC4.lean | 141 +++++ .../SourceCovariance.lean | 74 +++ .../SourceFourierSeries.lean | 147 +++++ .../SourceGaussianLaw.lean | 189 ++++++ .../SourceKernel.lean | 112 ++++ .../SourceLattice.lean | 159 +++++ .../SourceSmooth.lean | 254 ++++++++ .../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, 3061 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..ecc9d40d9 --- /dev/null +++ b/.github/workflows/source-smooth-realization.yml @@ -0,0 +1,579 @@ +# Prospective C261A successor candidate; no runtime admission until exact external declaration/readback. +# Actual source pickup: Math451/6206234169; UUID294fee4a-0d27-4345-aa55-a94158531285. +# SOURCE_GUARD_UTC=2026-10-16T02:50:00Z +# DOCUMENTARY_TARGET_UTC=2026-10-16T03:35:00Z +# LEASE_UNTIL_UTC=2026-10-16T03:45:00Z +# Complete final workflow/resource/source review and immutable head/tree/parent bindings precede ref/PR creation. +# Manifest state describes the mandatory prepublication contract; this file cannot establish its own external admission. +# Original run38400993873/attempt1 remains FAILED; old guards/PR/event/run remain historical. +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: + # Only the exact externally declared original opened/attempt1 route is eligible. + runs-on: ubuntu-latest + timeout-minutes: 30 + env: + LEAN_NUM_THREADS: '2' + ADMISSION_STATE: 'DECLARED_BEFORE_REF_OR_PR_PUBLICATION' + CLAIM_UUID: '294fee4a-0d27-4345-aa55-a94158531285' + SOURCE_GUARD_UTC: '2026-10-16T02:50:00Z' + EXPECTED_HEAD_REF: 'codex/c261a-hosted-successor-20261016-root01a11cbf' + HISTORICAL_MANIFEST_CLAIM_UUID: 'e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6' + EXPECTED_SOURCE_LIST_SHA256: '1c8b5045a5260e5da03c5da6042d6c92681e26f05935f13f362084fe3d1572a6' + EXPECTED_SOURCE_MANIFEST_SHA256: 'd3fe096b830c4c5bf2fff47a2a2aa528ae2a79d4cb9816afb6be536685d8d9ca' + EXPECTED_BASE_SHA: '319f9c45f66dbcce4a71b9c2f3e0fb62a666bfec' + EXPECTED_BASE_TREE: '78300962726873d85d5682a7be7d6beb7aebe63e' + EXPECTED_BASE_REF: 'main' + 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=EXTERNAL_RECORD_REQUIRED_NOT_ESTABLISHED_BY_WORKFLOW\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 "$ADMISSION_STATE" = DECLARED_BEFORE_REF_OR_PR_PUBLICATION + [[ "$CLAIM_UUID" =~ ^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$ ]] + 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=EXTERNAL_RECORD_REQUIRED_NOT_ESTABLISHED_BY_WORKFLOW\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 "$ADMISSION_STATE" = DECLARED_BEFORE_REF_OR_PR_PUBLICATION + [[ "$CLAIM_UUID" =~ ^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$ ]] + 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 --arg claim "$CLAIM_UUID" --arg base "$EXPECTED_BASE_SHA" --arg tree "$EXPECTED_BASE_TREE" ' .package == "frontiers/source_smooth_realization_20261011" and .state == "DECLARED_BEFORE_REF_OR_PR_PUBLICATION" and .source_claim.uuid == $claim and .parent.commit == $base and .parent.tree == $tree and (.files | length) == 19 and ([.files[].bytes] | add) == 97004 ' 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 + # Preserve the complete current base: exactly 21 package leaves and this workflow may be added. + repo_root=$(git rev-parse --show-toplevel) + { sed 's|^|frontiers/source_smooth_realization_20261011/|' .lake/evidence/package-members-required.txt; printf '%s\n' .github/workflows/source-smooth-realization.yml; } | LC_ALL=C sort > .lake/evidence/publication-paths-required.txt + git -C "$repo_root" diff --name-only "$EXPECTED_BASE_SHA" HEAD^2 | LC_ALL=C sort > .lake/evidence/publication-paths-actual.txt + cmp -s .lake/evidence/publication-paths-required.txt .lake/evidence/publication-paths-actual.txt + test "$(wc -l < .lake/evidence/publication-paths-actual.txt)" -eq 22 + git -C "$repo_root" diff --name-status "$EXPECTED_BASE_SHA" HEAD^2 > .lake/evidence/publication-statuses.txt + if grep -Evq '^A[[:space:]]' .lake/evidence/publication-statuses.txt; then exit 83; fi + while IFS= read -r file; do + test "$(git -C "$repo_root" ls-tree HEAD^2 -- "$file" | awk '{ print $1 }')" = 100644 + done < .lake/evidence/publication-paths-required.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..806775117 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SOURCE_MANIFEST.json @@ -0,0 +1,300 @@ +{ + "schema_version": 2, + "package": "frontiers/source_smooth_realization_20261011", + "state": "DECLARED_BEFORE_REF_OR_PR_PUBLICATION", + "source_claim": { + "uuid": "294fee4a-0d27-4345-aa55-a94158531285", + "native": "https://github.com/d6g8k5htny-coder/Math-/pull/451#issuecomment-6206234169", + "state": "ACTIVE_NATIVE_SOURCE_PICKUP" + }, + "parent": { + "commit": "319f9c45f66dbcce4a71b9c2f3e0fb62a666bfec", + "tree": "78300962726873d85d5682a7be7d6beb7aebe63e", + "ref": "main", + "as_of_only": true + }, + "source_origin": { + "local_repair_commit": "c28666182c5fae5b6a8d4d3aff4f5cf9f66c612f", + "local_repair_tree": "7c48b60a43803ad91794a9866c40d6a5eabc8c5f", + "ordered_parents": [ + "1f38a851595bc0664b543aeb59b462817ca3b8f9" + ], + "execution_cut": "original1f38a851 plus bound dirty repair; local freeze committed after execution", + "local_results_sha256": "3a39eedafb4cab590f6a19b8e9aa9ee30469397d9f790d03b17c583753785550", + "delivery_zip_sha256": "d82c239ad958a4607583f55d75415846b56ba4298cdac079856f96024633df30", + "native_delivery": "https://github.com/d6g8k5htny-coder/Math-/pull/451#issuecomment-6205560350", + "custody_correction": { + "original_recovery_zip_unchanged": true, + "original_zip_omitted_two_aggregate_receipts": true, + "owner_private_envelope_sha256": "554d73201a464abfa80631de67de76797b10ffbd4eb9a2288f88bd8660234f99", + "native_report": "https://github.com/d6g8k5htny-coder/Math-/pull/451#issuecomment-6205742935", + "metadata_correction": "https://github.com/d6g8k5htny-coder/Math-/pull/451#issuecomment-6206039747", + "results_sha256": "3a39eedafb4cab590f6a19b8e9aa9ee30469397d9f790d03b17c583753785550", + "candidate_ready_binding_sha256": "9a6eb9a3202d4dab7a98d7174ee468ba08ef7e375c5876c49b291dbe9bc66570", + "root_current_raw_private_envelope_reacquisition": "NOT_PERFORMED; public native custody report consumed" + } + }, + "historical_genesis": { + "source_claim_uuid": "e2f875ef-55a0-46d5-b85d-9b94cb6bc6c6", + "source_manifest_sha256": "56acfdbf20fd7645872f2ce3a60beb1186908dc4f7994d14b175ddc93106b65d", + "source_list_sha256": "0d78987b8baa27ce0917e126945ccff0261af74b3461722ae4f4768f62fb78eb", + "hosted_run": 38400993873, + "attempt": 1, + "result": "FAILURE", + "provenance_only": 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": 11336, + "sha256": "12ad7263267a970bd5d5c95d7c7aa62d9c971f7beebf28f1aa7ed16d3a112f1b", + "git_blob_sha1": "5b1518449d51aec024e17c442c5be5526838101b", + "role": "SOURCE_PAYLOAD_WITH_LOCAL_FORMAL_EVIDENCE", + "historical_genesis_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": 11222, + "sha256": "5defdf223e85e7ccd23b5a903a1a306fe7f723727eb6aabf62eef523ef8639ed", + "git_blob_sha1": "cb6f7b10881246f5e1fab530c58df3036f44279e", + "role": "SOURCE_PAYLOAD_WITH_LOCAL_FORMAL_EVIDENCE", + "historical_genesis_role": "NEW_UNCOMPILED_MATHEMATICAL_SOURCE" + }, + { + "path": "SourceSmoothControls.lean", + "bytes": 3257, + "sha256": "8eca5ecdb5e2a0c1cb786468b340e4516df653468f958e535f156baafef088b4", + "git_blob_sha1": "febe52a42d099844d02c59b728ca86417587b3e2", + "role": "SOURCE_PAYLOAD_WITH_LOCAL_FORMAL_EVIDENCE", + "historical_genesis_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" + } + ], + "payload_bytes": 97004, + "local_verification": "PASS at exact stated local scope; no hosted successor qualification", + "hosted_verification": "NOT_RUN", + "scientific_effect": "NONE", + "publication_contract": "Prospective frozen source candidate; matching exact external DECLARED admission must be published and fully read back before any triggering ref or PR exists. This manifest alone grants no runtime admission." +} diff --git a/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS b/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS new file mode 100644 index 000000000..b991528fe --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SOURCE_SHA256SUMS @@ -0,0 +1,20 @@ +fde850d24186b6e99c8c0debd641fb3ab85198b109eb66f71a1fea02bd6ea1b3 .gitignore +18f486b9a1e94d449ab078fccdb5bfaec7bad0075c3a8e8d26f96775b68e10f7 DESIGN.md +feea566d5aeba58459bd4a1f20f070bdcd80ee30712817324cdd594e3e232c95 GaussianSeriesFoundation.lean +d3fe096b830c4c5bf2fff47a2a2aa528ae2a79d4cb9816afb6be536685d8d9ca SOURCE_MANIFEST.json +b15e53b825c2e2d6af2af18182da227d8794dddcc3e1b29611a913f89a889397 SourceC4.lean +30560009582659a100637b5510c657cf1fa762f68a37bae8fab42c1eeee6aee5 SourceCovariance.lean +5f145e8e8693bfe4d1554092c8258dbda4f17f8e078c503029e4e8ff2c018014 SourceFourierSeries.lean +a60ab6099d3cef0eeecaefa9e35d95ec14ec54ffd6c89e42dfcf6170907166e8 SourceGaussianLaw.lean +5fa3abc8fb0db0c14c67b4ee840e659cdf80f7d22c9fd4cb5e6c1c7b204fbd21 SourceKernel.lean +c644305a426bc876f609c055ce999b8008f028c67a1091639d919f4122981b7b SourceLattice.lean +12ad7263267a970bd5d5c95d7c7aa62d9c971f7beebf28f1aa7ed16d3a112f1b SourceSmooth.lean +4dfa901029fab71d127c9f4c8cf30c937607f4444e6af64f429890d9d141d591 SourceSmoothAxiomAudit.lean +5defdf223e85e7ccd23b5a903a1a306fe7f723727eb6aabf62eef523ef8639ed SourceSmoothCarrier.lean +8eca5ecdb5e2a0c1cb786468b340e4516df653468f958e535f156baafef088b4 SourceSmoothControls.lean +02857b44552ab0e51a756b3b095c4ba43f8168ac332b069acb5bc8146d337eef SourceTorus.lean +b67b13030389dea4521e8e2afcac30ea44f84abd65c374bf208067b288fc64a1 SourceTorusC4.lean +92af14a2d83304de3f8576ee10b3d376587e93c4464f8c715b8d2e32360f44b0 SpectralWeights.lean +4cc60e1f98fc3a46bccafe6b8315445d950ca1db55ceba26fdebe3a45eafe59a lake-manifest.json +7782dd2fef85bf956a0ccc76e4e6420b8818eabb3bc133cade7252ea7d1d92e6 lakefile.toml +d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b lean-toolchain 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..5b1518449 --- /dev/null +++ b/frontiers/source_smooth_realization_20261011/SourceSmooth.lean @@ -0,0 +1,254 @@ +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 : Summable (fun k : ↥(halfLattice d) => orderPairedBound n d L k) := + (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, Function.comp_def] 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, modeMajorant] 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..cb6f7b108 --- /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 NNReal Manifold 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 + exact 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 (show Measurable (fun ω : SourceMode d → ℝ => orderModeBound n d L m * |ω m|) by + fun_prop).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