Research consolidation: restore reviewed PR236 source package

research/lean-paired-cube-d1d6/ARCHIVE_READBACK.json

@@ -0,0 +1,16 @@
+{
+  "accepted_manifest_sha256": "efc9bcde7d5ee1891fd5b5a61b46a76bab5ffcf57cbbd22b5e6c606a141dca57",
+  "archive": "scientific_sources.tar.gz",
+  "archive_sha256": "3ca5fa3051c8113ec05c613701d938d29ce1cf6d676a7cf118a041e4a19ff62f",
+  "bytes": 5841570,
+  "compilation_performed": false,
+  "elapsed_seconds": 1.8544307160045719,
+  "excluded": "No operational notes, logs, diagnostics, historical archives, compiled objects or unaccepted proof sources.",
+  "lean_modules": 3606,
+  "members": 3614,
+  "public_map_sha256": "995a55e631c5d5fa5ab8f6f8f84cd7b32714207963bf87b4e28f114dc2d8e249",
+  "scientific_inputs": 8,
+  "status": "PASS_CURATED_ARCHIVE_READBACK",
+  "theorems": 14320,
+  "uncompressed_file_bytes": 100172417
+}

research/lean-paired-cube-d1d6/README.md

@@ -0,0 +1,30 @@
+# Lean verification of paired-cube finite identities and κ arithmetic
+
+This package targets CrocSwap/integer-mult-bounds at merged commit `d1d6c070f5a8c684727ee7ec35d930f9ebfa9758`. It preserves the construction’s existing author-checked conditional value **κ = 4609169/10000000000 = 0.0004609169**. It adds no new exponent and does not claim a formal proof of the full asymptotic integer-multiplication theorem.
+
+The frozen accepted set contains **3,606 Lean modules and 14,320 audited theorem declarations**, including 2,816 axiom-free declarations. Other transitive dependencies are restricted to `propext`, `Quot.sound` and `Classical.choice`. The complete finite identity `J6 M V + 3 K2 = 6 I` holds for arbitrary integer payloads at all 1,760 targets of the actual 49,424-step signed word, with dirty auxiliary restoration. The package also includes exact frame/operator results, scoped local register/storage and scratch-boundary results, and source-derived finite checks for all 47 assembly inequalities and seven margins.
+
+`key_theorems/` provides readable copies of six principal theorem files. Their dependencies and the complete accepted source set are in the archive. The archive contains only accepted `.lean` sources and eight pinned scientific inputs: no historical logs, operational notes, diagnostics, compiled objects or unaccepted candidate sources. `INPUT_MAP.json` pins every file and the exact audit names.
+
+## Reproduce offline
+
+Use an already installed official Lean 4.21.0, commit 6741444a63ee, plus Python 3 on a POSIX system. No Mathlib or network access is needed for these accepted modules. Replace `/path/to/lean` below with that compiler. The installed pinned standard library is an explicit toolchain trust boundary.
+
+```sh
+sha256sum -c SHA256SUMS
+mkdir -p unpacked
+tar -xzf scientific_sources.tar.gz -C unpacked
+python offline_check.py --map INPUT_MAP.json --source-root unpacked --check-only
+python -m unittest -v test_offline_check.py
+python offline_check.py --map INPUT_MAP.json --source-root unpacked --build --resume --lean /path/to/lean --output /tmp/paired-cube-lean-build
+```
+
+For a bounded arithmetic check, add `--module PairedCubeCore --module PairedCubeIdentities --module AssemblyParameters13955` to the final command; accepted dependencies are included automatically. Sources, imports and printed audit names must match the map. Compilation uses one Lean job, a 4 GiB address-space cap and the recorded 60/120/300-second per-module limits. Resume rechecks source, dependency-object, compiler, object and audit-log identities. It never silently adopts missing or unaudited objects.
+
+## Evidence and remaining scope
+
+The accepted modules have prior successful per-module compiler and complete transitive-axiom audits. The newly introduced portable driver passed 11 deterministic fixture tests and actual isolated compilation/audit of four approved modules, 168 declarations, followed by successful receipt reuse. The curated archive was independently read back against every file digest. A complete clean rebuild with this new driver has **not** been run. Historical accepted compiler durations total about 4 h 39 m for 3,564 baseline modules;5–7hours is a planning estimate for a sequential clean run on similar hardware, not a measured clean-run result.
+
+Core integer-pair arithmetic now derives the 46 previously stored slack formulas and all seven margins from the pinned source expressions, with positive denominator conditions; the existing literal scalar guard supplies the 47th inequality. This is finite arithmetic. Real logarithm/exponential bounds, concrete rational/Gaussian field instantiation, full physical-word/readout composition, exact global restored-row and fixed-tape costs, and the inherited all-size analytic/compiler contracts remain explicit boundaries. Local scratch and storage theorems do not imply those global results.
+
+Source extraction, parsing and cryptographic provenance are executable trust boundaries. The scientific certificate’s own conditional scope remains unchanged. The underlying community construction retains all existing repository attribution; this verification work was prepared with OpenAI assistance.

