proofs(P4): append_preserves_verified + build_chain_all_verified

[hyperpolymath]

Summary

Closes the P4 slot of the foundation-pack inventory (#77).

Adds 2 theorems + 1 supporting lemma to `formal/Provenance.v`:

Name	Kind	Statement
`mk_honest_verifies`	Lemma	`forall cnt h, record_verify (mk_honest cnt h)`
`append_preserves_verified` (P4)	Theorem	`Forall record_verify c -> Forall record_verify (append_record c cnt)`
`build_chain_all_verified` (P4)	Theorem	`forall cnts, Forall record_verify (build_chain cnts)`

Foundation pack status post-P4

#	Theorem	Module	Status
P2	record_verify_iff_unchanged	Provenance.v	✓
P3	chain_linked_step + chain_linked	Provenance.v	✓
P4	append_preserves_verified + build_chain_all_verified	Provenance.v	this PR
D1	drift_score_in_unit_interval	Drift.v	✓
D2	detect_drift_sound/complete	Drift.v	✓
C2	txn_state_machine_well_formed	Transaction.v	✓
C7	wal_replay_idempotent	WAL.v	✓
N2	normalize_idempotent	Normalizer.v	✓
V2	vql_preservation	VCL.v	✓
Q1	planner_semantic_equivalence	PlannerSemantic.v	✓

With P4 landed: foundation pack 10/10 closed, all on Parameters only (zero axiom consumption).

Print Assumptions output (verified locally)

```
Axioms:
sha256 : content -> hash -> hash
hash : Type
genesis_hash : hash
content : Type
```

Both new theorems close on Parameters; `sha256_collision_resistant` axiom NOT consumed (reserved for later V8 uniqueness theorem).

Test plan

• CI `Coq Build Oracle` job green (compile + Provenance assumptions whitelist passes)
• No new axioms in `Print Assumptions` output

Local: PASS (`coqc 8.18.0`, Ubuntu apt-installed).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 238 issues detected

Severity	Count
🔴 Critical	18
🟠 High	53
🟡 Medium	167

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "build-validation.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action dtolnay/rust-toolchain@stable needs attention",
    "type": "unpinned_action",
    "file": "build-validation.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action Swatinem/rust-cache@v2 needs attention",
    "type": "unpinned_action",
    "file": "build-validation.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "build-validation.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action erlef/setup-beam@v1 needs attention",
    "type": "unpinned_action",
    "file": "build-validation.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/checkout@v6 needs attention",
    "type": "unpinned_action",
    "file": "elixir-ci.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action erlef/setup-beam@v1 needs attention",
    "type": "unpinned_action",
    "file": "elixir-ci.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/cache@v5 needs attention",
    "type": "unpinned_action",
    "file": "elixir-ci.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action tions/checkout@v6\n  needs attention",
    "type": "unpinned_action",
    "file": "elixir-ci.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action lef/setup-beam@v1\n  needs attention",
    "type": "unpinned_action",
    "file": "elixir-ci.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence