diff --git a/AGENTS.md b/AGENTS.md index 11fbf0f8..498cde73 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -364,8 +364,11 @@ Current Research Stack cornfield ref (for cross-repo lookup only): - The `python/` and `qubo/` directories are I/O and optimization shims only; they may not contain admissibility logic. - `docs/GLOSSARY.md` is the authoritative term dictionary. New domain terms - introduced in receipts, gates, or cross-module interfaces must be added there - with a source-module citation before they are used. + introduced in receipts, gates, or cross-module interfaces must be added there + with a source-module citation before they are used. +- `experiments/bosonic_continuous/` contains the continuous λ(p) interpolation + validation for the bosonic Monte Carlo estimator, demonstrating smooth transition + across p=1..6 with no regime boundary. Source for BMCTE class definition. - Research artifacts and scratch output should live outside the git tree unless promoted as durable receipts. - RRC status is tracked in `docs/RRC_REFACTOR_READINESS.md`. diff --git a/CITATION.cff b/CITATION.cff index 254fad36..1beeae07 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -174,6 +174,26 @@ references: url: "https://arxiv.org/abs/2605.17913" notes: "Binds to Research Stack `Semantics.FixedPoint` (inverse-proof machinery in `Semantics.Q16InverseProof`) → SilverSight `formal/CoreFormalism/FixedPoint.lean`; differentiable primal-dual IPM with bounded KKT systems for low-precision / fixed-point arithmetic, justifying the no-Float compute boundary." + - type: article + title: "Everything Is Logarithms" + authors: + - family-names: "Kritchevsky" + given-names: "Alex" + date-published: 2026-05-25 + url: "https://alexkritchevsky.com/2026/05/25/everything-is-logarithms.html" + notes: >- + Binds to SilverSight `formal/CoreFormalism/HachimojiLUT.lean` (PhaseCircle, + phaseEmbed) and `formal/CoreFormalism/ChentsovFinite.lean` (Fisher metric + uniqueness). Core claim: logarithms are coordinate-free objects; units + emerge from ratios (log N / log 2), and dim(U⊗V) = dim(U)×dim(V) mirrors + the additive structure of log. The multiplicative-to-additive isomorphism + underpins the phase-circle encoding (ℤ/360ℤ as an additive group of + logarithmic phase steps) and the Q16_16 entropy estimator (entropy_q16 + computes log₂ probabilities in integer arithmetic). The coordinate-free + framing also grounds Chentsov uniqueness: the Fisher metric is invariant + under sufficient statistics, i.e., under the natural logarithmic + re-parameterisation of probability families. + - type: article title: "Stabilizing Recurrent Dynamics for Test-Time Scalable Latent Reasoning in Looped Language Models" authors: diff --git a/docs/GLOSSARY.md b/docs/GLOSSARY.md index 9e10ece3..90ca031a 100644 --- a/docs/GLOSSARY.md +++ b/docs/GLOSSARY.md @@ -152,6 +152,10 @@ name and explains the delta. | **meta-solid** | Topological triple point where trace closure, local Yang-Baxter isotopy, and braid class are simultaneously exact. | ContextStream node `e967f515-3af9-46c9-9fc8-e5c766a6c4fc`; bound to `formal/CoreFormalism/BraidEigensolid.lean` | | **Finsler-Randers** | Directed routing metric used in the QUBO/TSP benchmark. | `qubo/finsler_metric.py` (planned) | | **QUBO** | Quadratic Unconstrained Binary Optimization; a classical/quantum optimization encoding. | `qubo/qubo_builder.py` (planned) | +| **BMCTE** | Bosonic Monte Carlo Tensor Estimation class: problems solvable by O(S·(Np+p²2^p)) stochastic contraction of Sym^p(U) without explicit Fock-space construction. | `experiments/bosonic_continuous/kernel/ryser_continuous.py` | +| **BoseMonteCarloEstimator** | Stochastic estimator P^p(U) = Σ_k |Per(U_{S_k})|² / K! using Monte Carlo sampling of mode configurations with Ryser permanent evaluation. | `4-Infrastructure/shim/rrc_bosonic_tensor_network.py` | +| **ContinuousInterpolation** | λ(p) = exp(-p²/N) smooth blending parameter between fully bosonic (λ→1) and weakly-correlated (λ→0) regimes. | `experiments/bosonic_continuous/tests/test_lambda_interpolation.py` | +| **EntropyInvarianceHypothesis** | In BMCTE regime, Shannon entropy H(p) ≈ 10 bits remains constant across p=1..6 for N=2000, indicating projection-dominated measurement rather than full-state exploration. | `experiments/bosonic_continuous/README.md` | ## Modules and library layers diff --git a/formal/CoreFormalism/HachimojiCodec.lean b/formal/CoreFormalism/HachimojiCodec.lean index ef2d2a19..da7261b2 100644 --- a/formal/CoreFormalism/HachimojiCodec.lean +++ b/formal/CoreFormalism/HachimojiCodec.lean @@ -84,10 +84,10 @@ def StateΚ : HachimojiState4D := def StateΩ : HachimojiState4D := { phase := 180, chirality := .ambidextrous, direction := .reverse, regime := .horribleManifoldTearing } -def StateΣ : HachimojiState4D := +def StateSigma : HachimojiState4D := { phase := 225, chirality := .right, direction := .reverse, regime := .horribleManifoldTearing } -def StateΠ : HachimojiState4D := +def StatePi : HachimojiState4D := { phase := 270, chirality := .right, direction := .reverse, regime := .horribleManifoldTearing } def StateΖ : HachimojiState4D := @@ -167,10 +167,10 @@ theorem StateΚ_consistent : consistencyInvariant StateΚ = true := by rfl theorem StateΩ_consistent : consistencyInvariant StateΩ = true := by rfl /-- Σ is consistent. -/ -theorem StateΣ_consistent : consistencyInvariant StateΣ = true := by rfl +theorem StateSigma_consistent : consistencyInvariant StateSigma = true := by rfl /-- Π is consistent. -/ -theorem StateΠ_consistent : consistencyInvariant StateΠ = true := by rfl +theorem StatePi_consistent : consistencyInvariant StatePi = true := by rfl /-- Ζ is consistent. -/ theorem StateΖ_consistent : consistencyInvariant StateΖ = true := by rfl @@ -196,10 +196,10 @@ theorem StateΚ_admits : admission StateΚ = .ADMIT := by rfl theorem StateΩ_quarantines : admission StateΩ = .QUARANTINE := by rfl /-- Σ admits (special symmetric partner exception). -/ -theorem StateΣ_admits : admission StateΣ = .ADMIT := by rfl +theorem StateSigma_admits : admission StateSigma = .ADMIT := by rfl /-- Π quarantines (reverse half, not Σ). -/ -theorem StateΠ_quarantines : admission StateΠ = .QUARANTINE := by rfl +theorem StatePi_quarantines : admission StatePi = .QUARANTINE := by rfl /-- Ζ quarantines (reverse half, not Σ). -/ theorem StateΖ_quarantines : admission StateΖ = .QUARANTINE := by rfl @@ -260,10 +260,10 @@ def classifyEquation (shape : EquationShape) : HachimojiState4D := -- Π (potential): high complexity else if shape.n_ops + shape.n_vars * shape.max_depth + shape.n_quantifiers * 2 ≥ 8 || shape.n_ops > 8 then - StateΠ + StatePi -- Σ (symmetric): balanced structure else if isSymmetric shape then - StateΣ + StateSigma -- Ρ (tight): high operator count, no quantifiers else if shape.n_ops > 5 && shape.n_quantifiers == 0 then StateΡ @@ -312,7 +312,7 @@ theorem test_exists_notin : theorem test_integral : admission (classifyEquation { n_vars := 4, n_ops := 4, max_depth := 1, n_quantifiers := 0, n_relations := 1 }) = .QUARANTINE := by - rfl + decide /-- "" (empty) → Ζ → QUARANTINE -/ theorem test_empty : @@ -345,10 +345,10 @@ theorem pipeline_safety (shape : EquationShape) No two distinct canonical states share the same descriptor. -/ theorem canonical_states_injective : StateΦ ≠ StateΛ ∧ StateΦ ≠ StateΡ ∧ StateΦ ≠ StateΚ ∧ - StateΦ ≠ StateΩ ∧ StateΦ ≠ StateΣ ∧ StateΦ ≠ StateΠ ∧ StateΦ ≠ StateΖ ∧ + StateΦ ≠ StateΩ ∧ StateΦ ≠ «StateSigma» ∧ StateΦ ≠ «StatePi» ∧ StateΦ ≠ StateΖ ∧ StateΛ ≠ StateΡ ∧ StateΛ ≠ StateΚ ∧ StateΛ ≠ StateΩ ∧ - StateΛ ≠ StateΣ ∧ StateΛ ≠ StateΠ ∧ StateΛ ≠ StateΖ := by - constructor <;> rfl + StateΛ ≠ «StateSigma» ∧ StateΛ ≠ «StatePi» ∧ StateΛ ≠ StateΖ := by + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide -- ============================================================ -- §12 FORWARD REGIME IS EXACTLY THE FIRST 4 STATES @@ -360,7 +360,7 @@ def isForward (s : HachimojiState4D) : Bool := /-- The forward states are exactly Φ, Λ, Ρ, Κ. -/ theorem forward_states_exactly (s : HachimojiState4D) - (hφ : s = StateΦ) (hλ : s = StateΛ) (hρ : s = StateΡ) (hκ : s = StateΚ) : + (hφ : s = StateΦ) (hL : s = StateΛ) (hρ : s = StateΡ) (hκ : s = StateΚ) : isForward s = true := by - rcases hφ <;> rcases hλ <;> rcases hρ <;> rcases hκ <;> simp [isForward] + rcases hφ <;> rcases hL <;> rcases hρ <;> rcases hκ <;> simp [isForward] <;> rfl diff --git a/formal/CoreFormalism/HachimojiLUT.lean b/formal/CoreFormalism/HachimojiLUT.lean index d3f66dbd..f4b5bf59 100644 --- a/formal/CoreFormalism/HachimojiLUT.lean +++ b/formal/CoreFormalism/HachimojiLUT.lean @@ -79,9 +79,9 @@ theorem canonical_indices_distinct : stateIndex StateΛ ≠ stateIndex StateΡ ∧ stateIndex StateΡ ≠ stateIndex StateΚ ∧ stateIndex StateΚ ≠ stateIndex StateΩ ∧ - stateIndex StateΩ ≠ stateIndex StateΣ ∧ - stateIndex StateΣ ≠ stateIndex StateΠ ∧ - stateIndex StateΠ ≠ stateIndex StateΖ := by + stateIndex StateΩ ≠ stateIndex StateSigma ∧ + stateIndex StateSigma ≠ stateIndex StatePi ∧ + stateIndex StatePi ≠ stateIndex StateΖ := by constructor <;> rfl /-- stateIndex agrees with phase / 45 for all 8 canonical states. -/ @@ -185,8 +185,8 @@ theorem canonical_phases_preserved : stateToPhase StateΡ = ⟨90, by norm_num⟩ ∧ stateToPhase StateΚ = ⟨135, by norm_num⟩ ∧ stateToPhase StateΩ = ⟨180, by norm_num⟩ ∧ - stateToPhase StateΣ = ⟨225, by norm_num⟩ ∧ - stateToPhase StateΠ = ⟨270, by norm_num⟩ ∧ + stateToPhase StateSigma = ⟨225, by norm_num⟩ ∧ + stateToPhase StatePi = ⟨270, by norm_num⟩ ∧ stateToPhase StateΖ = ⟨315, by norm_num⟩ := by constructor <;> rfl @@ -221,7 +221,7 @@ theorem pythagorean_position : equationPosition { n_vars := 3, n_ops := 7, max_depth := 0, n_quantifiers := 0, n_relations := 1 } = phaseEmbed ⟨225, by norm_num⟩ := by - simp [equationPosition, classifyEquation, stateToPhase, StateΣ] + simp [equationPosition, classifyEquation, stateToPhase, StateSigma] /-- Contradiction "0 = 1" lives at the Ω (collision) vertex. -/ theorem contradiction_position : diff --git a/lakefile.lean b/lakefile.lean index c9927e91..3f5cf645 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -31,7 +31,12 @@ lean_lib «SilverSightFormal» where `CoreFormalism.SieveLemmas, `CoreFormalism.InteractionGraphSidon, `CoreFormalism.BraidEigensolid, - `CoreFormalism.BraidSpherionBridge + `CoreFormalism.BraidSpherionBridge, + `CoreFormalism.ChentsovFinite, + `CoreFormalism.HachimojiBase, + `CoreFormalism.HachimojiManifoldAxiom, + `CoreFormalism.HachimojiCodec, + `CoreFormalism.HachimojiLUT ] lean_lib «SilverSightRRC» where