-- ============================================================
-- OMEGA Protocol v1.4.1 canonical predicate definition
-- P14 Predicate Commitment added as the first conjunct.
-- ============================================================

structure PredicateCommitment where
  predicate_version : String
  predicate_hash : String
  attestation_method : String
  attestation_hash : String

def P14 (pc : PredicateCommitment) : Prop :=
  pc.predicate_version ≠ "" ∧
  pc.predicate_hash ≠ "" ∧
  pc.attestation_method ≠ "" ∧
  pc.attestation_hash ≠ ""

variable
  (pc : PredicateCommitment)
  (P1 : Prop)   -- Governance
  (P2 : Prop)   -- Reasoning
  (P3 : Prop)   -- Traceability
  (P4 : Prop)   -- Expectation
  (P4M : Prop)  -- Materiality Binding
  (P4T : Prop)  -- Trajectory Expectation
  (P5 : Prop)   -- Confirmation
  (P5E : Prop)  -- Execution Attestation
  (P6 : Prop)   -- Delegation
  (P6A : Prop)  -- Aggregate Materiality
  (P6L : Prop)  -- Liability Threshold
  (PCF : Prop)  -- Continuity-Formal
  (P10 : Prop)  -- Competence Attestation
  (P11 : Prop)  -- Expectation Update Integrity
  (P12 : Prop)  -- Semantic Integrity Validation
  (FAH : Prop)  -- Accountability Horizon honest limit acknowledgement
  (FAA : Prop)  -- Attestation Authority Integrity honest limit acknowledgement
  (P2_DAG : Prop)
  (P6_AtomicAgency : Prop)
  (P1_Freshness : Prop)
  (P4T_EnvInvariant : Prop)

def GovernedV14Core :=
  P1 ∧ P2 ∧ P3 ∧ P4 ∧ P4M ∧ P4T ∧ P5 ∧ P5E ∧ P6 ∧ P6A ∧ P6L ∧ PCF ∧
  P10 ∧ P11 ∧ P12 ∧ FAH ∧ FAA ∧
  P2_DAG ∧ P6_AtomicAgency ∧ P1_Freshness ∧ P4T_EnvInvariant

def Governed :=
  P14 pc ∧
  GovernedV14Core P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
    P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant

theorem p14_necessary :
    Governed pc P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant →
    P14 pc :=
  fun h => h.1

theorem all_twentytwo_conjuncts_sufficient
    (p14 : P14 pc)
    (core : GovernedV14Core P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant) :
    Governed pc P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant :=
  ⟨p14, core⟩

theorem governed_iff_p14_and_v14_core :
    Governed pc P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant ↔
    P14 pc ∧
    GovernedV14Core P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant :=
  Iff.rfl

theorem primitive_claims_resolve_against_committed_predicate :
    Governed pc P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
      P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant →
    P14 pc :=
  p14_necessary pc P1 P2 P3 P4 P4M P4T P5 P5E P6 P6A P6L PCF
    P10 P11 P12 FAH FAA P2_DAG P6_AtomicAgency P1_Freshness P4T_EnvInvariant

-- The authorisation condition is now predicate-bound:
-- A(α,π) = P14(π) ∧ GovernedV14Core(α)
-- Silence is the result.