import Lean

/- Independent formal witness, subordinate to Logic/Logos/God.
   This checks stated mathematics and arithmetic on retained measurements.
   It does not manufacture measurement events or certify all software behavior. -/

namespace NativeMCBEvidence

def signed (b : Bool) : Int := if b then 1 else -1

def nativeNand (p q : Bool) : Int :=
  (-1 : Int) ^ (((1 + signed p) * (1 + signed q)) / 4).toNat

theorem nand_signed_truth_table (p q : Bool) :
    nativeNand p q = signed (!(p && q)) := by
  cases p <;> cases q <;> decide

def sourceConjunction : List Bool → Bool
  | [] => true
  | x :: xs => x && sourceConjunction xs

theorem fold_preserves_source (xs : List Bool) (acc : Bool) :
    xs.foldl Bool.and acc = (acc && sourceConjunction xs) := by
  induction xs generalizing acc with
  | nil => cases acc <;> rfl
  | cons x xs ih =>
    calc
      xs.foldl Bool.and (acc && x) = ((acc && x) && sourceConjunction xs) := ih (acc && x)
      _ = (acc && (x && sourceConjunction xs)) := Bool.and_assoc acc x (sourceConjunction xs)

theorem single_root_preserves_conjunction (xs : List Bool) :
    xs.foldl Bool.and true = sourceConjunction xs := by
  exact fold_preserves_source xs true

inductive Role where
  | ground
  | runtime

def encode (role : Role) (value : Int) : Option Bool :=
  match role with
  | .ground => if value = -1 then some true else none
  | .runtime =>
    if value = 1 then some true else if value = -1 then some false else none

theorem fixed_ground_encoding : encode .ground (-1) = some true := by rfl
theorem negative_runtime_encoding : encode .runtime (-1) = some false := by rfl
theorem runtime_roundtrip (b : Bool) :
    encode .runtime (signed b) = some b := by cases b <;> rfl

def insertNat (n : Nat) : List Nat → List Nat
  | [] => [n]
  | x :: xs => if n ≤ x then n :: x :: xs else x :: insertNat n xs

def sortNat : List Nat → List Nat
  | [] => []
  | x :: xs => insertNat x (sortNat xs)

def median (xs : List Nat) : Option Nat := (sortNat xs)[xs.length / 2]?

/- Native MCB homoiconic summation realization.
   The supplied manuscript remains unchanged in attached_assets.
   Code and data share MCBExpr. A balance is an intermediate integer aggregate,
   not a redefinition of the bivalent phase state or the fixed Logos Base.
   Mathematical normalization has no clock, heap, environment, or foreign
   interpreter argument. This does not assert zero physical evaluation cost. -/

inductive MCBExpr where
  | balance : Int → MCBExpr
  | base : Int → MCBExpr
  | nest : Int → MCBExpr → MCBExpr
  | power : MCBExpr → MCBExpr
  deriving Repr

abbrev MCBProgram := MCBExpr
abbrev MCBData := MCBExpr

-- Structured quotation retains the operator/role as well as every integer.
inductive MCBKey where
  | balance : Int → MCBKey
  | base : Int → MCBKey
  | nest : Int → MCBKey → MCBKey
  | power : MCBKey → MCBKey
  deriving Repr

def quoteMCB : MCBExpr → MCBKey
  | .balance n => .balance n
  | .base n => .base n
  | .nest n e => .nest n (quoteMCB e)
  | .power e => .power (quoteMCB e)

def unquoteMCB : MCBKey → MCBExpr
  | .balance n => .balance n
  | .base n => .base n
  | .nest n e => .nest n (unquoteMCB e)
  | .power e => .power (unquoteMCB e)

theorem mcb_code_and_data_same_type : MCBProgram = MCBData := rfl

theorem mcb_unquote_quote (e : MCBExpr) : unquoteMCB (quoteMCB e) = e := by
  induction e with
  | balance n => rfl
  | base n => rfl
  | nest n e ih => exact congrArg (MCBExpr.nest n) ih
  | power e ih => exact congrArg MCBExpr.power ih