research/lean-paired-cube-d1d6/SHA256SUMS

@@ -0,0 +1,13 @@
+451a7b5bda78cee812635db276627b8f632a7620f18cb2d05cc1c69cfbefc0db  ARCHIVE_READBACK.json
+995a55e631c5d5fa5ab8f6f8f84cd7b32714207963bf87b4e28f114dc2d8e249  INPUT_MAP.json
+7d1daa10754fde946ade1db0b0cb1c422c09e457daa7a29f7c49464ed25f76b3  README.md
+acc991d4c6b08796dbf76a3c55b41e908c709bb80fa2f68ce6171de2f48ebb07  key_theorems/AssemblyCoreLink13955.lean
+831fba92659d0020b4176c8c4783a5027aabc1fed1803801c7a0fddaeec45d9a  key_theorems/AssemblySummary13955.lean
+69ba50a30f19db5df3fb2a37f0f4864dfec2322d9820ca15a8aaf461d0cce6f0  key_theorems/FullActualIdentity.lean
+f03b9ac843898a56a476558b832659d5bece8fa8ddf52a26f53496d1de9e72c8  key_theorems/FullCoefficientIdentity.lean
+26d65f7955dbfffc12cf2b8380f3ba26ead70cbf99d0498b5895792fb166bdb8  key_theorems/PreparedSequentialRootEvent.lean
+e3a649c76fadeef7b02a5b69def3d17b969139386605ee759254e8823280103b  key_theorems/SequentialRootScratchBoundary.lean
+dd4368c3b942f471504fc26d2193e802de24fcb1911fed05f1c118a7076bc796  offline_check.py
+bb44e63b12c4317f5dd0ff06ffd8710bfb36ab3b14113ccd4cccebb4c251224c  prepare_curated_map.py
+3ca5fa3051c8113ec05c613701d938d29ce1cf6d676a7cf118a041e4a19ff62f  scientific_sources.tar.gz
+e9f9cfd69ae2235bdd7271bcae6b88aebef045c461391afd2b96e11dc2c9553f  test_offline_check.py

research/lean-paired-cube-d1d6/key_theorems/AssemblyCoreLink13955.lean

