Research-Stack/5-Applications/scripts/bridge_lean_math_forest.py

#!/usr/bin/env python3
"""
Bridge Lean Analysis Math with Forest Equations

Uses Equation Forest bridge nodes (B1-B8) to systematically bridge
Lean analysis math equations with forest equations based on intersections.
"""

import json
from pathlib import Path
from typing import Dict, List, Tuple, Any


class ForestBridge:
    """
    Bridges equations using Equation Forest bridge nodes.
    """
    
    # Bridge nodes from Equation Forest
    BRIDGES = {
        "B1": {"name": "Entropy ↔ Load", "from": "entropy", "to": "load"},
        "B2": {"name": "AVMR ↔ Entropy", "from": "avmr", "to": "entropy"},
        "B3": {"name": "S3C ↔ Codec", "from": "s3c", "to": "codec"},
        "B4": {"name": "PIST ↔ Surface", "from": "pist", "to": "surface"},
        "B5": {"name": "Geometry ↔ Energy", "from": "geometry", "to": "energy"},
        "B6": {"name": "Load ↔ Verification", "from": "load", "to": "verification"},
        "B7": {"name": "Energy ↔ Control", "from": "energy", "to": "control"},
        "B8": {"name": "Codec ↔ Verification", "from": "codec", "to": "verification"}
    }
    
    def __init__(self):
        self.bridges_created = []
    
    def classify_equation_domain(self, equation: Dict[str, str]) -> str:
        """
        Classify equation into a domain for bridging.
        """
        # Handle both Lean equations (Model_Name) and forest equations (name)
        name = equation.get("Model_Name", equation.get("name", "")).lower()
        family = equation.get("Family", equation.get("family", "")).lower()
        equation_str = equation.get("Equation", equation.get("equation", "")).lower()
        
        # Classification logic
        if "continuity" in name or "differentiable" in name:
            return "surface"  # Continuity = surface smoothness
        elif "convex" in name:
            return "geometry"  # Convexity = geometric property
        elif "lipschitz" in name or "ode" in name:
            return "energy"  # ODE/Lipschitz = energy dynamics
        elif "topology" in family or "manifold" in name:
            return "geometry"  # Topology = geometry
        elif "efficiency" in family:
            return "load"  # Efficiency = load reduction
        elif "entropy" in equation_str:
            return "entropy"
        elif "verification" in equation_str:
            return "verification"
        elif "control" in equation_str:
            return "control"
        elif "codec" in equation_str or "compression" in equation_str:
            return "codec"
        elif "pist" in equation_str:
            return "pist"
        elif "avmr" in equation_str:
            return "avmr"
        elif "s3c" in equation_str:
            return "s3c"
        else:
            return "surface"  # Default to surface for analysis math
    
    def find_bridge(self, from_domain: str, to_domain: str) -> Dict[str, str]:
        """
        Find appropriate bridge node between two domains.
        """
        for bridge_id, bridge in self.BRIDGES.items():
            if bridge["from"] == from_domain and bridge["to"] == to_domain:
                return {"id": bridge_id, **bridge}
            if bridge["from"] == to_domain and bridge["to"] == from_domain:
                return {"id": bridge_id, **bridge}
        
        # No direct bridge, try indirect
        return None
    
    def create_bridge(self, lean_eq: Dict[str, str], forest_eq: Dict[str, str]) -> Dict[str, Any]:
        """
        Create a bridge between Lean and forest equations.
        """
        lean_domain = self.classify_equation_domain(lean_eq)
        forest_domain = self.classify_equation_domain(forest_eq)
        
        bridge = self.find_bridge(lean_domain, forest_domain)
        
        if bridge:
            bridge_record = {
                "bridge_id": bridge["id"],
                "bridge_name": bridge["name"],
                "lean_equation": lean_eq["Model_Name"],
                "forest_equation": forest_eq["name"],
                "lean_domain": lean_domain,
                "forest_domain": forest_domain,
                "connection_type": "direct"
            }
        else:
            # Indirect bridge via intermediate domain
            bridge_record = {
                "bridge_id": "INDIRECT",
                "bridge_name": f"{lean_domain} → {forest_domain}",
                "lean_equation": lean_eq["Model_Name"],
                "forest_equation": forest_eq["name"],
                "lean_domain": lean_domain,
                "forest_domain": forest_domain,
                "connection_type": "indirect"
            }
        
        self.bridges_created.append(bridge_record)
        return bridge_record
    
    def bridge_all(self, lean_equations: List[Dict[str, str]], 
                   forest_equations: List[Dict[str, str]]) -> List[Dict[str, Any]]:
        """
        Bridge all Lean equations with forest equations.
        """
        bridges = []
        
        # Create bridges based on intersections
        for lean_eq in lean_equations:
            for forest_eq in forest_equations:
                # Check if they should be bridged
                lean_name = lean_eq["Model_Name"].lower()
                forest_name = forest_eq["name"].lower()
                
                # Bridge based on domain classification
                lean_domain = self.classify_equation_domain(lean_eq)
                forest_domain = self.classify_equation_domain(forest_eq)
                
                # Only bridge if domains differ
                if lean_domain != forest_domain:
                    bridge = self.create_bridge(lean_eq, forest_eq)
                    bridges.append(bridge)
        
        return bridges