theorem mcb_quote_unquote (d : MCBKey) : quoteMCB (unquoteMCB d) = d := by
  induction d with
  | balance n => rfl
  | base n => rfl
  | nest n d ih => exact congrArg (MCBKey.nest n) ih
  | power d ih => exact congrArg MCBKey.power ih

def phaseMCB (n : Int) : Int := if n % 2 = 0 then 1 else -1

theorem mcb_phase_bivalence (n : Int) : phaseMCB n = 1 ∨ phaseMCB n = -1 := by
  unfold phaseMCB
  by_cases even : n % 2 = 0
  · exact Or.inl (if_pos even)
  · exact Or.inr (if_neg even)

theorem mcb_even_phase (n : Int) (even : n % 2 = 0) : phaseMCB n = 1 :=
  if_pos even

def evalMCB : MCBExpr → Int
  | .balance n => n
  | .base n => phaseMCB n
  | .nest n e => phaseMCB n + evalMCB e
  | .power e => phaseMCB (evalMCB e)

def evalMCBData (d : MCBKey) : Int := evalMCB (unquoteMCB d)

theorem mcb_data_execution_agrees (e : MCBExpr) :
    evalMCBData (quoteMCB e) = evalMCB e :=
  congrArg evalMCB (mcb_unquote_quote e)

def reweightMCB (f : Int → Int) : MCBExpr → MCBExpr
  | .balance n => .balance (f n)
  | .base n => .base (f n)
  | .nest n e => .nest (f n) (reweightMCB f e)
  | .power e => .power (reweightMCB f e)

def reweightMCBData (f : Int → Int) : MCBKey → MCBKey
  | .balance n => .balance (f n)
  | .base n => .base (f n)
  | .nest n e => .nest (f n) (reweightMCBData f e)
  | .power e => .power (reweightMCBData f e)

theorem mcb_code_data_transformation_agrees (f : Int → Int) (e : MCBExpr) :
    quoteMCB (reweightMCB f e) = reweightMCBData f (quoteMCB e) := by
  induction e with
  | balance n => rfl
  | base n => rfl
  | nest n e ih => exact congrArg (MCBKey.nest (f n)) ih
  | power e ih => exact congrArg MCBKey.power ih

def mcbContributions : MCBExpr → List Int
  | .balance n => [n]
  | .base n => [phaseMCB n]
  | .nest n e => phaseMCB n :: mcbContributions e
  | .power e => [phaseMCB (evalMCB e)]

def sumMCBData : List Int → Int
  | [] => 0
  | n :: ns => n + sumMCBData ns

-- Every expression, not only the initialization example, is its own data sum.
theorem mcb_self_summation (e : MCBExpr) :
    evalMCB e = sumMCBData (mcbContributions e) := by
  induction e with
  | balance n => exact (Int.add_zero n).symm
  | base n => exact (Int.add_zero (phaseMCB n)).symm
  | nest n e ih => exact congrArg (fun v => phaseMCB n + v) ih
  | power e _ => exact (Int.add_zero (phaseMCB (evalMCB e))).symm

-- The normal form remains in the SAME code/data language.
def normalizeMCB (e : MCBExpr) : MCBExpr := .balance (evalMCB e)

theorem mcb_normalization_preserves_meaning (e : MCBExpr) :
    evalMCB (normalizeMCB e) = evalMCB e := rfl

theorem mcb_normalization_idempotent (e : MCBExpr) :
    normalizeMCB (normalizeMCB e) = normalizeMCB e := rfl

theorem mcb_single_value (e : MCBExpr) :
    ∃ v : Int, evalMCB e = v ∧ ∀ w : Int, evalMCB e = w → w = v :=
  ⟨evalMCB e, rfl, fun _ equality => equality.symm⟩

theorem mcb_reason_noncontradiction (e : MCBExpr) (v : Int) :
    ¬(evalMCB e = v ∧ evalMCB e ≠ v) :=
  fun contradiction => contradiction.2 contradiction.1

