NF Deduplication Invariant

Address DAG construction is deduplication-invariant: identifying shared branches produces the same DAG regardless of order. Follows from Hyperfactorization uniqueness. NF-level analogue of NF-Confluence.

NF Deduplication Invariant

Summary

Address DAG construction is deduplication-invariant: identifying shared branches produces the same DAG regardless of order. Follows from Hyperfactorization uniqueness. NF-level analogue of NF-Confluence.

Statement

%
\label{cor:nf-dedup-invariant}
The Address DAG construction
(Definition~\ref{def:address-dag},
Chapter~\ref{ch:dimension-fibration})
is an invariant under deduplication.
That is, if two quadtree expansions
share the same index at some branch,
identifying (deduplicating) those branches
produces the same Address DAG
regardless of the order
in which deduplication is performed.

Proof / Justification

By the Hyperfactorization Theorem
(Theorem~\ref{thm:hyperfactorization}),
each index $X \in \tau\text{-Idx}$
has a \emph{unique} ABCD address.
The Address DAG is therefore canonically determined
by the \emph{set} of reachable indices,
independent of the traversal order
used to discover them.
If two quadtree branches share the same index $X$,
their ABCD addresses are identical
(by uniqueness),
so merging them produces the same DAG node
regardless of which branch is encountered first.

Source Context

• Registry source: book-01.jsonl line 243
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part05/ch24-hyperfactorization.tex lines 270-282

Lean / Formalization Notes

• Formalization: planned
• Module: None
• Name: None

Dependencies

• Canonical: I.T04, I.D24

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.