Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

NativeFiniteBudgetClassification

Abstract

Native finite whole-row criterion and lawful source fibers

On the complete nonempty ActualFiber P old H, failure of analyze at any old row equal to an actual canonicalRow supplies two lawful sources at every inclusive original depth. A witnessing base is used only to rewrite the retained row in the proof. If any permitted original effective serial service at a certified N had one common finite raw bound and correct complete rowWord output, original_whole_row_implies_depth_and_image would provide such a determining depth, contradicting the pair at that depth. This excludes all permitted serial services for every N; it does not restrict their workspace, local computation, address lengths or update counts to those of a finite table. The stationary positive construction and exact operational realization are described in NativeWholeRowService and NativePassiveServiceRealization. Uniform encoded common-input materializer computability remains an additional effectiveness assertion.

Definition 1.1 (unarySpecialize).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.unarySpecialize

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.unarySpecialize (✓ std3).

Source. Repository-derived.

Commentary.

Repository-derived native finite-term construction used by the whole-fiber results.

Definition 1.2 (forbidden).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.forbidden

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.forbidden (✓ std3).

Source. Repository-derived.

Commentary.

Repository-derived native finite-term construction used by the whole-fiber results.

Definition 1.3 (sigmaTerm).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.sigmaTerm

Formalization. D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.sigmaTerm (✓ std3).

Source. Repository-derived.

Commentary.

Repository-derived native finite-term construction used by the whole-fiber results.

Theorem 1.4 (lawful nonground perturbation).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.lawful_nonground_perturbation

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.lawful_nonground_perturbation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Equal-mass separation gives a lawful equality solution. Change only a genuine bound coordinate below inclusive depth h, avoid the complete finite old-inequality exclusion set, and preserve the same Y restriction. All-solutions factorization forces the selected new equation to become unequal. Native statement: theorem lawful_nonground_perturbation {X : Type} [Fintype X] [DecidableEq X] (p : Presentation X) (A B : Term X) (Δ : Equations X) (S : SubstInfo) (hok : (encodeEquations p [(A,B)]).unify SubstInfo.empty = .ok S) (noCollapse : collapse p S Δ = false) (x : X) (bound : x ∈ D p S) (nonground : termVars (action p S x) ≠ []) (h : Nat) : ∃ v w : X → Source, Diseq Δ v ∧ Diseq Δ w ∧ evaluate v A = evaluate v B ∧ evaluate w A ≠ evaluate w B ∧ (∀ y a, a.length ≤ h → readout a (v y) = readout a (w y))

Theorem 1.5 (nonground full fiber obstruction).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.nonground_full_fiber_obstruction

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.nonground_full_fiber_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

At every inclusive original depth, both valuations lift to the same complete old-row/history fiber. The selected reached-hole relation changes, so the complete canonical new rows differ. Native statement: theorem nonground_full_fiber_obstruction (P Q : CutSet) (hP : CutPrefixFree P) (hQ : CutPrefixFree Q) (base : Source) (H : History) (η : Patterns (canonicalRow P base) (requiredDepth Q H)) (pass : feasible η H = true) (q r : Address) (hq : q ∈ symbolicOrdered Q (wholeTerm η)) (hr : r ∈ symbolicOrdered Q (wholeTerm η)) (A B : Term (Variables η)) (atq : termAt q (wholeTerm η) = some A) (atr : termAt r (wholeTerm η) = some B) (S : SubstInfo) (hok : (encodeEquations (presentation η) [(A,B)]).unify SubstInfo.empty = .ok S) (noCollapse : collapse (presentation η) S (delta η) = false) (x : Variables η) (bound : x ∈ D (presentation η) S) (nonground : termVars (action (presentation η) S x) ≠ []) : ∀ h : Nat, ∃ u v : Source, (canonicalRow P u = canonicalRow P base ∧ NativeDepthPatterns.Consistent H u) ∧ (canonicalRow P v = canonicalRow P base ∧ NativeDepthPatterns.Consistent H v) ∧ (∀ a : Address, a.length ≤ h → readout a u = readout a v) ∧ canonicalRow Q u ≠ canonicalRow Q v

Theorem 1.6 (exterior full fiber infinite).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.exterior_full_fiber_infinite

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.exterior_full_fiber_infinite (✓ std3). ∎

Source. Repository-derived.

Commentary.

A residual exterior coordinate has infinitely many lawful replacements after finite exclusion. Free-constructor projection recovers each replacement from the complete concrete exterior. Native statement: theorem exterior_full_fiber_infinite (P Q : CutSet) (hP : CutPrefixFree P) (hQ : CutPrefixFree Q) (base : Source) (H : History) (η : Patterns (canonicalRow P base) (requiredDepth Q H)) (pass : feasible η H = true) (x : Variables η) (outside : x ∈ exteriorVariables (symbolicExterior Q [] (wholeTerm η))) : Set.Infinite ((canonicalRow Q) ‘’ {u : Source | canonicalRow P u = canonicalRow P base ∧ NativeDepthPatterns.Consistent H u})

Theorem 1.7 (exterior no finite depth).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.exterior_no_finite_depth

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.exterior_no_finite_depth (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite Pattern h plus one carrier makes every depth-determined row image finite. The infinite full-row image therefore refutes every finite determining depth. Native statement: theorem exterior_no_finite_depth (P Q : CutSet) (hP : CutPrefixFree P) (hQ : CutPrefixFree Q) (base : Source) (H : History) (η : Patterns (canonicalRow P base) (requiredDepth Q H)) (pass : feasible η H = true) (x : Variables η) (outside : x ∈ exteriorVariables (symbolicExterior Q [] (wholeTerm η))) : ∀ h : Nat, ∃ u v : Source, (canonicalRow P u = canonicalRow P base ∧ NativeDepthPatterns.Consistent H u) ∧ (canonicalRow P v = canonicalRow P base ∧ NativeDepthPatterns.Consistent H v) ∧ (∀ a : Address, a.length ≤ h → readout a u = readout a v) ∧ canonicalRow Q u ≠ canonicalRow Q v

Theorem 1.8 (criterion failure arbitrary depth).

Lean statement: D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.criterion_failure_arbitrary_depth

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/Observer/NativeFiniteBudgetClassification.criterion_failure_arbitrary_depth (✓ std3). ∎

Source. Repository-derived.

Commentary.

Failure of the actual whole criterion yields a feasible bad cell. Exterior freedom and feasible genuine nonground binding cover both alternatives, producing lawful whole-row discrepancy at every inclusive depth without an operational-service assumption. Native statement: theorem criterion_failure_arbitrary_depth (P Q : CutSet) (hP : CutPrefixFree P) (hQ : CutPrefixFree Q) (base : Source) (H : History) (bad : (analyze (canonicalRow P base) Q H).passes = false) : ∀ h : Nat, ∃ u v : Source, (canonicalRow P u = canonicalRow P base ∧ NativeDepthPatterns.Consistent H u) ∧ (canonicalRow P v = canonicalRow P base ∧ NativeDepthPatterns.Consistent H v) ∧ (∀ a : Address, a.length ≤ h → readout a u = readout a v) ∧ canonicalRow Q u ≠ canonicalRow Q v

References