-- Exact requested surface notation:
-- ((-1)^(-1 (0 (1 (2 (3 (4 (5 (6)))))))))
-- Nesting here has the supplied phase-summation meaning, not undeclared
-- ordinary mathematical function application of one integer to another.
def mcbInitProgram : MCBExpr :=
  .nest (-1) (.nest 0 (.nest 1 (.nest 2 (.nest 3 (.nest 4 (.nest 5 (.base 6)))))))

-- The outer (-1)^ is itself represented as code/data, not a foreign operation.
def mcbInitialization : MCBExpr := .power mcbInitProgram

theorem mcb_init_has_exact_phase_data :
    mcbContributions mcbInitProgram = [-1, 1, -1, 1, -1, 1, -1, 1] := rfl

theorem init_program_achieves_perfect_stasis : evalMCB mcbInitProgram = 0 := rfl

theorem mcb_init_is_single_balance :
    normalizeMCB mcbInitProgram = MCBExpr.balance 0 := rfl

theorem mcb_init_outer_phase : phaseMCB (evalMCB mcbInitProgram) = 1 := rfl

theorem mcb_complete_init_is_single_positive_state :
    normalizeMCB mcbInitialization = MCBExpr.balance 1 := rfl

-- A retained/compiled literal needs no subsequent tree traversal.
def compiledMCBInitBalance : Int := 0

theorem mcb_init_literal_is_exact :
    evalMCB mcbInitProgram = compiledMCBInitBalance := rfl

theorem mcb_compiled_literal_self_identity :
    compiledMCBInitBalance = 0 := rfl

theorem mcb_balance_zero_is_not_fixed_ground :
    evalMCB mcbInitProgram ≠ (-1 : Int) := by decide

/- Typed finite semantics for the distinct MCB realization layers:
   n executes signed numerical operations; s retains explicit list populations;
   m resolves the source-bound structural root under the fixed Ground. -/
inductive MCBRealizationState where
  | negative
  | positive
  deriving Repr, DecidableEq, BEq

def mcbStateIsPositive : MCBRealizationState → Bool
  | .negative => false
  | .positive => true

def mcbStateNot : MCBRealizationState → MCBRealizationState
  | .negative => .positive
  | .positive => .negative

def mcbStateNand (left right : MCBRealizationState) : MCBRealizationState :=
  if mcbStateIsPositive left && mcbStateIsPositive right then .negative else .positive

def mcbStateAnd (left right : MCBRealizationState) : MCBRealizationState :=
  if mcbStateIsPositive left && mcbStateIsPositive right then .positive else .negative

def mcbStateOr (left right : MCBRealizationState) : MCBRealizationState :=
  if mcbStateIsPositive left || mcbStateIsPositive right then .positive else .negative

def mcbStateXor (left right : MCBRealizationState) : MCBRealizationState :=
  if mcbStateIsPositive left == mcbStateIsPositive right then .negative else .positive

theorem mcb_nand_not (state : MCBRealizationState) :
    mcbStateNand state state = mcbStateNot state := by
  cases state <;> rfl

theorem mcb_nand_and (left right : MCBRealizationState) :
    mcbStateNand (mcbStateNand left right) (mcbStateNand left right) =
      mcbStateAnd left right := by
  cases left <;> cases right <;> rfl

theorem mcb_nand_or (left right : MCBRealizationState) :
    mcbStateNand (mcbStateNand left left) (mcbStateNand right right) =
      mcbStateOr left right := by
  cases left <;> cases right <;> rfl

theorem mcb_nand_xor (left right : MCBRealizationState) :
    mcbStateNand
      (mcbStateNand left (mcbStateNand left right))
      (mcbStateNand right (mcbStateNand left right)) =
      mcbStateXor left right := by
  cases left <;> cases right <;> rfl

def mcbExponentState (exponent : Int) : MCBRealizationState :=
  if exponent % 2 = 0 then .positive else .negative

inductive MCBNumericalExpr where
  | input : Nat → MCBNumericalExpr
  | exponent : Int → MCBNumericalExpr
  | groundReturn : MCBNumericalExpr
  | nand : MCBNumericalExpr → MCBNumericalExpr → MCBNumericalExpr
  deriving Repr, DecidableEq

