SilverSight/python/phi/consistency.py
allaun 1794299a6c chore(quality): native_decide migration, docs, and phi pipeline cleanup
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)
2026-06-27 01:56:54 -05:00

104 lines
3.5 KiB
Python

"""
phi.consistency — Layer 4: 6 consistency rules → ADMIT / QUARANTINE
Each equation is checked against 6 rules. All must pass for the
equation to be ADMITted. The results are embedded in the DNA as
G (pass) / T (fail) bases for allele-specific PCR filtering.
Dependencies: phi.ast_parse (for tree-based checks).
"""
from __future__ import annotations
import ast
import re
from typing import Dict, Optional
from .ast_parse import parse_to_ast
# ── Well-known math function names (considered "defined references") ─────
KNOWN_MATH_NAMES = frozenset({
"sin", "cos", "tan", "log", "ln", "exp", "sqrt", "abs", "sum",
"min", "max", "floor", "ceil", "round", "sign", "arg", "norm",
"det", "trace", "tr", "diag", "vec", "mat", "rank", "dim",
"arccos", "arcsin", "arctan", "sinh", "cosh", "tanh",
"Re", "Im", "conj", "adj", "trans", "id",
})
# ── The 6 rules ──────────────────────────────────────────────────────────
CONSISTENCY_RULES = [
"balanced_parens", # Rule 1: parentheses must be balanced
"valid_operator_order", # Rule 2: no illegal consecutive operators
"valid_variable_name", # Rule 3: identifiers start with letter/underscore
"no_empty_expression", # Rule 4: equation is non-empty
"single_expression", # Rule 5: parseable as single AST expression
"defined_reference", # Rule 6: all names are known or short vars
]
RULE_ORDER = list(CONSISTENCY_RULES)
def check_consistency(equation: str) -> Dict[str, bool]:
"""Check all 6 consistency rules.
Returns dict of rule_name → True/False.
All True = ADMIT; any False = QUARANTINE.
"""
result: Dict[str, bool] = {}
# ── Rule 1: Balanced parentheses ──
depth = 0
for c in equation:
if c == "(":
depth += 1
elif c == ")":
depth -= 1
if depth < 0:
break
result["balanced_parens"] = depth == 0
# ── Rule 2: No illegal consecutive operators ──
ops = set("+-*/^=<>!")
valid_pairs = frozenset({"<=", ">=", "==", "!=", "**"})
bad = False
for i in range(len(equation) - 1):
pair = equation[i:i+2]
if equation[i] in ops and equation[i + 1] in ops:
if pair not in valid_pairs:
bad = True
break
result["valid_operator_order"] = not bad
# ── Rule 3: Identifiers start with letter or underscore ──
tokens = re.findall(r"[A-Za-z_]\w*|\d+|[^\w\s]", equation)
bad_vars = any(
re.match(r"^\d", t) and not re.match(r"^\d+$", t)
for t in tokens
)
result["valid_variable_name"] = not bad_vars
# ── Rule 4: Non-empty ──
result["no_empty_expression"] = len(equation.strip()) > 0
# ── Rule 5: Parseable as single expression ──
tree = parse_to_ast(equation)
result["single_expression"] = tree is not None
# ── Rule 6: All names are known or short ──
result["defined_reference"] = True
if tree is not None:
for node in ast.walk(tree):
if isinstance(node, ast.Name):
name = node.id
allowed = (
len(name) <= 2
or name.startswith("_")
or "_" in name
or name in KNOWN_MATH_NAMES
)
if not allowed:
result["defined_reference"] = False
return result