Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The full finite named family

Abstract

Finite canonical native branching before free-shape unification

X is the entire declared finite family of names, represented by a presentation p. An Equation is a primitive definition z=T(n), a native shift definition z=rho to power a of x, an ordered pair definition z=pair(x,y), or an equality x=y. Every occurrence of a name refers to the same original source value. Unused declared names remain in X. Source consists of arbitrary finite ordered Boolean trees, and rho is the actual native substitution, not a free unary symbol. In the display, canonicalCodes(v)(x)=encode(v(x)), canonicalShapes(v)(x)=shape(encode(v(x))), NativeHolds is Equation.Holds, and BranchHolds is BranchEquation.Holds.

Definition 1.1 (Executable finite constructor choices).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branches

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branches (✓ std3).

Source. Repository-derived.

Commentary.

choices retains primitive, shift and equality equations. For each pair definition it offers exactly an ordinary case and a collapse case. branches forms their finite ordered product over the whole input list, retaining repeated constraints. An ordinary case requires the output code to be the pair of its input codes. A collapse case requires input ranks r+1 and r and output rank r+2 for some unrestricted natural r. That rank is not enumerated or bounded. Every code in the theorem is the actual canonical encode of the same original valuation.

Definition 1.2 (Erase ranks only after selecting cases).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.shape

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.shape (✓ std3).

Source. Repository-derived.

Commentary.

shape replaces each primitive rank by one fixed free primitive leaf and preserves ordered pairs. Primitive definitions and collapse cases become primitive shape equalities. Shift definitions become equalities of shapes. An ordinary pair definition becomes a free binary constructor equation. No interpreted native power is sent to the free occurs check. The exact canonical branch equations are retained alongside these weaker free-shape equations.

Definition 1.3 (Retain the actual scalar and block offsets).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceOffsetEdges

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceOffsetEdges (✓ std3).

Source. Repository-derived.

Commentary.

The source comparison carrier traverses the selected branch equations before rank erasure. A shift edge carries its actual natural offset as an integer; ordinary and equality comparisons carry zero. Primitive and collapse equations contribute no residual edge because their residual-free comparisons are against primitive leaves, while their original scalar and collapse constraints remain in BranchEquation.Holds. The edge carrier retains every occurrence and every repeated comparison.

Definition 1.4 (Project the source offset carrier to undirected adjacency).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceOccurrenceEdges

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceOccurrenceEdges (✓ std3).

Source. Repository-derived.

Commentary.

Projecting an offset edge forgets only its numeric offset and keeps its two residual occurrences. The resulting list is the source graph adjacency generated by every ordinary, shift, equality, constant and collapse comparison. Collapse scalar equations are retained in the branch data even when their residual projection is empty.

Definition 1.5 (Connectivity of the actual source comparison graph).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceConnected

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.sourceConnected (✓ std3).

Source. Repository-derived.

Commentary.

sourceConnected is the equivalence closure of sourceOccurrenceEdges. Its vertices are the same total occurrenceVertices supplied by the MGU action, including isolated occurrences of unused names. It is defined from the source branch constructors and only then related to the free-shape graph.

Theorem 1.6 (Compose ambient rank translations).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.shift_add

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.shift_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

Successive nonnegative translations add their offsets at every primitive leaf and preserve ordered pairing.

Theorem 1.7 (Expand every selected code equation).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branch_sound

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branch_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every branch equation implies its original native equation after ambient expansion. This applies to arbitrary finite codes without a normality premise, using the native recurrence in the collapse case.

Theorem 1.8 (Every constructor choice has its original equation).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.choices_origin

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.choices_origin (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each primitive, shift and equality choice keeps its original equation; both the ordinary and collapse choices have the same native pairing equation as origin.

Theorem 1.9 (Exact finite branching of named native equations).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branches_exact

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.branches_exact (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite named native system holds at v exactly when one computed branch holds at the actual canonical encoding of v. This is the constructor-case component of native_branch_reduction, before free-shape unification.

Theorem 1.10 (Exact source-to-shape graph identification).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.source_comparison_graph_identification

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.source_comparison_graph_identification (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite selected branch and every total term assignment, the projected source comparison carrier is definitionally traversed over the same named terms as the shape equations. The proof checks each primitive, shift, ordinary, collapse and equality constructor: shift retains its integer offset, ordinary and equality retain their corresponding leaves, and constant or collapse comparisons project to no residual edge. Therefore the source adjacency list is exactly occurrenceEdges(shapeEquations B, s), with no dropped or added occurrence.

Theorem 1.11 (Actual source connectivity has one component per residual sort).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.source_connected_iff_sort

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.source_connected_iff_sort (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an actual successful free-shape MGU, sourceConnected on the source comparison carrier is equivalent, for all total vertices, to equality of residual sort. This is an exact application of the existing MGU occurrence theorem through the proved source graph identification; the source quantifiers retain every declared name, every occurrence and the original branch scalar/rank constraints.

Theorem 1.12 (Exact canonical branching with total MGU shape reconstruction).

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/Constructor/NativePositiveBranchReduction.native_branch_reduction (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every presentation p, finite named equation list E and entire original valuation v, all native equations hold exactly when there is a member B of the computed finite list branches(E) such that all canonical codes are normal, all exact code equations of B hold, and the actual free unifier of shapeEquations(B) succeeds. Evaluating its total action at the original canonical shapes returns the original shape at every declared name. Both the free-shape connectivity and the source comparison connectivity are equivalent to equality of residual sort, with the source graph retaining actual shift offsets and all branch scalar constraints. ListMem in the display denotes ordinary list membership; sort(x,p,y) is y.

Canonical encoding commutes with every actual native power. This follows by structural induction from the commutation of smart collapse with a common rank shift. At each pair, the two canonical input codes either have consecutive primitive ranks and collapse, or smart retains the ordinary pair. This gives a complete finite case selection. Conversely, expansion of each selected code equation gives its actual native equation, including the collapse identity. Erasing ranks then supplies a ground solution of every selected free-shape equation. Existing unification completeness gives the actual successful result, its restriction identity reconstructs all named shapes, and the exact residual-occurrence graph theorem gives the connected sort components.

This is the canonical case reduction for an already named finite system. It does not construct the naming program for arbitrary MixedExpr inputs, solve affine rank equalities, compute minimum block bases, return an executable list of unrestricted native image charts, reconstruct all native outputs from independent bases, or perform signed pullback. The exact code constraints in this intermediate reduction are not a synthesized positive image cover.

References