@@ -0,0 +1,65 @@
+import AssemblySummary13955
+import PairedCubeCore
+namespace PairedCubeAssembly13955
+set_option maxRecDepth 10000
+set_option maxHeartbeats 4000000
+
+/-! The imported 124-declaration Core source is unchanged. These identities
+link its Nat cross-product interfaces to the full assembly expression graph.
+The final scalar guard is reused as a proved dependency rather than recomputed. -/
+
+def coreA : Pair := ⟨(PairedCubeCore.aNum : Int), (PairedCubeCore.aDen : Int)⟩
+def coreQ : Pair := ⟨(PairedCubeCore.qNum : Int), (PairedCubeCore.qDen : Int)⟩
+def coreEps : Pair := ⟨(PairedCubeCore.epsNum : Int), (PairedCubeCore.epsDen : Int)⟩
+def coreMinimum : Pair := ⟨(PairedCubeCore.minimumNum : Int), (PairedCubeCore.minimumDen : Int)⟩
+def coreKappa : Pair := ⟨(PairedCubeCore.kappaNum : Int), (PairedCubeCore.kappaDen : Int)⟩
+
+theorem bit_saving_matches_core : SameValue a coreA := by
+  decide
+
+theorem q_matches_core : SameValue q coreQ := by
+  decide
+
+theorem epsilon_matches_core : SameValue eps coreEps := by
+  decide
+
+theorem minimum_matches_core : SameValue minimum coreMinimum := by
+  decide
+
+theorem explicit_kappa_unchanged : KAPPA.num = 4609169 ∧ KAPPA.den = 10000000000 ∧
+    SameValue KAPPA coreKappa := by
+  decide
+
+theorem row_coefficient_retains_core_derivation :
+    (72^3 ≤ 2*60^3 ∧ 2*60^4 < 72^4 ∧ 4*2571+9909+252 = (20445 : Nat)) ∧
+    ExactValue rowCoefficient 20445 1 := by
+  exact ⟨PairedCubeCore.halving_and_row_coefficient, row_coefficient_derived⟩
+
+theorem core_absorption_unchanged : SameValue minimum coreMinimum ∧
+    SameValue KAPPA coreKappa ∧
+    PairedCubeCore.kappaNum*PairedCubeCore.minimumDen <
+      PairedCubeCore.minimumNum*PairedCubeCore.kappaDen := by
+  exact ⟨minimum_matches_core, explicit_kappa_unchanged.2.2,
+    PairedCubeCore.selected_strict_absorption_cross⟩
+
+theorem all_47_strict_formula_checks : AllSlacksLinked ∧
+    PairedCubeCore.literalCharge < PairedCubeCore.guardE := by
+  exact ⟨all_46_slack_formulas_linked, PairedCubeCore.full_scalar_guard⟩
+
+theorem complete_finite_assembly_interface : AllSlacksLinked ∧ AllMarginsLinked ∧
+    SameValue minimum coreMinimum ∧ SameValue KAPPA coreKappa ∧
+    Below KAPPA minimum ∧ PairedCubeCore.literalCharge < PairedCubeCore.guardE := by
+  exact ⟨all_46_slack_formulas_linked, all_seven_margin_formulas_linked,
+    minimum_matches_core, explicit_kappa_unchanged.2.2, strict_absorption,
+    PairedCubeCore.full_scalar_guard⟩
+
+end PairedCubeAssembly13955
+#print axioms PairedCubeAssembly13955.bit_saving_matches_core
+#print axioms PairedCubeAssembly13955.q_matches_core
+#print axioms PairedCubeAssembly13955.epsilon_matches_core
+#print axioms PairedCubeAssembly13955.minimum_matches_core
+#print axioms PairedCubeAssembly13955.explicit_kappa_unchanged
+#print axioms PairedCubeAssembly13955.row_coefficient_retains_core_derivation
+#print axioms PairedCubeAssembly13955.core_absorption_unchanged
+#print axioms PairedCubeAssembly13955.all_47_strict_formula_checks
+#print axioms PairedCubeAssembly13955.complete_finite_assembly_interface

research/lean-paired-cube-d1d6/key_theorems/AssemblySummary13955.lean