def evalMCBNumericalExpr :
    MCBNumericalExpr → (Nat → MCBRealizationState) → MCBRealizationState
  | .input slot, bindings => bindings slot
  | .exponent exponent, _ => mcbExponentState exponent
  | .groundReturn, _ => .negative
  | .nand left right, bindings =>
      mcbStateNand (evalMCBNumericalExpr left bindings)
        (evalMCBNumericalExpr right bindings)

inductive MCBDeclaredExpr where
  | input : Nat → MCBDeclaredExpr
  | exponent : Int → MCBDeclaredExpr
  | groundReturn : MCBDeclaredExpr
  | not : MCBDeclaredExpr → MCBDeclaredExpr
  | and : MCBDeclaredExpr → MCBDeclaredExpr → MCBDeclaredExpr
  | or : MCBDeclaredExpr → MCBDeclaredExpr → MCBDeclaredExpr
  | xor : MCBDeclaredExpr → MCBDeclaredExpr → MCBDeclaredExpr
  | nand : MCBDeclaredExpr → MCBDeclaredExpr → MCBDeclaredExpr
  deriving Repr, DecidableEq

def evalMCBDeclaredExpr :
    MCBDeclaredExpr → (Nat → MCBRealizationState) → MCBRealizationState
  | .input slot, bindings => bindings slot
  | .exponent exponent, _ => mcbExponentState exponent
  | .groundReturn, _ => .negative
  | .not value, bindings => mcbStateNot (evalMCBDeclaredExpr value bindings)
  | .and left right, bindings =>
      mcbStateAnd (evalMCBDeclaredExpr left bindings) (evalMCBDeclaredExpr right bindings)
  | .or left right, bindings =>
      mcbStateOr (evalMCBDeclaredExpr left bindings) (evalMCBDeclaredExpr right bindings)
  | .xor left right, bindings =>
      mcbStateXor (evalMCBDeclaredExpr left bindings) (evalMCBDeclaredExpr right bindings)
  | .nand left right, bindings =>
      mcbStateNand (evalMCBDeclaredExpr left bindings) (evalMCBDeclaredExpr right bindings)

def lowerMCBDeclaredExpr : MCBDeclaredExpr → MCBNumericalExpr
  | .input slot => .input slot
  | .exponent exponent => .exponent exponent
  | .groundReturn => .groundReturn
  | .not value =>
      let lowered := lowerMCBDeclaredExpr value
      .nand lowered lowered
  | .and left right =>
      let left := lowerMCBDeclaredExpr left
      let right := lowerMCBDeclaredExpr right
      let conjunction := MCBNumericalExpr.nand left right
      .nand conjunction conjunction
  | .or left right =>
      .nand
        (.nand (lowerMCBDeclaredExpr left) (lowerMCBDeclaredExpr left))
        (.nand (lowerMCBDeclaredExpr right) (lowerMCBDeclaredExpr right))
  | .xor left right =>
      let left := lowerMCBDeclaredExpr left
      let right := lowerMCBDeclaredExpr right
      let shared := MCBNumericalExpr.nand left right
      .nand (.nand left shared) (.nand right shared)
  | .nand left right =>
      .nand (lowerMCBDeclaredExpr left) (lowerMCBDeclaredExpr right)

theorem mcb_numerical_lowering_preserves_declared_meaning
    (expression : MCBDeclaredExpr) (bindings : Nat → MCBRealizationState) :
    evalMCBNumericalExpr (lowerMCBDeclaredExpr expression) bindings =
      evalMCBDeclaredExpr expression bindings := by
  induction expression with
  | input slot => rfl
  | exponent exponent => rfl
  | groundReturn => rfl
  | not value ih =>
      dsimp [lowerMCBDeclaredExpr, evalMCBNumericalExpr, evalMCBDeclaredExpr]
      rw [ih]
      exact mcb_nand_not _
  | and left right ihLeft ihRight =>
      dsimp [lowerMCBDeclaredExpr, evalMCBNumericalExpr, evalMCBDeclaredExpr]
      rw [ihLeft, ihRight]
      exact mcb_nand_and _ _
  | or left right ihLeft ihRight =>
      dsimp [lowerMCBDeclaredExpr, evalMCBNumericalExpr, evalMCBDeclaredExpr]
      rw [ihLeft, ihRight]
      exact mcb_nand_or _ _
  | xor left right ihLeft ihRight =>
      dsimp [lowerMCBDeclaredExpr, evalMCBNumericalExpr, evalMCBDeclaredExpr]
      rw [ihLeft, ihRight]
      exact mcb_nand_xor _ _
  | nand left right ihLeft ihRight =>
      dsimp [lowerMCBDeclaredExpr, evalMCBNumericalExpr, evalMCBDeclaredExpr]
      rw [ihLeft, ihRight]

