feat: L-S48 MultiDieAggCorrect.v — 8-die merkle aggregation correctness proof (Wave-13b)

[gHashTag]

Closes #803

L-S48 Multi-Die Aggregation Correctness Proof (Wave-13b)

PhD anchor: φ² + φ⁻² = 3 | DOI: 10.5281/zenodo.19227877

Coq Proof Summary

File: docs/phd/theorems/igla/MultiDieAggCorrect.v

Pattern: Opaque Parameter hash_combine + congruence (Wave-12c style) — keeps proof O(1).

Theorems proved:

1. super_root_deterministic

   • forall leaves leaves', leaves = leaves' -> super_root leaves = super_root leaves'
   • Proof: subst; congruence

2. super_root_assoc_layers

   • 3-stage layered reduction (8→4→2→1) is definitionally equal to flat hash expansion
   • Proof: unfold definitions + congruence

3. super_root_refl (corollary)

Verification

coqc MultiDieAggCorrect.v
Exit: 0   (coqc 8.20.1, no Admitted, ends Qed.)

RTL Citation

• Repo: gHashTag/tt-trinity-gf16
• File: src/multi_die_reducer.v
• Sim: MULTI_DIE_REDUCER_GREEN (88/88 PASS)

Files

File	Description
docs/phd/theorems/igla/MultiDieAggCorrect.v	Coq proof, 3 theorems, opaque hash + congruence
docs/phd/artifacts/coq_citation_map.json	Maps MultiDieAggCorrect.v → multi_die_reducer.v

Topology Note

The 3-stage merkle tree maps exactly to RTL pipeline:

Stage 0: 8 leaves → 4 nodes (hash_combine pairs)
PipeReg1: latch 4 nodes
Stage 1: 4 nodes → 2 nodes
PipeReg2: latch 2 nodes
Stage 2: 2 nodes → super-root
OutReg: latch super-root

Author: Dmitrii Vasilev admin@t27.ai
Apache-2.0