def main():
    """Bridge Lean analysis math with forest equations."""
    print("=" * 70)
    print("BRIDGE LEAN ANALYSIS MATH WITH FOREST")
    print("=" * 70)
    
    # Load Lean math equations
    print("\n[*] Loading Lean math equations...")
    with open('/home/allaun/Documents/Research Stack/data/lean_math_forest_import.json', 'r') as f:
        lean_data = json.load(f)
    
    lean_equations = lean_data["math_models"]
    print(f"    Loaded {len(lean_equations)} Lean equations")
    
    # Load forest equations
    print(f"\n[*] Loading forest equations...")
    forest_equations = []
    tsv_path = Path(__file__).resolve().parent.parent.parent / "3-Mathematical-Models" / "MATH_MODEL_MAP.tsv"
    with open(tsv_path, 'r') as f:
        lines = f.readlines()
        for line in lines[1:]:  # Skip header
            parts = line.strip().split('\t')
            if len(parts) >= 4:
                forest_equations.append({
                    "name": parts[1],
                    "family": parts[2],
                    "equation": parts[3],
                    "variables": parts[4]
                })
    
    print(f"    Loaded {len(forest_equations)} forest equations")
    
    # Create bridges
    print(f"\n[*] Creating bridges using Equation Forest bridge nodes...")
    bridge_system = ForestBridge()
    
    # Bridge Lean equations with forest equations
    bridges = bridge_system.bridge_all(lean_equations, forest_equations)
    
    print(f"    Created {len(bridges)} bridges")
    
    # Analyze bridges by type
    direct_bridges = [b for b in bridges if b["connection_type"] == "direct"]
    indirect_bridges = [b for b in bridges if b["connection_type"] == "indirect"]
    
    print(f"\n[*] Bridge Analysis:")
    print(f"    Direct bridges: {len(direct_bridges)}")
    print(f"    Indirect bridges: {len(indirect_bridges)}")
    
    # Show bridges by bridge node
    bridge_counts = {}
    for bridge in direct_bridges:
        bridge_id = bridge["bridge_id"]
        bridge_counts[bridge_id] = bridge_counts.get(bridge_id, 0) + 1
    
    print(f"\n[*] Direct Bridges by Node:")
    for bridge_id, count in sorted(bridge_counts.items()):
        bridge_name = ForestBridge.BRIDGES[bridge_id]["name"]
        print(f"    {bridge_id} ({bridge_name}): {count} bridges")
    
    # Show sample bridges
    print(f"\n[*] Sample Direct Bridges:")
    for bridge in direct_bridges[:10]:
        print(f"    {bridge['bridge_id']}: {bridge['lean_equation']} ↔ {bridge['forest_equation']}")
        print(f"        {bridge['lean_domain']} → {bridge['forest_domain']}")
    
    print(f"\n[*] Sample Indirect Bridges:")
    for bridge in indirect_bridges[:5]:
        print(f"    {bridge['lean_equation']} ↔ {bridge['forest_equation']}")
        print(f"        {bridge['lean_domain']} → {bridge['forest_domain']}")
    
    # Calculate bridge coverage
    lean_bridged = set(b["lean_equation"] for b in bridges)
    forest_bridged = set(b["forest_equation"] for b in bridges)
    
    print(f"\n[*] Bridge Coverage:")
    print(f"    Lean equations bridged: {len(lean_bridged)}/{len(lean_equations)} ({len(lean_bridged)/len(lean_equations)*100:.1f}%)")
    print(f"    Forest equations bridged: {len(forest_bridged)}/{len(forest_equations)} ({len(forest_bridged)/len(forest_equations)*100:.1f}%)")
    
    # Save results
    results = {
        "total_bridges": len(bridges),
        "direct_bridges": len(direct_bridges),
        "indirect_bridges": len(indirect_bridges),
        "bridge_counts": bridge_counts,
        "bridges": bridges,
        "coverage": {
            "lean_bridged": len(lean_bridged),
            "lean_total": len(lean_equations),
            "forest_bridged": len(forest_bridged),
            "forest_total": len(forest_equations)
        }
    }
    
    output_path = "/home/allaun/Documents/Research Stack/data/lean_math_forest_bridges.json"
    with open(output_path, 'w') as f:
        json.dump(results, f, indent=2)
    
    print(f"\n[*] Results saved to: {output_path}")
    
    print("\n" + "=" * 70)
    print("✅ LEAN MATH - FOREST BRIDGING COMPLETE")
    print("=" * 70)


if __name__ == "__main__":
    main()