SilverSight/formal/SilverSight/PhiConsistency.lean

/-
PhiConsistency.lean — Ring 4: 6 consistency rules → ADMIT / QUARANTINE

phi.consistency.check_consistency() runs 6 structural checks on an equation
string and encodes each result as a single DNA base in Layer 4 of the 30-base
layout (bases 24-29):

  G = rule passed   T = rule failed   (no other base ever appears — Ring 3)

RULE_ORDER (phi.consistency.py line 47):
  0 → balanced_parens      (DNA pos 24) parenthesis depth never < 0, ends 0
  1 → valid_operator_order (DNA pos 25) no illegal consecutive op pairs
  2 → valid_variable_name  (DNA pos 26) no "1x"-style numeric-prefixed idents
  3 → no_empty_expression  (DNA pos 27) stripped input is non-empty
  4 → single_expression    (DNA pos 28) parses as one Python AST expr
  5 → defined_reference    (DNA pos 29) all Names: ≤2 chars, has '_', or
                                        is in KNOWN_MATH_NAMES

This ring does NOT re-implement the Python predicates in Lean.
It establishes the structural contract:
  • 6 named rules, each with a unique Layer 4 slot
  • Encoding: G = pass, T = fail (disjoint, total)
  • ADMIT ↔ all 6 slots are G
  • QUARANTINE ↔ some slot is T
  • ADMIT and QUARANTINE are mutually exclusive and exhaustive

Anti-drift: any reordering of RULE_ORDER, addition/removal of rules, or
change to the G/T encoding breaks this bridge before reaching Ring 5.
-/

import SilverSight.PhiDNALayout
import Mathlib.Tactic

namespace SilverSight.PhiConsistency

open HachimojiBase
open SilverSight.PhiDNALayout

-- ============================================================
-- §1  THE 6 RULES  (phi.consistency.RULE_ORDER)
-- ============================================================

/-- The 6 structural consistency rules checked by phi.consistency.
    Constructor order matches RULE_ORDER exactly (slot = constructor index). -/
inductive ConsistencyRule where
  | balanced_parens       -- slot 0: depth ≥ 0 throughout, ends at 0
  | valid_operator_order  -- slot 1: no illegal consecutive op pairs
  | valid_variable_name   -- slot 2: no numeric-prefixed identifiers
  | no_empty_expression   -- slot 3: stripped input is non-empty
  | single_expression     -- slot 4: parses as one Python AST expression
  | defined_reference     -- slot 5: all names ≤2 chars, '_'-bearing, or known
  deriving DecidableEq, Repr, Fintype

/-- Exactly 6 rules. -/
theorem rule_card : Fintype.card ConsistencyRule = 6 := by decide

-- ============================================================
-- §2  SLOT MAPPING (rule → Layer 4 offset in Fin 6)
-- ============================================================

/-- The Layer 4 slot (0-5) for each rule.  Offset is RULE_ORDER index. -/
def ConsistencyRule.slot : ConsistencyRule → Fin 6
  | .balanced_parens      => ⟨0, by omega⟩
  | .valid_operator_order => ⟨1, by omega⟩
  | .valid_variable_name  => ⟨2, by omega⟩
  | .no_empty_expression  => ⟨3, by omega⟩
  | .single_expression    => ⟨4, by omega⟩
  | .defined_reference    => ⟨5, by omega⟩

/-- The absolute DNA position (0-29) for each rule. -/
def ConsistencyRule.dnaPos (r : ConsistencyRule) : Fin 30 :=
  ⟨24 + r.slot.val, by omega⟩

/-- Rule slots are distinct: no two rules share a Layer 4 position. -/
theorem slot_injective : Function.Injective ConsistencyRule.slot := by
  intro a b h
  cases a <;> cases b <;> simp_all [ConsistencyRule.slot]

/-- DNA positions are distinct (follows from slot injectivity). -/
theorem dnaPos_injective : Function.Injective ConsistencyRule.dnaPos := by
  intro a b h
  apply slot_injective
  have hv : 24 + a.slot.val = 24 + b.slot.val := by
    have := congr_arg Fin.val h
    simpa [ConsistencyRule.dnaPos] using this
  exact Fin.ext (by omega)

/-- Every rule's DNA position is in Layer 4 (24 ≤ pos < 30). -/
theorem rule_in_layer4 (r : ConsistencyRule) :
    24 ≤ r.dnaPos.val ∧ r.dnaPos.val < 30 := by
  cases r <;> simp [ConsistencyRule.dnaPos, ConsistencyRule.slot]

