allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-12 02:20:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): remove stale PISTMachine sorries

Browse source
This commit is contained in:
Allaun Silverfox 2026-05-26 14:29:04 -05:00
parent aeb98c4166
commit 088307d997
1 changed files with 27 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
2-Search-Space/PIST/PISTMachine.lean
View file

@ -73,14 +73,33 @@ def lambda (s : State) : Nat :=
/-- Theorem: Mirror preserves mass. -/ /-- Theorem: Mirror preserves mass. -/
theorem mirror_preserves_mass (n : Nat) : theorem mirror_preserves_mass (n : Nat) :
hyperbolaIndex (mirror n) = hyperbolaIndex n := by hyperbolaIndex (mirror n) = hyperbolaIndex n := by
-- TODO(lean-port): Prove mirror preserves hyperbolaIndex. let k := Nat.sqrt n
sorry 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. -/
theorem zero_mass_iff_square (n : Nat) : theorem zero_mass_iff_square (n : Nat) :
hyperbolaIndex n = 0 ↔ (Nat.sqrt n)^2 = n := by hyperbolaIndex n = 0 ↔ (Nat.sqrt n)^2 = n := by
-- TODO(lean-port): Complete zero_mass_iff_square equivalence proof. simp [hyperbolaIndex, a, b]
sorry 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 /-! ## MNLOG-001 Mass Number Valuations for PISTMachine Theorems
@ -128,8 +147,8 @@ def PISTLogicalMass.massNumber (lm : PISTLogicalMass) : Q0_16 :=
def mirrorPreservesMassMass : PISTLogicalMass := def mirrorPreservesMassMass : PISTLogicalMass :=
{ {
field := { domain := "PIST state machine", contract := "hyperbola index preservation", validator := "algebraic proof" }, field := { domain := "PIST state machine", contract := "hyperbola index preservation", validator := "algebraic proof" },
admissible := 80, -- Strong invariant: mass preservation is core property admissible := 80,
residual := { uncertainty := 2, assumptions := 3, cost := 5 }, -- Moderate proof complexity residual := { uncertainty := 2, assumptions := 3, cost := 5 },
projection := { name := "linear projection", scaling := 256 } projection := { name := "linear projection", scaling := 256 }
} }
@ -137,8 +156,8 @@ def mirrorPreservesMassMass : PISTLogicalMass :=
def zeroMassIffSquareMass : PISTLogicalMass := def zeroMassIffSquareMass : PISTLogicalMass :=
{ {
field := { domain := "PIST state machine", contract := "square boundary invariants", validator := "algebraic proof" }, field := { domain := "PIST state machine", contract := "square boundary invariants", validator := "algebraic proof" },
admissible := 75, -- Strong invariant: characterizes grounded phase admissible := 75,
residual := { uncertainty := 3, assumptions := 3, cost := 7 }, -- Higher proof complexity residual := { uncertainty := 3, assumptions := 3, cost := 7 },
projection := { name := "linear projection", scaling := 256 } projection := { name := "linear projection", scaling := 256 }
} }