mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
1794299a6c
Systematic native_decide → dec_trivial/rfl migration across all Lean modules to comply with AGENTS.md rule 5 (no native_decide unless only option): - CoreFormalism: BraidEigensolid, BraidField, ChentsovFinite, HachimojiBase, HachimojiBridging, HachimojiCodec, HachimojiLUT, HachimojiManifoldAxiom, Q16_16Numerics - BindingSite: BindingSiteCodec, BindingSiteEntropy, BindingSiteHachimoji - SilverSight: ProductSchema, ProductWireFormat, PolyFactorIdentity, Schema, WireFormat - PVGS_DQ_Bridge: all three files (native_decide->dec_trivial) - UniversalEncoding/ChiralitySpace Additional changes: - gemma4_mcp.py: upgraded to two-tier routing (local Gemma4 + FreeLLMAPI proxy) - ChentsovFinite: added traceability map and Chentsov (1972) citation - HachimojiBase: renamed Σ→Sig, Π→Pi to avoid non-ASCII issues - Import path fixes for Mathlib 4.30.0-rc2 compatibility - Doc updates: PURE_FORMULAS, SOS_CERTIFICATE, fundamental math derivations - Build log: 2026-06-26 session findings - BRKGLASS_NR_BRACKET_PROPOSAL: updated to REAL-DATA VALIDATED status - New docs: FOUNDATIONAL_GUIDANCE, PURE_EQUATION_MAP, CHENTSOV_FINITE_MATH, BREAKGLASS_FUSION_REVIEW_SPEC, COLD_REVIEWER_FORMULA - New python: phi pipeline (equation_dna_encoder, ast_parse, charclass, consistency, embed, output), nr_bracket_validation with receipt Build: lake build SilverSightRRC — passes on all committed modules. Excluded: HachimojiN8Bridge, HachimojiCharClass (missing CoreFormalism.HachimojiManifoldAxiom olean — WIP)
85 lines
4.8 KiB
Text
85 lines
4.8 KiB
Text
/-
|
||
BindingSite.BindingSiteHachimoji — Amino acid encoding and Fisher metric.
|
||
|
||
Defines the computable core of the binding site pipeline and the noncomputable
|
||
Fisher metric used in the §5 theorems of BindingSiteEntropy.lean.
|
||
|
||
Chentsov uniqueness (ChentsovFinite.lean) is quarantined — it has 15+ sorries
|
||
and is a deep geometry result. This file provides the amino acid / state
|
||
machinery WITHOUT depending on the Chentsov proof.
|
||
-/
|
||
import BindingSite.BindingSiteTypes
|
||
import Mathlib.Data.Real.Basic
|
||
import Mathlib.Data.Fin.Basic
|
||
|
||
namespace BindingSite
|
||
|
||
open SilverSight.FixedPoint
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §1 Amino acid probability distribution (for math §5 only)
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- A probability distribution over 50 atom types (Void-X parameterization).
|
||
Used only in noncomputable Fisher metric theorems; not in the compute path. -/
|
||
structure AminoAcidDistribution where
|
||
val : Fin 50 → ℝ
|
||
pos : ∀ i, 0 < val i
|
||
sum_eq : ∑ i, val i = 1
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §2 Fisher metric (noncomputable — appears only in math section)
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Fisher information metric on Δ⁴⁹ (50-dimensional probability simplex).
|
||
Diagonal form: g_ij(p) = δ_ij / p_i.
|
||
Uniqueness up to positive scalar: Chentsov's theorem (quarantined). -/
|
||
noncomputable def fisherMetric50 (p : AminoAcidDistribution) (i j : Fin 50) : ℝ :=
|
||
if i = j then 1 / p.val i else 0
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §3 Dominant state extractor
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Return the most common BindingSiteState in a list of classified residues.
|
||
Tie-breaking: earlier states win. -/
|
||
def dominantState (residues : List BindingSiteResidue) : BindingSiteState :=
|
||
let counts : List (BindingSiteState × Nat) :=
|
||
[ (.Phi, residues.countP (·.state == .Phi))
|
||
, (.Lambda, residues.countP (·.state == .Lambda))
|
||
, (.Rho, residues.countP (·.state == .Rho))
|
||
, (.Kappa, residues.countP (·.state == .Kappa))
|
||
, (.Omega, residues.countP (·.state == .Omega))
|
||
, (.Sigma, residues.countP (·.state == .Sigma))
|
||
, (.Pi, residues.countP (·.state == .Pi))
|
||
, (.Zeta, residues.countP (·.state == .Zeta))
|
||
]
|
||
(counts.foldl (fun (best : BindingSiteState × Nat) pair =>
|
||
if pair.2 > best.2 then pair else best) (.Zeta, 0)).1
|
||
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
-- §4 Profile builder
|
||
-- ═══════════════════════════════════════════════════════════════════════════
|
||
|
||
/-- Build a BindingSiteProfile from a list of classified residues.
|
||
All arithmetic is Q16_16; no Float. -/
|
||
def buildProfile
|
||
(classified : List (AminoAcidToken × Q16_16 × BindingSiteState))
|
||
: BindingSiteProfile :=
|
||
let entropies := classified.map (·.2.1)
|
||
let dominant := dominantState (classified.map fun (t, e, s) =>
|
||
{ token := t, entropy := e, state := s
|
||
, position := (Q16_16.zero, Q16_16.zero, Q16_16.zero)
|
||
, bindability := Q16_16.ofNat 50 })
|
||
{ residues := classified.map fun (t, e, s) =>
|
||
{ token := t, entropy := e, state := s
|
||
, position := (Q16_16.zero, Q16_16.zero, Q16_16.zero)
|
||
, bindability := Q16_16.ofNat 50 }
|
||
, totalEntropy := q16Mean entropies
|
||
, maxEntropy := q16Max entropies
|
||
, minEntropy := q16Min entropies
|
||
, siteState := dominant
|
||
, druggable := dominant == .Pi || dominant == .Lambda
|
||
, receiptHash := "PENDING" }
|
||
|
||
end BindingSite
|