-- ============================================================
-- §3  ENCODING
-- ============================================================

/-- Encode a rule outcome as a HachimojiBase.
    phi.consistency.py: "G" if ... else "T" (consistency_dna line). -/
def encodeRule : Bool → HachimojiBase
  | true  => G  -- pass
  | false => T  -- fail

/-- encodeRule is always binary (G or T). -/
theorem encodeRule_binary (b : Bool) : encodeRule b = G ∨ encodeRule b = T := by
  cases b <;> simp [encodeRule]

/-- G encodes pass. -/
@[simp] theorem encodeRule_true  : encodeRule true  = G := rfl

/-- T encodes fail. -/
@[simp] theorem encodeRule_false : encodeRule false = T := rfl

/-- encodeRule is injective (distinct outcomes → distinct bases). -/
theorem encodeRule_injective : Function.Injective encodeRule := by decide

-- ============================================================
-- §4  ADMIT AND QUARANTINE PREDICATES
-- ============================================================

/-- A layout is ADMITted iff every consistency rule passes (all Layer 4 = G). -/
def isAdmit (d : PhiLayout) : Prop :=
  ∀ r : ConsistencyRule, d.layer4 r.slot = G

/-- A layout is QUARANTINEd iff some consistency rule fails (some Layer 4 = T). -/
def isQuarantine (d : PhiLayout) : Prop :=
  ∃ r : ConsistencyRule, d.layer4 r.slot = T

-- ============================================================
-- §5  MUTUAL EXCLUSIVITY AND EXHAUSTIVENESS
-- ============================================================

/-- ADMIT and QUARANTINE are mutually exclusive.
    A layout cannot simultaneously have all G and some T in Layer 4. -/
theorem admit_not_quarantine (d : PhiLayout) : ¬(isAdmit d ∧ isQuarantine d) := by
  intro ⟨hadmit, r, hquar⟩
  have hG := hadmit r
  rw [hG] at hquar
  exact absurd hquar (by decide)

/-- Every layout is either ADMITted or QUARANTINEd (or both — but §5 shows not both).
    Proof: if not all rules pass, some rule fails. -/
theorem admit_or_quarantine (d : PhiLayout) : isAdmit d ∨ isQuarantine d := by
  by_cases h : isAdmit d
  · exact Or.inl h
  · right
    simp only [isAdmit, not_forall] at h
    obtain ⟨r, hr⟩ := h
    exact ⟨r, (layer4_binary d r.slot).resolve_left hr⟩

/-- The two predicates partition all PhiLayouts. -/
theorem admit_quarantine_partition (d : PhiLayout) :
    (isAdmit d ∧ ¬isQuarantine d) ∨ (¬isAdmit d ∧ isQuarantine d) := by
  rcases admit_or_quarantine d with ha | hq
  · left
    exact ⟨ha, fun hq => admit_not_quarantine d ⟨ha, hq⟩⟩
  · right
    exact ⟨fun ha => admit_not_quarantine d ⟨ha, hq⟩, hq⟩

-- ============================================================
-- §6  WITNESS: all-pass and one-fail layouts
-- ============================================================

/-- A fully-passing layout: all 6 bases are G. -/
def allPassLayout : PhiLayout :=
  mkPhiLayout (fun _ => G) (fun _ => G) (fun _ => G) (fun _ => true)

theorem allPass_isAdmit : isAdmit allPassLayout := by
  intro r
  simp only [PhiLayout.layer4, allPassLayout, mkPhiLayout]
  have h1 : ¬(24 + r.slot.val < 8)  := by have := r.slot.isLt; omega
  have h2 : ¬(24 + r.slot.val < 16) := by have := r.slot.isLt; omega
  have h3 : ¬(24 + r.slot.val < 24) := by have := r.slot.isLt; omega
  simp only [dif_neg h1, dif_neg h2, dif_neg h3, ite_true]

/-- A layout that fails only balanced_parens (slot 0). -/
def parensFailLayout : PhiLayout :=
  mkPhiLayout (fun _ => G) (fun _ => G) (fun _ => G)
    (fun i => i.val ≠ 0)

theorem parensFail_isQuarantine : isQuarantine parensFailLayout :=
  ⟨.balanced_parens, by
    simp only [PhiLayout.layer4, parensFailLayout, mkPhiLayout, ConsistencyRule.slot]
    norm_num [dif_neg (show ¬(24 + 0 < 8) by omega),
              dif_neg (show ¬(24 + 0 < 16) by omega),
              dif_neg (show ¬(24 + 0 < 24) by omega)]⟩

end SilverSight.PhiConsistency