Complete native fresh-sensor sector
Abstract
One actual native execution binds the complete rational sector to its material and genuine raw designated sensors.
Theorem 1.1 (Same-execution material, raw bindings and all-time sector).
Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Geometry/NativeFreshSensorAcquisition.complete_native_sector (✓ std3). ∎
Source. Repository-derived.
Commentary.
The original t is any finite native Source satisfying D, the original LAB birth condition. The conclusion applies in particular to every earned branching source with at least three original leaves and every positive finite disjoint beta-cherry family. No Positive-image assumption is added. Cherries records literal beta-beta subtrees and disjoint cones; vector at offsets empty,L,LL,LLL,R,LR gives a,b,c,d,e,f, and half=(a-c)/2. All equations hold at every ambient address. The operation B is the actual native neighbor sum of grown(t), not a supplied matrix. Observation is restriction to the sensors list, exactly one terminal per original leaf, so it has b coordinates. The three count equations retain the distinction between all terminals and designated sensors.
oldField is the complete old owner-pair preparation x(theta); zeroExtend is the literal old-cell inclusion E. The native run performs P;S at each original alpha and S;S-left at each original beta in fixed left-to-right order, before any Tick. Its y equals E x(theta) on the actual attained material. Inherited sends alpha labels to LL and beta labels to LLL; fresh lists alpha R and beta R then LR, with branch prefixes and global allocation order. Every designated sensor is both a current terminal and the destination of an actually allocated integer label in that same run.
Installation includes an authentic exhaustive original raw table with all old identifiers below next, genuine current and fresh grants, original root/orientation, exact rational arithmetic, Hold, exclusive complete serialization and sufficient finite backing. Absent, branch, wrong-type, RangeRefusal, BadFrame, proper pending prefixes and disabled missing-right dispatch keep their original meanings; every transaction consumes all output, End, acknowledgement and Return. Physical conformance, true zero origin and record isolation remain ASSUMED-UNVERIFIED premises. There is no Reset, clone, interior numerical port, competing writer or timing/allocation/provider side channel. The theorem concerns a mathematical sector: H(theta) generally differs from the attained E x(theta). It claims neither acquisition of H(theta) nor equality of complete future service. BH(theta) may be visible at nondesignated terminals. Rights survive; restriction by observation is only the designated sensing policy.