Guarded rank-only navigation and records
Abstract
NativeRankedNavigationCompiler
Theorem 1.1 (A finite Presburger formula for all rank-only records).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeRankedNavigationCompiler.rank_only_refinement_compilation (✓ std3). ∎
Source. Repository-derived.
Commentary.
Source is the ordered free binary magma with alpha labelled true and beta labelled false. Native substitution sends alpha to beta and beta to the ordered pair of beta and alpha. Write T(r) for its r-th iterate at alpha. Thus T(0) is alpha, T(1) is beta, and T(r+2) has left child T(r+1) and right child T(r). False address edges go left and true edges go right.
Endpoint(k) contains a residual-free RankedExpr(k,0), a fixed natural epoch, and an arbitrary fixed finite address. The original rank tuple n maps Fin(k) to the natural numbers. A scalar occurrence with decoration a evaluates to T(n(j)+a); every repeated occurrence retains the same j. Grounds are actual fixed finite trees and explicit pairs retain their ordered structure. An endpoint tree is the epoch-th substitution iterate of rankedEval(n,Fin.elim0,expression). No residual tree variables occur.
pathCost is zero for the empty address. Prepending a left edge adds one; prepending a right edge adds two. pathThreshold is zero for the empty address. Prepending an edge of cost d gives max(2,d+pathThreshold(tail)). Native path induction proves that subtree(p,T(t)) is some u exactly when there is a natural r with pathThreshold(p) at most t, t=r+pathCost(p), and T(r)=u. The maximum retains every intermediate branch requirement. In particular, the final left edge requires starting index at least two: index one is a beta leaf even though subtracting one would yield a natural number. No truncated subtraction interprets an impossible path.
atEpoch distributes the fixed substitution power through the finite syntax. A ground is substituted literally, and each scalar decoration increases by the epoch. navigate then follows explicit pairs and actual fixed grounds until the address ends, becomes absent, or enters a scalar atom with a remaining suffix. navigationValue agrees with actual subtree navigation for every unbounded original rank tuple, including endpoints born after substitution.
For a reached atomic suffix introduce a fresh natural endpoint index r. guardFormula conjoins its exact threshold and the equation n(j)+a=r+pathCost(p). A constant lower bound h is a finite conjunction excluding indices 0 through h-1, which bounds the syntax construction without bounding the variable rank. Whole-expression endpoints have a true guard and absent endpoints have a false guard. reachedExpr keeps the complete reached expression, preserving all original rank names, or uses the fresh atomic endpoint index. The existing ranked_equality_compilation theorem supplies exact whole native equality, including equality between a ranked atom and an explicit pair.
Record(k) is either a literal endpoint and retained Reply or a positive link between two endpoints. RecordHolds(n,literal(a,y)) states exact native readout equality to y. Its four possible replies are alpha, beta, branch and absent. Absence negates endpoint reachedness. Each other reply requires a reached endpoint; alpha and beta compare its whole subtree with the corresponding leaf, while branch excludes both leaves. RecordHolds(n,link(a,b)) requires actual subtrees some u and some v at both endpoints and u=v. linkFormula conjoins both independent reach guards and equality of the complete reached expressions before existentially binding their two fresh natural indices.
refinementFormula maps the finite record list to its exact formulas and conjoins them. Every original scalar coordinate remains free; only fresh endpoint indices are existentially bound. Its realization at any one shared n is equivalent to every RecordHolds(n,r) in the list. Empty lists produce top. Zero rank dimensions, root addresses, empty suffixes, both leaf labels, fixed ground exterior pieces, repeated records and rank names, and links at distinct fixed epochs are included. The construction is computable finite first-order Presburger syntax. It does not require quantifier elimination, a general decision procedure, a rank bound or a complexity bound.
This is the native rank-only refinement interpretation of URR Definition 4.4, using the arithmetic navigation route in CAR Lemma 4.1. The result is a repository-derived connection to the existing native subtree, readout and ranked equality definitions. It concerns literal records and positive links on residual-free endpoints. Complete chart supports, global address translation and quantified arithmetic decisions are separate results. The complete-row application below composes the native navigation and equality results with depth patterns and symbolic recutting. An external rank policy may restrict the family further when supplied with its own arithmetic interpretation; it asserts no additional acquired rank port or physical operation.
Complete-row application of the existing native results.
Complete rows at independent rank tuples. Let E be a residual-free RankedExpr(k,0), F a residual-free RankedExpr(l,0), and Q any fixed finite prefix-free cut. The literalRecord of a source consists of its entire address-labelled cut exterior and the finite relation of all reached-hole pairs whose complete native subtrees agree. Renaming the original coordinates of E by Fin.castAdd(l) and of F by Fin.natAdd(k) gives one free tuple on Fin(k+l). These embeddings keep each repeated original coordinate shared. The finite construction below yields a first-order natural-number Presburger formula whose realization at Fin.addCases(n,m) is exactly equality of these two actual literal records, for every independently arbitrary n and m.
Choose d=1+cutDepth(Q). NativeWholeRowService.patternList enumerates every depth-d pattern, including early Boolean leaves and the depth-zero frontier. Its frontierList enumerates exactly the reached frontier positions. Deduplicated list indices give computable frontier and branch names; sorted cut addresses give hole-marker names with an explicit decoder. A branch pair has one finite fresh-rank slot for each of its frontier positions. For each position, navigate_value identifies navigation with the original source subtree. guard_realize and navigation_witness give the exact guard and reachedExpr, preserving the whole expression when the address stops in explicit syntax, absence when blocked, and a guarded fresh atomic rank after entering an atomic suffix. A frontier may be a compound native tree; it is never required to be one ranked atom.
For each branch conjoin all frontier guards and two ranked_equality_compilation instances asserting that the original sources equal their complete filled patterns. These reconstruction equalities certify early leaves and all finite branch choices. depthEquiv and frontier_geometry supply the actual branch and its fresh ranks in the converse direction. pattern_evaluate connects expression substitution to complete pattern filling, and pattern_deep derives the needed depth condition internally. Since every Q address has length below d, symbolic_recut_exact identifies each complete symbolic record with literalRecord on the same original source. No DeepAt premise on that source is imposed, and every uncut frontier value remains an unrestricted complete native tree.
For exterior comparison, treat only address-labelled cut holes as a finite alphabet of residual names. Substitute each actual frontier expression into the corresponding symbolic exterior; Boolean leaves and ordered pairs retain their native meanings. The explicit marker decoder has a left inverse at every address in Q, so renaming markers preserves and reflects exterior equality. simultaneous_ground_separation identifies equality of the resulting finite marker terms with equality under all native marker valuations. uniform_residual_reflection selects one separator from the fixed exterior expression pair before any original or fresh rank tuple is supplied. ranked_equality_compilation at that fixed separator therefore gives exact marked-exterior equality simultaneously at every unbounded extended rank tuple. It preserves the entire uncut exterior, including arbitrarily large atomic and compound pieces.
For the partition, conjoin membership equivalence for every pair in Q times Q. Each membership test retains both symbolic reached-hole guards and whole-subtree equality. There are no partition entries outside this finite product. Thus the biconditionals preserve both equality and disequality among reached holes, as well as diagonal reachedness. Combine the exterior and partition formulas, existentially bind only the finite fresh-rank block using relabel and exs, and take a finite disjunction over the explicit pattern-pair lists. These are computable finite syntax operations; original ranks remain free and unbounded. Empty Q compares whole sources through their exteriors, while the singleton root cut gives the same one-hole row for every source.
A supplied concrete source is handled by a fixed ground expression on the other side. For an arbitrary supplied finite canonical LiteralRow C, first collect the numeric class names that actually occur. Fill each name with a distinct finite native code, using code_injective, to obtain a concrete representative W. legal_values_row proves that C is realizable at Q exactly when canonicalRow(Q,W)=C. This is a finite decidable normalization test, not an added realizability hypothesis: failure produces the false formula; success compares with W and uses canonicalRow_record_iff to retain the entire exterior, partition and supplied canonical numbering. For a root cut, class zero passes this test and a sole class-one marker fails.
This application is a composition of existing results and explicit finite Presburger syntax construction for CAR Lemma 4.1 items 3 and 4. It introduces no new mathematical compiler declaration. Source grounds, addresses, cut sets and expressions are fixed finite inputs; all original rank dimensions, rank-zero and rank-one cases, missing addresses, repeated coordinates, empty cuts and root cuts are included. The construction has no general quantifier-elimination or formula decision procedure, physical observer or action realization, chart-support, complexity or memory bound, or literature-originality claim. Prefix-freeness remains a hypothesis of the native row correspondence.