theorem
proved
forward_accumulates
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
47 intro i _; exact abs_nonneg _
48
49/-- Forward direction: adding a step with nonzero Berry phase increases Z. -/
50theorem forward_accumulates (phases : List ℝ) (new_phase : ℝ) (hn : new_phase ≠ 0) :
51 let z_before := (phases.map fun p => |p|).foldl (· + ·) 0
52 let z_after := ((phases ++ [new_phase]).map fun p => |p|).foldl (· + ·) 0
53 z_before < z_after := by
54 simp only
55 rw [List.map_append, List.foldl_append]
56 simp only [List.map_cons, List.map_nil, List.foldl_cons, List.foldl_nil]
57 linarith [abs_pos.mpr hn]
58
59/-- Reversing a loop subtracts phase (opposite sign). -/
60theorem reverse_subtracts (phase : ℝ) :
61 let forward_phase := phase
62 let reverse_phase := -phase
63 forward_phase + reverse_phase = 0 := by
64 simp only
65 ring
66
67/-- Z-complexity uses absolute values, so reversal adds to Z, not subtracts. -/
68theorem z_absolute_immune_to_reversal (phase : ℝ) (hp : phase ≠ 0) :
69 |phase| = |-phase| := by
70 rw [abs_neg]
71
72/-- The arrow of time: if Z(t₁) < Z(t₂), then t₁ is before t₂. -/
73def isBefore (z1 z2 : ℝ) : Prop := z1 < z2
74
75/-- The before relation is transitive (time is ordered). -/
76theorem before_transitive (z1 z2 z3 : ℝ) (h12 : isBefore z1 z2) (h23 : isBefore z2 z3) :
77 isBefore z1 z3 := by
78 unfold isBefore at *; linarith
79
80/-- The before relation is irreflexive (a moment is not before itself). -/
papers checked against this theorem (showing 28 of 28)
-
Solar pretraining lifts flare classification with scarce labels
"We use the SDO archive spanning 2010-2024. Data from 2010-2020 constitute the training split and 2020-2024 the test split ... with no temporal overlap."
-
Berry phase quantifies excess responses in driven nonequilibrium cycles
"Hexc = ∮Γ dλ·R(λ) with R(λ) = ⟨∇λVλ⟩sλ; Ωμν = ∂μ⟨∂νVλ⟩sλ − ∂ν⟨∂μVλ⟩sλ measures violation of Maxwell relations (Eqs. 43-47)"
-
Latent tokens replace text for driving chain-of-thought
"interleaving (1) action-proposal tokens... and (2) world model tokens, which are grounded in a learned latent world model and express future outcomes"
-
Motion cues give VLAs hindsight and foresight for long robot tasks
"Hindsight, Insight, and Foresight... bidirectional temporal reasoning"
-
LLM agents detect sarcasm by scoring meaning-intention mismatch
"reformulate sarcasm understanding as a world model inspired reasoning process... observation→latent state→prediction→prediction error→decision"
-
Matching bounds close gap in 1-identification complexity
"Algorithm 1 … Parallel Sequential Exploration Exploitation on Brackets … round-robin execution of SEE copies … κee_b, κet_b concentration events"
-
GRB 110801A's first-burst afterglow precedes second prompt
"The early optical light curve displays a sharp transition from a rise of ∼t^{2.5} to ∼t^{6.5}... RS and FS components"
-
EPPNet best explains how diffusion models build MRI scans
"denoising trajectory ... q(x_t|x_{t-1}) = N(√(1-β_t) x_{t-1}, β_t I) ... reverse process p_θ"
-
Mueller matrices fix invariant geometric phase to retarding component
"the retarding part of the characteristic pure component selected by the characteristic decomposition, which defines a canonical holonomic content"
-
Bellman values break down into graphs for logic tasks
"Lemma 2 ... RAℓ-BE ... lim γ→1 Vγj = V*[G(∧j∈J (qj U rj))]"
-
Score discrepancy bounds show fixed CFG weights are suboptimal
"ω(t) = ω₀ exp(λ(1-t/t_max)) ... aligns the guidance strength with the diffusion dynamics via an exponential decay control function"
-
Binary spiking LM matches performance at 5 percent compute
"Rate-MSE loss aligns time-averaged spike rates over T steps (Eq. 9, 13)"
-
New pipeline turns sparse 2D MRI into 4D whole-heart models
"dual-context temporal block that fuses global and local cardiac temporal information... temporal self-attention... sliding window of size (2K+1)"
-
Simulations divide polymers into three water-interaction classes
"τ_HB … follows Arrhenius behavior … Below Tg, τ_HB … exhibits super-Arrhenius behavior."
-
Path integral method includes geometric phase from conical intersections
"the multi-electronic-state path integral (MES-PI) formulation in imaginary time naturally captures the GP effect through the electronic trace of the product of statistically weighted overlap matrices between successive imaginary-time slices"
-
Head-specific caches lift 60-second video scores from 77.87 to 81.21
"Wave Heads exhibit a small and stable fluctuation period under FFT analysis... P < β where β is determined by theoretical and experimental analysis (period threshold 6.4)."
-
Thermal Hall effect seen in quartz but absent in silica glass
"magnetic field exerts a transverse Berry force on this drift, and this force is balanced by an entropic restoring force"
-
BN doping makes naphthalene Dewar isomerization asymmetric
"The transition structure closely resembles an S0/S1 conical intersection... vibrationally activated nonradiative funnel"
-
Superconductivity boosts CDW phase coherence in cuprates
"BCS-like growth of phase coherence below Tc ... near-perfect wave-vector locking"
-
Altermagnons switch from selective damping to deformed coherence at MIT
"The resulting fluctuation propagator encodes the dynamical response, such that static and dynamical susceptibilities are computed from the corresponding slave-boson fluctuation correlators"
-
Deeper Picard iterations cut truncation error without unbounded estimation error
"the entropy-based Rademacher bound remains controlled independently of ℓ... pRΩeq ≲ 1/√n ∫ √HΩ(c(1-δ)ε) dε"
-
Non-reference net selects lowest indistinguishable resolution
"leverage the spatio-temporal limits of the human visual system... temporal masking effects... 120Hz"
-
Manifold model forecasts paper impact by tracking topic evolution
"continuous-time spatiotemporal manifold ... topic spine model ... vanguard loss ... align with the topic’s forward momentum"
-
Broadcast videos yield A-S profiles for football fatigue monitoring
"temporal smoothing... Kalman filter... Savitzky–Golay filter... l_n temporal window... ln = 20 (1.64 s)"
-
Latent visual steps lift medical VQA accuracy from 48 to 53 percent
"reusing hidden states as continuous latent steps, enabling iterative preservation and refinement of query-relevant visual evidence"
-
Capture-aware patches attack palmprint recognition
"We optimize P under an expectation-over-transformation (EoT) formulation... stochastic capture model parameterized by ξ"
-
Wireless ECGs agree with clinical data on RR intervals and HRV
"We therefore analyze data from 54 healthy subjects who performed five physical activities using wireless ECGs outside of clinical settings"
-
Test selection recast as Ising spin optimization
"CIM solver... Gaussian Approximated Positive-P (GAPP) model... spin amplitude trajectories"