@@ -0,0 +1,82 @@
+import AssemblyPairLaws13955
+import AssemblyParameters13955
+import AssemblySlacksA13955
+import AssemblySlacksB13955
+import AssemblyMargins13955
+import AssemblyDenominators13955
+namespace PairedCubeAssembly13955
+
+def AllSlacksLinked : Prop :=
+  (ExactValue slack_bit_positive 4613422943 10000000000000 ∧ Positive slack_bit_positive) ∧
+  (ExactValue slack_complex_above_bit 243146057 10000000000000 ∧ Positive slack_complex_above_bit) ∧
+  (ExactValue slack_complex_below_one_over32 307643431 10000000000 ∧ Positive slack_complex_below_one_over32) ∧
+  (ExactValue slack_beta_positive 1 1000000 ∧ Positive slack_beta_positive) ∧
+  (ExactValue slack_beta_below_one 999999 1000000 ∧ Positive slack_beta_below_one) ∧
+  (ExactValue slack_leaf_saving_above_bit 243141200431 10000000000000000 ∧ Positive slack_leaf_saving_above_bit) ∧
+  (ExactValue slack_q_positive 230671142536577057 500000000000000000000 ∧ Positive slack_q_positive) ∧
+  (ExactValue slack_q_below_internal 4613422943 500000000000000000000 ∧ Positive slack_q_below_internal) ∧
+  (ExactValue slack_q_below_leaf 12157064634972943 500000000000000000000 ∧ Positive slack_q_below_leaf) ∧
+  (ExactValue slack_c_positive 23067114484328848236577057 50000000000000000000000000000 ∧ Positive slack_c_positive) ∧
+  (ExactValue slack_c_below_one 49976932885515671151763422943 50000000000000000000000000000 ∧ Positive slack_c_below_one) ∧
+  (ExactValue slack_q_below_reservations 230671142536577057 50000000000000000000000000000 ∧ Positive slack_q_below_reservations) ∧
+  (ExactValue slack_lambda_above_tau 4613422943 1000000000000000000000 ∧ Positive slack_lambda_above_tau) ∧
+  (ExactValue slack_lambda_above_sigma 24314610313422943 1000000000000000000000 ∧ Positive slack_lambda_above_sigma) ∧
+  (ExactValue slack_lambda_above_internal 4613422943 1000000000000000000000 ∧ Positive slack_lambda_above_internal) ∧
+  (ExactValue slack_lambda_prime_above_lambda 4613422943 1000000000000000000000 ∧ Positive slack_lambda_prime_above_lambda) ∧
+  (ExactValue slack_compact_leaf 12157064634972943 500000000000000000000 ∧ Positive slack_compact_leaf) ∧
+  (ExactValue slack_compact_reservations 230671142536577057 50000000000000000000000000000 ∧ Positive slack_compact_reservations) ∧
+  (ExactValue slack_lambda_prime_below_one 230671142536577057 500000000000000000000 ∧ Positive slack_lambda_prime_below_one) ∧
+  (ExactValue slack_epsilon_positive 49999999500000000000000000000 50046134228737986553936577057 ∧ Positive slack_epsilon_positive) ∧
+  (ExactValue slack_epsilon_below_one 46134728737986553936577057 50046134228737986553936577057 ∧ Positive slack_epsilon_below_one) ∧
+  (ExactValue slack_guard_width 46134728737986553936577057 50046134228737986553936577057 ∧ Positive slack_guard_width) ∧
+  (ExactValue slack_K_geometry 2306761448432885054328848236577057 5004613422873798655393657705700000000 ∧ Positive slack_K_geometry) ∧
+  (ExactValue slack_K_dominates_log 2306711425365770339328857463422943 5004613422873798655393657705700000000 ∧ Positive slack_K_dominates_log) ∧
+  (ExactValue slack_record_suffix 46134728737986553936577057 50046134228737986553936577057 ∧ Positive slack_record_suffix) ∧
+  (ExactValue slack_phase_local 36907732944255014411275091663422943 40036907382990389243149261645600000000 ∧ Positive slack_phase_local) ∧
+  (ExactValue slack_phase_boundary 27680687058255018102013446063422943 40036907382990389243149261645600000000 ∧ Positive slack_phase_boundary) ∧
+  (ExactValue slack_gamma_sublinear 11533807357499995386577057 50046134228737986553936577057 ∧ Positive slack_gamma_sublinear) ∧
+  (ExactValue slack_cell_above_band 49988465692642500004613422943 100092268457475973107873154114 ∧ Positive slack_cell_above_band) ∧
+  (ExactValue slack_prime_interval_packing 46134728737986553936577057 50046134228737986553936577057 ∧ Positive slack_prime_interval_packing) ∧
+  (ExactValue slack_alpha_positive 34600921380486558550000000 50046134228737986553936577057 ∧ Positive slack_alpha_positive) ∧
+  (ExactValue slack_alpha_below_one 50011533307357499995386577057 50046134228737986553936577057 ∧ Positive slack_alpha_below_one) ∧
+  (ExactValue slack_alpha_below_one_fourth 49907730543216040319736577057 200184536914951946215746308228 ∧ Positive slack_alpha_below_one_fourth) ∧
+  (ExactValue slack_delta_positive 1 800000000 ∧ Positive slack_delta_positive) ∧
+  (ExactValue slack_delta_below_one_eighth 99999999 800000000 ∧ Positive slack_delta_below_one_eighth) ∧
+  (ExactValue slack_short_record_fallback 499769111016140682562896443488438348781249 500461342287379865539365770570000000000000 ∧ Positive slack_short_record_fallback) ∧
+  (ExactValue slack_small_field_exposure 23067614714999990773154114 50046134228737986553936577057 ∧ Positive slack_small_field_exposure) ∧
+  (ExactValue slack_artificial_boundary 280304486459762979712765368256463422943 40036907382990389243149261645600000000 ∧ Positive slack_artificial_boundary) ∧
+  (ExactValue slack_row_product_gap 141461 5 ∧ Positive slack_row_product_gap) ∧
+  (ExactValue slack_original_prefix_above_kappa 5054386350468686063524720470067 500461342287379865539365770570000000000 ∧ Positive slack_original_prefix_above_kappa) ∧
+  (ExactValue slack_coordinate_movement_above_kappa 4253943 10000000000000 ∧ Positive slack_coordinate_movement_above_kappa) ∧
+  (ExactValue slack_compact_phase_layer_above_kappa 49772927594887408131062764367 500461342287379865539365770570000000000 ∧ Positive slack_compact_phase_layer_above_kappa) ∧
+  (ExactValue slack_bulk_exposure_above_kappa 4253943 10000000000000 ∧ Positive slack_bulk_exposure_above_kappa) ∧
+  (ExactValue slack_Gaussian_arithmetic_above_kappa 230674995542499379056693553711102309 1000922684574759731078731541140000000000 ∧ Positive slack_Gaussian_arithmetic_above_kappa) ∧
+  (ExactValue slack_scalar_work_above_kappa 461351142692499286788234693711102309 1000922684574759731078731541140000000000 ∧ Positive slack_scalar_work_above_kappa) ∧
+  (ExactValue slack_dimension_above_kappa 499769323909543061963253178701062764367 500461342287379865539365770570000000000 ∧ Positive slack_dimension_above_kappa)
+
+def AllMarginsLinked : Prop :=
+  (ExactValue margin_original_prefix 2306761448432885054328848236577057 5004613422873798655393657705700000000 ∧ AtMost minimum margin_original_prefix ∧ Below KAPPA margin_original_prefix) ∧
+  (ExactValue margin_coordinate_movement 4613422943 10000000000000 ∧ AtMost minimum margin_coordinate_movement ∧ Below KAPPA margin_coordinate_movement) ∧
+  (ExactValue margin_compact_phase_layer 23067114022986563163422943 50046134228737986553936577057 ∧ AtMost minimum margin_compact_phase_layer ∧ Below KAPPA margin_compact_phase_layer) ∧
+  (ExactValue margin_bulk_exposure 4613422943 10000000000000 ∧ AtMost minimum margin_bulk_exposure ∧ Below KAPPA margin_bulk_exposure) ∧
+  (ExactValue margin_Gaussian_arithmetic 27680687058255018102013446063422943 40036907382990389243149261645600000000 ∧ AtMost minimum margin_Gaussian_arithmetic ∧ Below KAPPA margin_Gaussian_arithmetic) ∧
+  (ExactValue margin_scalar_work 36907732944255014411275091663422943 40036907382990389243149261645600000000 ∧ AtMost minimum margin_scalar_work ∧ Below KAPPA margin_scalar_work) ∧
+  (ExactValue margin_dimension 49999999500000000000000000000 50046134228737986553936577057 ∧ AtMost minimum margin_dimension ∧ Below KAPPA margin_dimension)
+
+theorem all_46_slack_formulas_linked : AllSlacksLinked := by
+  exact ⟨slack_bit_positive_derived, slack_complex_above_bit_derived, slack_complex_below_one_over32_derived, slack_beta_positive_derived, slack_beta_below_one_derived, slack_leaf_saving_above_bit_derived, slack_q_positive_derived, slack_q_below_internal_derived, slack_q_below_leaf_derived, slack_c_positive_derived, slack_c_below_one_derived, slack_q_below_reservations_derived, slack_lambda_above_tau_derived, slack_lambda_above_sigma_derived, slack_lambda_above_internal_derived, slack_lambda_prime_above_lambda_derived, slack_compact_leaf_derived, slack_compact_reservations_derived, slack_lambda_prime_below_one_derived, slack_epsilon_positive_derived, slack_epsilon_below_one_derived, slack_guard_width_derived, slack_K_geometry_derived, slack_K_dominates_log_derived, slack_record_suffix_derived, slack_phase_local_derived, slack_phase_boundary_derived, slack_gamma_sublinear_derived, slack_cell_above_band_derived, slack_prime_interval_packing_derived, slack_alpha_positive_derived, slack_alpha_below_one_derived, slack_alpha_below_one_fourth_derived, slack_delta_positive_derived, slack_delta_below_one_eighth_derived, slack_short_record_fallback_derived, slack_small_field_exposure_derived, slack_artificial_boundary_derived, slack_row_product_gap_derived, slack_original_prefix_above_kappa_derived, slack_coordinate_movement_above_kappa_derived, slack_compact_phase_layer_above_kappa_derived, slack_bulk_exposure_above_kappa_derived, slack_Gaussian_arithmetic_above_kappa_derived, slack_scalar_work_above_kappa_derived, slack_dimension_above_kappa_derived⟩
+
+theorem all_seven_margin_formulas_linked : AllMarginsLinked := by
+  exact ⟨margin_original_prefix_derived, margin_coordinate_movement_derived, margin_compact_phase_layer_derived, margin_bulk_exposure_derived, margin_Gaussian_arithmetic_derived, margin_scalar_work_derived, margin_dimension_derived⟩
+
+theorem minimum_is_attained : margin_compact_phase_layer = minimum := by
+  rfl
+
+theorem finite_assembly_formula_certificate : AllSlacksLinked ∧ AllMarginsLinked ∧ ExactValue minimum 23067114022986563163422943 50046134228737986553936577057 ∧ Below KAPPA minimum ∧ ExactValue (minimum-KAPPA) 49772927594887408131062764367 500461342287379865539365770570000000000 := by
+  exact ⟨all_46_slack_formulas_linked, all_seven_margin_formulas_linked, minimum_derived.1, strict_absorption, absorption_gap_derived.1⟩
+
+end PairedCubeAssembly13955
+#print axioms PairedCubeAssembly13955.all_46_slack_formulas_linked
+#print axioms PairedCubeAssembly13955.all_seven_margin_formulas_linked
+#print axioms PairedCubeAssembly13955.minimum_is_attained
+#print axioms PairedCubeAssembly13955.finite_assembly_formula_certificate