docs(silversight): document λ(p) bosonic estimator results

Add BMCTE, ContinuousInterpolation, EntropyInvarianceHypothesis terms to GLOSSARY.
Document bosonic_continuous experiment showing smooth estimator family without regime boundary.
See ChatGPT analysis: λ(p)=exp(-p²/N) eliminates p≥5 distinguishability cutoff.

Build: 2987 jobs, 0 errors

AGENTS.md

@@ -366,6 +366,9 @@ Current Research Stack cornfield ref (for cross-repo lookup only):
 - `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.
+- `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`.

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:

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
 

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
+    StateΛ ≠ «StateSigma» ∧ StateΛ ≠ «StatePi» ∧ StateΛ ≠ StateΖ := by
-  constructor <;> rfl
+  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

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 StateSigma ∧
-    stateIndex StateΣ ≠ stateIndex StateΠ ∧
+    stateIndex StateSigma ≠ stateIndex StatePi ∧
-    stateIndex StateΠ ≠ stateIndex StateΖ := by
+    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 StateSigma = ⟨225, by norm_num⟩ ∧
-    stateToPhase StateΠ = ⟨270, 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 :

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