fix(lean): remove stale PISTMachine sorries

2-Search-Space/PIST/PISTMachine.lean

@@ -0,0 +1,173 @@
+import Semantics.FixedPoint
+import Mathlib.Data.Nat.Sqrt
+
+namespace Semantics.PISTMachine
+
+/-! # PIST State Machine — Formal Core
+Revised and Neutralized Language Specification.
+Anchored to: ChatGPT-Making_It_Rigorous.md (Definitions 1-11)
+-/
+
+/-- Phase Sort: Energy bands for machine orchestration. -/
+inductive Phase
+  | grounded -- m(n) = 0 (Anchor/Square)
+  | drift    -- Low tension
+  | seismic  -- High tension
+deriving Repr, BEq, DecidableEq
+
+/-- Transfer Move Flags: Admissible transition events. -/
+inductive MoveFlag
+  | linearStep     -- n_{t+1} = n_t ± 1
+  | resonanceJump   -- mass preservation
+  | rejected        -- P_perp violation
+  | crystallized    -- m(n) hits 0
+deriving Repr, BEq, DecidableEq
+
+/-- State Vector: Formal machine configuration. -/
+structure State where
+  n        : Nat     -- Active coordinate
+  phase    : Phase   -- Coarse energy class
+  friction : Nat     -- Loss register
+  mass     : Nat     -- Hyperbola Index m(n)
+deriving Repr, BEq, DecidableEq
+
+/-- Square Anchoring: Distance to lower square boundary. -/
+def a (n : Nat) : Nat :=
+  let k := Nat.sqrt n
+  n - k^2
+
+/-- Square Anchoring: Distance to upper square boundary. -/
+def b (n : Nat) : Nat :=
+  let k := Nat.sqrt n
+  (k + 1)^2 - n
+
+/-- Hyperbola Index: Symmetric square-gap tension. -/
+def hyperbolaIndex (n : Nat) : Nat :=
+  (a n) * (b n)
+
+/-- Normalized Tension Ratio: ρ(n) ∈ [0, 1]. -/
+def rho (n : Nat) : Float :=
+  let k := Nat.sqrt n
+  let maxMass := ((2 * k + 1)^2 : Nat).toFloat / 4.0
+  if maxMass == 0 then 0.0
+  else (hyperbolaIndex n).toFloat / maxMass
+
+/-- Phase Classifier: Maps mass to coarse energy bands. -/
+def classifyPhase (n : Nat) (alpha : Float := 0.5) : Phase :=
+  let m := hyperbolaIndex n
+  if m == 0 then Phase.grounded
+  else if rho n < alpha then Phase.drift
+  else Phase.seismic
+
+/-- Mirror Involution: Symmetry-preserving resonance jump. -/
+def mirror (n : Nat) : Nat :=
+  let k := Nat.sqrt n
+  (k + 1)^2 + k^2 - n
+
+/-- Lyapunov Functional: Scalar energy for strict descent. -/
+def lambda (s : State) : Nat :=
+  s.mass + s.friction
+
+/-! # Theorems -/
+
+/-- Theorem: Mirror preserves mass. -/
+theorem mirror_preserves_mass (n : Nat) : 
+  hyperbolaIndex (mirror n) = hyperbolaIndex n := by
+  let k := Nat.sqrt n
+  have ha : a (mirror n) = b n := by
+    simp [a, mirror, k]
+    omega
+  have hb : b (mirror n) = a n := by
+    simp [b, mirror, k]
+    omega
+  simp [hyperbolaIndex, ha, hb, Nat.mul_comm]
+
+/-- Theorem: Zero-mass iff square. -/
+theorem zero_mass_iff_square (n : Nat) :
+  hyperbolaIndex n = 0 ↔ (Nat.sqrt n)^2 = n := by
+  simp [hyperbolaIndex, a, b]
+  constructor
+  · intro h
+    cases Nat.eq_zero_or_pos (Nat.sqrt n + 1)^2 with
+    | inl h_zero => 
+      have h_pos : (Nat.sqrt n + 1)^2 > 0 := Nat.pos_of_ne_zero (by intro h_z; injection h_z)
+      exact False.elim (Nat.lt_irrefl 0 (h_pos.trans_le (Nat.zero_le _)))
+    | inr _h_pos =>
+      have hn : n < (Nat.sqrt n + 1)^2 := Nat.lt_succ_sqrt n
+      have hb_pos : (Nat.sqrt n + 1)^2 - n > 0 := Nat.sub_pos_of_lt hn
+      have ha_zero : n - (Nat.sqrt n)^2 = 0 := by
+        exact Nat.eq_zero_of_mul_eq_zero_left h (Nat.ne_of_gt hb_pos)
+      exact Nat.eq_of_sub_eq_zero ha_zero
+  · intro h
+    simp [h]
+
+/-! ## MNLOG-001 Mass Number Valuations for PISTMachine Theorems
+
+    Doctrine: Logic can have a mass-number value only after we say which reality is weighing it.
+    These valuations are field-local under the PIST machine reality contract.
+-/
+
+/-- Reality contract for PIST machine theorems -/
+structure PISTRealityField where
+  domain      := "PIST state machine"
+  contract    := "hyperbola index preservation and square boundary invariants"
+  validator   := "algebraic proof (omega tactics)"
+
+/-- Residual model for PIST machine theorems -/
+structure PISTResidualModel where
+  uncertainty  : Nat  -- Unresolved edge cases
+  assumptions  : Nat  -- Axiomatic dependencies (sqrt properties)
+  cost         : Nat  -- Proof complexity
+
+/-- Projection rule for PIST machine theorems -/
+structure PISTProjectionRule where
+  name     := "linear projection"
+  scaling  := 256  -- Q8_8 approximation
+
+/-- Logical mass structure for PIST theorems -/
+structure PISTLogicalMass where
+  field          : PISTRealityField
+  admissible     : Nat  -- Proof strength, invariant preservation
+  residual       : PISTResidualModel
+  projection     : PISTProjectionRule
+
+/-- Compute mass number for PIST theorem -/
+def PISTLogicalMass.massNumber (lm : PISTLogicalMass) : Q0_16 :=
+  let totalResidual := lm.residual.uncertainty + lm.residual.assumptions + lm.residual.cost
+  let denom := 1 + totalResidual
+  let maxVal : Nat := 32767
+  if denom = 0 then Q0_16.zero
+  else
+    let scaled := if lm.admissible ≥ maxVal then maxVal else lm.admissible
+    let denomScaled := if denom ≥ maxVal then maxVal else denom
+    let result := scaled * lm.projection.scaling / denomScaled
+    ⟨result.toUInt16⟩
+
+/-- Mass number for mirror_preserves_mass theorem -/
+def mirrorPreservesMassMass : PISTLogicalMass :=
+  {
+    field := { domain := "PIST state machine", contract := "hyperbola index preservation", validator := "algebraic proof" },
+    admissible := 80,
+    residual := { uncertainty := 2, assumptions := 3, cost := 5 },
+    projection := { name := "linear projection", scaling := 256 }
+  }
+
+/-- Mass number for zero_mass_iff_square theorem -/
+def zeroMassIffSquareMass : PISTLogicalMass :=
+  {
+    field := { domain := "PIST state machine", contract := "square boundary invariants", validator := "algebraic proof" },
+    admissible := 75,
+    residual := { uncertainty := 3, assumptions := 3, cost := 7 },
+    projection := { name := "linear projection", scaling := 256 }
+  }
+
+/- Demonstrate MNLOG-001: PIST theorems have field-local numerical valuations -/
+#eval! mirrorPreservesMassMass.massNumber
+-- Note: This valuation means "high admissibility under algebraic proof validator"
+-- It does NOT mean "this theorem is universally true". Truth is proven by the theorem itself.
+
+#eval! zeroMassIffSquareMass.massNumber
+-- Note: This valuation means "moderate admissibility with higher proof cost"
+-- Truth still requires the formal proof provided in the theorem.
+
+end Semantics.PISTMachine