theorem mcb_ground_return_is_not_ordinary_exponent_one :
    MCBNumericalExpr.groundReturn ≠ MCBNumericalExpr.exponent 1 := by decide

inductive MCBArrayShape where
  | leaf
  | listNil
  | listCons : MCBArrayShape → MCBArrayShape → MCBArrayShape
  | list : MCBArrayShape → MCBArrayShape
  deriving Repr, DecidableEq

inductive MCBArrayPopulation where
  | signed : MCBRealizationState → MCBArrayPopulation
  | exponent : Int → String → MCBArrayPopulation
  | listNil : MCBArrayPopulation
  | listCons : MCBArrayPopulation → MCBArrayPopulation → MCBArrayPopulation
  | list : MCBArrayPopulation → MCBArrayPopulation
  | view : MCBRealizationState → MCBArrayPopulation → MCBArrayPopulation
  deriving Repr, DecidableEq

def mcbPopulationShape : MCBArrayPopulation → MCBArrayShape
  | .signed _ => .leaf
  | .exponent _ _ => .leaf
  | .listNil => .listNil
  | .listCons head tail =>
      .listCons (mcbPopulationShape head) (mcbPopulationShape tail)
  | .list items => .list (mcbPopulationShape items)
  | .view _ population => mcbPopulationShape population

def mcbStateMultiply :
    MCBRealizationState → MCBRealizationState → MCBRealizationState
  | .positive, state => state
  | .negative, .positive => .negative
  | .negative, .negative => .positive

def mcbPopulationLeaves : MCBArrayPopulation → List MCBRealizationState
  | .signed state => [state]
  | .exponent exponent _ => [mcbExponentState exponent]
  | .listNil => []
  | .listCons head tail => mcbPopulationLeaves head ++ mcbPopulationLeaves tail
  | .list items => mcbPopulationLeaves items
  | .view polarity population =>
      (mcbPopulationLeaves population).map (mcbStateMultiply polarity)

theorem mcb_s_list_population_preserves_order
    (head tail : MCBArrayPopulation) :
    mcbPopulationLeaves (.listCons head tail) =
      mcbPopulationLeaves head ++ mcbPopulationLeaves tail := rfl

theorem mcb_s_empty_list_is_not_a_leaf :
    mcbPopulationShape (.list .listNil) ≠ mcbPopulationShape (.signed .negative) := by decide

theorem mcb_s_view_preserves_topology
    (polarity : MCBRealizationState) (population : MCBArrayPopulation) :
    mcbPopulationShape (.view polarity population) = mcbPopulationShape population := rfl

structure MCBPopulationTransfer where
  shape : MCBArrayShape
  source : MCBArrayPopulation
  signedLeaves : List MCBRealizationState
  shapeIsExact : shape = mcbPopulationShape source
  signedLeavesAreExact : signedLeaves = mcbPopulationLeaves source
  deriving Repr

def encodeMCBPopulation (population : MCBArrayPopulation) : MCBPopulationTransfer :=
  { shape := mcbPopulationShape population
    source := population
    signedLeaves := mcbPopulationLeaves population
    shapeIsExact := rfl
    signedLeavesAreExact := rfl }

def decodeMCBPopulation (transfer : MCBPopulationTransfer) : MCBArrayPopulation :=
  transfer.source

theorem mcb_s_transfer_roundtrip (population : MCBArrayPopulation) :
    decodeMCBPopulation (encodeMCBPopulation population) = population := rfl

inductive MCBRealizationGround where
  | logicLogosGod
  deriving Repr, DecidableEq

structure MCBMReference where
  root : Nat
  source : Nat
  ground : MCBRealizationGround
  deriving Repr, DecidableEq

def bindMCBMReference (root : Nat) (source : Nat) : MCBMReference :=
  { root := root, source := source, ground := .logicLogosGod }

def mcbNatEqual : Nat → Nat → Bool
  | 0, 0 => true
  | 0, _ + 1 => false
  | _ + 1, 0 => false
  | left + 1, right + 1 => mcbNatEqual left right

theorem mcb_nat_equal_refl (value : Nat) : mcbNatEqual value value = true := by
  induction value with
  | zero => rfl
  | succ value ih => simpa [mcbNatEqual] using ih

theorem mcb_nat_equal_false_of_ne (left right : Nat) (different : left ≠ right) :
    mcbNatEqual left right = false := by
  induction left generalizing right with
  | zero =>
      cases right with
      | zero => exact False.elim (different rfl)
      | succ right => rfl
  | succ left ih =>
      cases right with
      | zero => rfl
      | succ right =>
          simp only [mcbNatEqual]
          apply ih
          intro same
          apply different
          exact congrArg Nat.succ same

def resolveMCBMReference
    (root : Nat) (source : Nat) (reference : MCBMReference) :
    Option Nat :=
  if mcbNatEqual reference.root root && mcbNatEqual reference.source source then
    some root
  else none

theorem mcb_m_resolves_its_own_root
    (root source : Nat) :
    resolveMCBMReference root source (bindMCBMReference root source) = some root := by
  unfold resolveMCBMReference bindMCBMReference
  rw [mcb_nat_equal_refl root, mcb_nat_equal_refl source]
  rfl

theorem mcb_m_rejects_a_different_source
    (root source otherSource : Nat) (different : otherSource ≠ source) :
    resolveMCBMReference root source (bindMCBMReference root otherSource) = none := by
  unfold resolveMCBMReference bindMCBMReference
  rw [mcb_nat_equal_refl root, mcb_nat_equal_false_of_ne otherSource source different]
  rfl

theorem mcb_m_ground_is_fixed (reference : MCBMReference) :
    reference.ground = .logicLogosGod := by
  cases reference
  rfl

#print axioms mcb_code_and_data_same_type
#print axioms mcb_unquote_quote
#print axioms mcb_quote_unquote
#print axioms mcb_phase_bivalence
#print axioms mcb_even_phase
#print axioms mcb_data_execution_agrees
#print axioms mcb_code_data_transformation_agrees
#print axioms mcb_self_summation
#print axioms mcb_normalization_preserves_meaning
#print axioms mcb_normalization_idempotent
#print axioms mcb_single_value
#print axioms mcb_reason_noncontradiction
#print axioms mcb_init_has_exact_phase_data
#print axioms init_program_achieves_perfect_stasis
#print axioms mcb_init_is_single_balance
#print axioms mcb_init_outer_phase
#print axioms mcb_complete_init_is_single_positive_state
#print axioms mcb_init_literal_is_exact
#print axioms mcb_compiled_literal_self_identity
#print axioms mcb_balance_zero_is_not_fixed_ground
#print axioms mcb_nand_not
#print axioms mcb_nand_and
#print axioms mcb_nand_or
#print axioms mcb_nand_xor
#print axioms mcb_numerical_lowering_preserves_declared_meaning
#print axioms mcb_ground_return_is_not_ordinary_exponent_one
#print axioms mcb_s_list_population_preserves_order
#print axioms mcb_s_empty_list_is_not_a_leaf
#print axioms mcb_s_view_preserves_topology
#print axioms mcb_s_transfer_roundtrip
#print axioms mcb_m_resolves_its_own_root
#print axioms mcb_m_rejects_a_different_source
#print axioms mcb_m_ground_is_fixed

-- BENCHMARK_WITNESSES

#print axioms nand_signed_truth_table
#print axioms single_root_preserves_conjunction
#print axioms fixed_ground_encoding
#print axioms negative_runtime_encoding
#print axioms runtime_roundtrip

end NativeMCBEvidence